수년간 OCaml로 개발해 온 필자가 왜 Lean 4로 주 언어를 옮겼는지, OCaml의 보수성, 최적화·메타프로그래밍·빌드 시스템 등의 이슈와 Lean에서의 대비점을 실제 코드와 함께 설명합니다.
왜 Lean 4가 나의 주 언어로 OCaml을 대체했는가
오늘 해커 뉴스(Hacker News)를 읽다가 우연히 "Why I Chose OCaml as my Primary Language"라는 글을 보게 됐습니다.
이 글은 저에게 특히 흥미로웠습니다. 지난 몇 년 동안 저는 점차적으로1 제 주 언어를 OCaml에서 더 새롭고 더 뜨거운 언어인 Lean으로 옮겨왔고, 글쓴이가 왜 OCaml을 선택했는지는 이해하지만, 개인적으로는 같은 결정을 내리진 않았을 것 같거든요.
그 글이 OCaml의 미덕을 시적으로 찬양한다면, 반대편 이야기도 흥미로울 것 같았습니다 — 왜 당신의 주 언어로 OCaml을 원하지 않을 수도 있는지 — 그리고 다년간 경험이 있고 다작한3 전(前) OCaml 개발자(그리고 올해 OCaml 워크숍 의장~)의 관점에서요.
이 글의 나머지 부분에서는 지난 반십 년 동안 OCaml로 해킹하며 겪은 몇 가지 고충과, 결국 왜 그 때문에 다른 언어로 옮기게 되었는지를 살펴보겠습니다. 덤으로, 각 이슈마다 Lean에서는 이 문제가 어떻게 해결되는지 맛보기 예시도 곁들이고, 왜 Lean에 대해 이렇게 흥분하는지 살짝 암시하겠습니다.
이 글의 목적은 OCaml을 쓸데없이 깎아내리려는 것이 아닙니다. 저는 OCaml에 상당한3 노력을 투자했으며, 그 시간들을 매우 애정 어린 시선으로 돌아봅니다. 제가 이 이슈들을 지적하는 이유는 더 넓은 커뮤니티가 Lean 같은 새로운 언어들에 흥미를 느끼길 바람과 동시에, OCaml 커뮤니티가 개선할 수 있는 지점들에도 스포트라이트를 비추고 싶기 때문입니다!
그럼 바로 들어가봅시다!
OCaml의 중요한 특징 중 하나는 언어나 커뮤니티 모두가 “놀랄 일이 없는” 것을 자랑스럽게 여긴다는 점입니다. 이는 WYSIWY(보이는 대로 동작)의 철학으로 반영됩니다.
OCaml 코드 전반의 핵심 원칙은, 코드를 이해하기 매우 쉽다는 것입니다. 숙련된 OCaml 개발자는 어떤 함수가 런타임에서 정확히 어떻게 동작하는지, 성능 특성이 어떤지, 메모리 할당은 어떻게 이루어지는지를 빠르게 말할 수 있습니다.
let List.iter f =
function
| [] -> () (* 할당 없음 *)
| h :: t -> f h; List.iter f t (* 할당 없음 *)
let sum ls =
let sum = { contents = 0 } in (* 할당 (1 블록) *)
let f x = sum := !sum + x in (* 할당 (클로저) *)
List.iter f ls; (* 할당 없음 *)
a.contents (* 할당 없음 *)
예를 들어, 위 코드 블록만 봐도 힙에 메모리 블록 1개와 클로저 1개를 할당한다는 것을 즉시 알 수 있습니다.
이 단순화된 모델 덕분에 런타임 성능이 매우 예측 가능하고, 수동으로 최적화하기도 쉽습니다. 하지만…
이 말은 곧, 코드를 빠르게 만드는 책임이 전적으로 개발자에게만 있다는 뜻이고, 때로는 성능을 위해 프로그램의 _논리_를 흐리게 만들어야 할 수도 있다는 뜻입니다.
좀 더 구체적으로, 리스트의 합을 계산하면서 동시에 각 값을 그 인덱스만큼 증가시키는 다음 함수를 생각해 봅시다:
let incr_sum ls =
let f = (fun (sum, i) vl -> (* 할당 (클로저) *)
let sum = sum + vl in
let vl = vl + i in
let acc = (sum, i + 1) in (* 할당 (튜플) *)
(vl, acc) (* 할당 (튜플) *)
)
let (ls, (sum, _len)) ==
List.fold_map ls (0,0) in (* 할당 (리스트 + 튜플) *)
(ls, sum) (* 할당 (튜플) *)
할당을 분명히 보이게 하려고 일부러 늘여 썼습니다만, 정말 코드 골프를 하듯 쓴다면 제 코드는 아마 아래처럼 단순화했을 겁니다:
let incr_sum ls =
let open Pair in
let update vl =
Fun.flip (map_same2 (+)) (vl, 1) &&& snd_map ((+) vl) in
List.fold_map (Fun.flip update) (0,0) ls
|> map_fst fst
|> swap
읽기 어려운 코드는 해스켈만의 전유물이 아니죠4. 어쨌든 성능 관점에서 보면, 이 구현은 (단순화한 버전은 말할 것도 없이) 중간 튜플과 클로저를 많이 할당하기 때문에 최적은 아닙니다.
메모리가 제약이 된다면, 보수적인 최적화만 수행하는5 OCaml 컴파일러 특성상, 원하는 할당 패턴을 얻기 위해 이 함수를 다시 찾아와 수동으로 고쳐 써야 합니다. 예를 들면 다음과 같습니다:
let incr_sum ls =
let i = ref 0 in (* 할당 (블록) *)
let sum = ref 0 in (* 할당 (블록) *)
let f = (fun vl -> (* 할당 (클로저) *)
i := !i + 1;
sum := !sum + vl;
vl + (!i - 1) (* 핫패스에서 추가 할당 없음 *)
) in
let ls = List.map f ls in (* 할당 (리스트) *)
(ls, !sum) (* 할당 (튜플) *)
명령형 배경이라면 이 버전이 “더 좋아” 보일 수 있습니다. 하지만 큰 함수형 프로그램에서는 이런 함수형 파이프라인을 쌓는 방식이 더 관용적이고 코드도 짧아지며, 숙련된 OCaml 개발자들에게는 꽤 흔한 스타일입니다.
여기서 핵심은, 개별 개발자 관점에서 의도(이를테면 리스트에 대해 어떤 폴드를 계산한다는 것)를 간결히 표현하는 것과 높은 성능을 얻는 것 사이에서 타협을 강요받는다는 점입니다. 진공 상태라면 이런 타협도 괜찮을 수 있지만, 유지보수 부담 증가라는 비용이 따라옵니다.
이제 Lean에서는 어떻게 다른지 이야기해 봅시다.
새로운 언어이니만큼 커뮤니티 방향에 대해 장담하긴 어렵고, 제가 아는 한 지금 컴파일러가 급진적인 최적화를 하지는 않습니다. 하지만 언어 자체가 a) 더 많은 메모리 재사용(참조 카운팅과 메모리 재사용을 영리하게 결합한 Perceus 덕분), b) 순수 함수형 언어로 컴파일되면서도 확장 가능한 형태의 최적화를 가능하게 하는 매크로 기반 추상화 타워 덕분에 이를 보완합니다:
def incr_sum (ls: List Int) : List Int × Int := Id.run $ do
let mut sum := 0
let mut res := #[]
for (vl, i) in ls.zipIdx do
sum := sum + 1
res := res.push (vl + i)
return (res.toList, sum)
인정하건대, 위 코드의 추상화들 때문에 OCaml보다 약간 느릴 수도 있습니다. 하지만 Lean의 메타프로그래밍 지원이 좋은 점은, 이론적으로 필요할 때 파이프라인에 우리만의 최적화를 점진적으로 주입할 수 있다는 것입니다. 매크로 이야기는 곧 다시 하겠습니다.
언어 자체의 보수성에서 뻗어나가, 이런 보수적이고 하위 호환을 중시하는 철학은 언어의 컴파일러 생태계에도 어느 정도 확장됩니다. OCaml은 놀랄 만큼 안정적인 언어이며, 생태계에 이렇게 높은 기준을 고집하는 커뮤니티에 큰 박수를 보냅니다.
10년도 더 된 코드라도, 최신 OCaml 컴파일러에서 거의 바꾸지 않거나 아주 최소한만 수정하고도 돌아간다고 장담할 수 있습니다.
이는 시간이 흘러도 코드의 유용성을 담보해준다는 점에서 훌륭합니다. 하지만 안타깝게도 그 대가로 언어의 발전 속도가 매우 느리며, 이는 표준 라이브러리 같은 부분에도 그대로 적용됩니다.
다음은 동적 배열을 추가하는 논의—즉 O(1) 접근과 크기 변경이 가능한 배열 자료구조—를 생각해 봅시다:
type 'a t (* 동적 배열 *)
val alloc: int -> 'a t (* 할당 *)
val (.[]): 'a t -> int -> 'a (* O(1) 조회 *)
val (.[]<-): 'a t -> int -> 'a -> unit (* O(1) 갱신 *)
val push: 'a t -> 'a -> unit (* 필요 시 재할당 *)
이는 2019년에(무려 6년 전!!) 커뮤니티의 새내기가 처음 제안했습니다:
PR은 곧 명명 규칙 같은 비본질적 논의에 휩쓸렸고 결국 닫혔습니다.
3년 뒤, 두 번째 시도로 또 다른 PR이 만들어졌지만, 결과는 같았습니다:
이 긴 사가는 작년에 와서야 마침내 결론이 났고, 동적 배열이 표준 라이브러리에 합류했습니다:
물론 이렇게 단순한 자료구조를 도입하는 데도 커뮤니티가 신중을 기한 정당한 이유가 있었습니다. 하위 호환성을 중시하는 만큼, 표준 라이브러리에 들어오는 것은 앞으로도 계속 유지보수해야 함을 뜻하니 매우 조심스럽게 움직일 필요가 있었죠.
다시 강조하자면, 하위 호환성에 대한 OCaml의 강한 헌신은 진정으로 언어의 가장 인상적인 특징 중 하나입니다. 하지만 자신이 선택한 언어에서 새로운 추상화를 확장·탐구하고 싶은 개발자 입장에서는 이게 다소 김을 새게 할 수 있겠죠.
type-classes의 OCaml식 변형인 [모듈러 임플리시트(Modular Implicits)]는 수년째 논의되어 왔지만, 가까운 시일 내에 배포될 가능성은 낮습니다:
대조적으로 Lean은 이제 막 등장한 패기 넘치는 신예라서, 언어 개발자들이 훨씬 더 빠르게 움직이고 과감한 변경도 마다하지 않습니다. 그 결과 최신 Lean으로 업데이트하면 정말로 코드가 깨질 때가 자주 있고, 그럴 때 핵심 라이브러리를 고치는 데 매달리는 작은 생태계가 존재합니다. 하지만 멋진 점은 언어의 개발자이자 사용자로서, 여러분의 변경을 언어에 실제로 반영시키는 일이 충분히 가능하다는 것입니다.
상대적으로 작은 이슈이긴 하지만, 예전에 꽤 고생한 적이 있어 언급할 가치가 있다고 봅니다.
OCaml의 빌드 시스템은 오랜 시간에 걸쳐 많이 진화했고, 대부분에게 잘 작동하는 견고하고 효율적인 해법에 수렴하는 데 시간이 걸렸습니다. Jane Street가 만든 Dune 빌드 시스템 덕분에, 이제 OCaml은 빌드 측면에서 아주 멋지고 일관된 스토리를 갖게 됐습니다.
프로젝트와 의존성을 꽤 무난하고 단순한 s-식 기반 문법으로 기술하는 dune 파일만 작성하면, 짜잔, 거의 수고 없이 빌드됩니다~
(library
(name lib)
(deps ...))
…물론 “행복 경로(happy path)”에서 크게 벗어나지 않는다는 전제하에서요.
즉, dune은 대부분의 OCaml 프로젝트에 잘 맞습니다만, 스스로를 “의견이 강한 빌드 관리자”라 부르는 만큼 의도적으로 가능한 빌드 액션을 제한합니다 — 빌드 과정의 일부로 텍스트를 생성한다든가 하는 일을 하려 들면, 곧바로 벽을 맞닥뜨리게 될 겁니다.
Dune은 순수 OCaml 너머로도 여러 확장을 지원합니다. 예를 들어 FFI를 위한 Ctypes 기반 프로젝트, C 빌드, 심지어 Rocq 빌드도 어느 정도 지원합니다. 다만 이런 확장들은 대부분 Jane Street가 원하거나 사용하는 것들을 중심으로 움직이기에, 정해진 길에서 너무 멀어지면 고생을 하게 됩니다.
여기서 Lean과 비교하는 건 완전히 공정하진 않습니다. Lean은 아직 나이가 어려서 어떤 빌드 과정을 최종적으로 채택할지 정리 중이고, 패키지 매니지먼트도 OCaml만큼 견고하다고 하긴 어렵습니다(버전이 살짝만 어긋나도 관계없는 패키지가 빌드에 실패하는 문제를 꽤 자주 겪습니다).
그럼에도 꼭 짚고 싶은 멋진 점이 하나 있습니다:
Lean의 Lake 빌드 파일은 Lean 자체로 작성됩니다!
이게 영원히 그럴지는 모르겠습니다. 문서상으론 TOML로 이동하려는 흐름도 보이긴 합니다. 그래도 이 글을 쓰는 시점에는 Lean 프로젝트의 빌드 기술 형식 중 하나가, 빌드 DSL을 임포트한 Lean 파일 자체입니다:
import Lake
open Lean Lake DSL
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
require betterfind from "./BetterFind"
package probability where
lean_lib BallsInBins where
Lakefile은 그 자체가 Lean 코드이고, Lean의 메타프로그래밍 설비의 확장성 덕분에, 빌드 프로세스에 자신만의 확장을 구성하는 데 엄청난 유연성을 제공합니다. 주말 동안 혼자서 Dune에서 필요했던 기능 여러 개를 재구현하기도 했습니다. 예를 들어 OCaml의 ctypes/ctypes-build의 제한적 대체물, 혹은 LaTeX PDF 생성 같은 것들이요.
여기까지 제가 OCaml을 사용하면서 겪은 가장 큰 고충들을 정리해 보았습니다. 이 글이 언어와 그 특징들을 다른 관점에서 바라보는 기회를 제공했고, 혹시 마음에 들지 않을 수 있는 부분들을 보여줬기를 바랍니다.
모든 비판에는 일종의 단서가 있습니다. 어떤 의미에서 이 문제들은 솔로 개발자일 때만 문제일 수 있다는 점입니다 — 언어의 WYSIWY 특성, 제한적인 메타프로그래밍 지원, 제약이 있는 빌드 시스템과 런타임 표현은, 만약 여러분이 안정적이고 일관된 코드를 원하는 회사라면 오히려 장점일 수 있습니다. 이는 Jane Street나 Ahrefs 같은 회사에서 OCaml이 인기 있는 이유를 설명해 줍니다. 지루하고 재미없는 코드가 오히려 분명한 장점이니까요(매크로 오타 하나로 수십 억을 날린 일을 설명하고 싶은 사람은 아무도 없습니다).
그럼에도, 첨단 PL 연구의 최신 기능을 갖춘 정말로 유연하고 확장 가능한 프로그래밍 언어의 승수 효과를 누리고 싶은 개발자라면, Lean을 한 번 써보길 권합니다!
게다가, 덤으로 최첨단 수학 연구에 기여하게 될지도 모릅니다~
마침 물리적으로 성별 전환을 하던 시기와도 겹쳤답니다 ㅎㅎ~
Lean은 의존형 정리 증명기이면서 동시에 실용적이고 쓸 만한 함수형 언어라는 점에서 특히 흥미롭습니다. 일상적인 사용에서는 OCaml과 충분히 겨룰 만합니다.
이 글의 핵심에는 그리 중요하지 않지만, 제 OCaml 커뮤니티 내 자격증명은 대략 다음과 같습니다.
믿기 어렵겠지만, 위는 저 나름대로 자제한 버전입니다. 정말로 코드 골프를 한다면 아마 이렇게 썼을 겁니다:
let incr_sum ls =
let open Fun in
let update =
curry
Pair.((fold (flip (map_same2 (+)) % (flip make 1))
&&& fold (snd_map % (+))) % swap) in
List.fold_map update (0,0) ls
|> Pair.swap % Pair.map_fst fst
아름답죠.
Flambda 모드는 상황을 조금 개선하긴 하지만, 무엇을 최적화할지는 여전히 극도로 보수적입니다.
파서를 확장하기가 너무 쉬워서, 제 프로젝트 중에는 아예 다른 언어의 문법을 Lean 안에 임베드한 것도 있습니다. 예컨대 Clingo 답 집합 프로그래밍 언어 바인딩 같은 경우가 그렇습니다.
declare_syntax_cat clingo_symbol
syntax "#inf" : clingo_symbol
syntax "#sup" : clingo_symbol
syntax num : clingo_symbol
syntax str : clingo_symbol
syntax ident : clingo_symbol
declare_syntax_cat clingo_term
-- symbol
syntax (name := clingo_term_symbolic) clingo_symbol : clingo_term
-- unary operators
syntax "-" clingo_term : clingo_term
syntax "~" clingo_term : clingo_term
syntax "|" clingo_term "|" : clingo_term
-- binary operators
syntax:10 clingo_term:10 " ^ " clingo_term:11 : clingo_term
syntax:20 clingo_term:20 " ? " clingo_term:21 : clingo_term
syntax:30 clingo_term:30 " & " clingo_term:31 : clingo_term
syntax:40 clingo_term:40 " + " clingo_term:41 : clingo_term
syntax:50 clingo_term:50 " - " clingo_term:51 : clingo_term
syntax:60 clingo_term:60 " * " clingo_term:61 : clingo_term
syntax:70 clingo_term:70 " / " clingo_term:71 : clingo_term
syntax:80 clingo_term:80 " \\ " clingo_term:81 : clingo_term
syntax:90 clingo_term:90 " ** " clingo_term:91 : clingo_term