효과를 타입 시스템 안에서 추적하고 최적화하여 비용 없이 다루려는 Prism 컴파일러의 설계와 아이디어를 소개한다.
이번 글은 아주 괴짜 같은 내용이 될 테니 조금만 참아 주시기 바랍니다. 여기 함수가 하나 있습니다. 다른 함수 읽듯이 읽어 보고, 그다음 타입이 무엇인지 말해 보세요.
fn fib(n) =
var a := 0
var b := 1
repeat(n) fn
let t = a + b
a := b
b := t
a
이것은 가변 루프입니다. var가 있고, 할당이 있고, 스왑이 자기 자신을 먹어 버리지 않도록 임시 변수가 있습니다. 한 줄 한 줄 그대로, 재귀는 젊은이들의 놀이라고 결심한 뒤 Python에서 쓰게 될 fib입니다.
이 함수의 타입은 Int -> Int이며, 제자리에서 동작하는 함수형입니다. 함수에 효과가 있는데도 효과 타입이 없는 이유는, 그 효과가 함수 바깥에서는 관찰되지 않기 때문입니다. 이 함수를 호출하는 누구의 입장에서 보더라도, 이 함수는 순수합니다. 내부에서 두 변수를 제자리에서 바꾸고, 문이 닫히기 전에 증거를 말끔히 치워 지문 하나 남기지 않습니다. 그리고 그 모든 일을 컴파일러가 대신 해 줍니다. Python에서 쓸 법한 코드에, OCaml에서 얻는 타입과, 모나드 없는 조합입니다.
이것이 Prism입니다. 지난 3년 동안 제가 작업해 온 개념 증명용 함수형 컴파일러로, OCaml 5, Haskell, Koka의 지적 계보에서 영감을 받은 현대적 타입으로 효과를 모델링하는 데 중심을 두고 있습니다. 지난 5~6년의 함수형 프로그래밍에서 핵심 아이디어는 이렇습니다. 효과는 현실이고, 효과는 괜찮으며, 흥미로운 질문은 그것을 어떻게 피할지가 아니라 어떻게 타입 시스템 안에 넣고, 그 비용이 0이 될 때까지 최적화할지입니다.
필요한 아이디어는 하나뿐입니다. 대수적 효과 핸들러입니다. 효과는 연산을 선언하고, 핸들러는 그 연산에 의미를 부여합니다. 다음은 시퀀스를 산출하는 생산자이며, 누가 듣고 있는지는 전혀 모릅니다.
effect Gen {
ctl yield(Int) : Unit
}
fn produce(n) : !{Gen} Unit =
if n == 0 then
()
else
yield(n)
produce(n - 1)
타입의 !{Gen}은 이 함수가 yield 연산을 수행한다는 사실을 문서로 인정하는 것이고, 따라서 상위 어딘가에서 반드시 처리해 주어야 한다는 뜻입니다. 이제 같은 생산자를 두 개의 다른 핸들러에 넘겨 보겠습니다.
fn total(n) =
handle produce(n) with
yield(v, k) => v + k(())
return r => 0
fn count(n) =
handle produce(n) with
yield(v, k) => 1 + k(())
return r => 0
k는 continuation, 즉 나머지 계산이며, 손에 쥘 수 있는 평범한 값으로 구체화되어 있습니다. total은 그것을 재개해서 더하고, count는 재개해서 개수를 셉니다. 핸들러는 k를 완전히 무시할 수도 있고(그것은 예외입니다), 한 번 호출할 수도 있으며(그것은 상태이거나 생성기입니다), 여러 번 호출할 수도 있습니다. 마지막 경우가 대수적 효과를 단순한 문법 설탕 이상으로 만드는 동작입니다. 여기서는 핸들러가 후보마다 같은 continuation을 다시 재개함으로써 피타고라스 삼중항을 찾습니다. 다시 말해, 직선형 코드와 “그래, 그리고 다른 갈래도 해 봐”라고 말하는 핸들러만으로 전체 탐색 트리를 뒤집니다.
effect Amb {
ctl choose(Int) : Int,
ctl reject(Unit) : Int
}
fn triple(n) : !{Amb} Int =
let a = choose(n)
let b = choose(n)
let c = choose(n)
if a > 0 && b > 0 && a <= b && a * a + b * b == c * c then
a * 10000 + b * 100 + c
else
reject(())
fn solutions(n) =
handle triple(n) with
choose(m, k) => flatten(map(\(i) -> k(i), range(0, m)))
reject(u, k) => Nil
return r => Cons(r, Nil)
fn main() =
let sols = solutions(14)
println(length(sols))
println(sum(sols))
choose(n)은 0..n-1 안의 값을 하나 제안하고, reject()는 막다른 가지를 잘라냅니다. 그리고 핸들러가 후보마다 k를 한 번씩 재개하므로, triple은 그냥 숫자 세 개를 고르는 함수처럼 읽힙니다.
OCaml 5를 써 보셨다면 익숙하게 느껴질 것입니다. 다만 OCaml은 효과를 타입 밖에 두므로, 처리되지 않은 효과가 있다는 사실을 금요일 운영 환경 런타임에서야 알게 됩니다. Haskell을 써 보셨다면 이것도 익숙할 것입니다. 다만 Haskell에서는 모나드 트랜스포머 스택을 조립하고, 각 연산을 모든 층을 거쳐 손으로 lift하고, 주니어 동료에게 모나드는 endofunctor 범주에서의 monoid일 뿐인데 뭐가 문제냐고 설명해야 합니다. Prism의 효과는 row polymorphic입니다. 호출을 가로질러 구조적으로 합집합을 이룹니다. 쌓을 탑도 없고 lift할 것도 없습니다. 탑이 아니라 집합일 뿐이기 때문입니다.
효과가 일급이 되면, 지난 30년 언어 설계의 놀랄 만큼 많은 아이디어가 사실 같은 메커니즘 아래에서 통합된다는 점이 드러납니다.
예외는 continuation을 버리는 핸들러입니다. final ctl로 표시된 절은 k를 버리므로, 본문 값이 핸들러의 결과가 되고 나머지 계산은 그냥 폐기됩니다. Result를 줄줄이 전달할 필요도 없고, 호출 스택 위로 ? 색종이를 뿌릴 필요도 없습니다. 그냥 직접 스타일 코드가 멈추면 됩니다.
fn safe_grade(n) =
handle grade(n) with
final ctl abort(msg) => concat("invalid: ", msg)
return r => r
그리고 예외는 효과 row 안의 라벨일 뿐이므로, 확장 가능한 예외를 공짜로 얻습니다. 서로 다른 실패는 각각 자기만의 연산이므로, 함수 타입의 row는 그 함수에서 정확히 어떤 예외가 빠져나갈 수 있는지 나타냅니다. !{Gen}이 이 함수가 yield한다는 사실을 적어 주는 것과 같은 방식입니다. 상속받아야 할 루트 Exception 클래스도 없고, 수정해야 할 계층도 없습니다. 새 예외는 그냥 새 라벨입니다. 호출을 가로질러 구조적으로 합집합을 이루므로, abort할 수 있는 함수와 timeout할 수 있는 함수를 조합하면 row에 둘 다 담긴 함수가 됩니다. 그중 하나를 처리하면 그 라벨만 사라지고 나머지는 row에 남습니다. 즉, 부분 복구는 주석으로 약속하는 일이 아니라 타입 시스템이 추적하는 일이 됩니다.
effect Abort { ctl abort(String) : Unit }
effect Timeout { ctl timeout(Int) : Unit }
-- fetch의 row는 발생시킬 수 있는 두 실패를 모두 적어 둔다
fn fetch(id) : !{Abort, Timeout} String =
if id < 0 then abort("bad id")
if id > 99 then timeout(id)
"ok"
-- Timeout은 기본값으로 해소하고, Abort는 그대로 빠져나간다
fn with_default(id) : !{Abort} String =
handle fetch(id) with
final ctl timeout(_) => "cached"
return r => r
핸들러가 Timeout을 벗겨 내므로, with_default에는 정확히 !{Abort}만 남습니다. 더 많지도 적지도 않습니다. Java의 checked exception은 원래 이런 것이 되고 싶었지만, 열린 구조적 집합이 아니라 클래스 계층에 용접되어 있었기 때문에 실패했습니다.
생성기와 스트림은 emit을 수행하는 생산자, 그것을 받아 다시 emit하는 변환기, 그리고 접는 소비자입니다. 파이프라인은 하나의 생산자 주위에 중첩된 핸들러들이므로, 중간 리스트가 애초에 생기지 않습니다.
srange(1, n).smap(square).skeep(even).stake(5).ssum()
조기 종료, 즉 stake(5)는 필요한 것을 얻고 나면 continuation을 버리는 핸들러일 뿐입니다. 취소는 쓰레기를 만들고, 그 쓰레기는 컬렉터 없이 정적으로 알려진 지점에서 회수됩니다. 이것이 앞에서 예고한 좋은 부분이며, 곧 다시 돌아오겠습니다. 이 스트림 라이브러리는 Haskell의 pipes와 conduit에서 영감을 받았습니다.
렌즈는 더 이상 라이브러리가 아니라 언어에 통합되어 있습니다. 레코드 갱신 경로와 메모리 모델이 그것입니다. 중첩된 레코드 타입이 세 개 있을 때, 하나의 경로 표현식으로 임의 깊이까지 도달해 여러 필드를 한 번에 설정할 수 있습니다.
type Vec2 = Vec2 { x: Int, y: Int }
type Player = Player { pos: Vec2, hp: Int }
type Game = Game { player: Player, score: Int } deriving (Lens)
let g2 = { g | player.pos.x = 30, player.hp = 95, score = 110 }
이 코드는 중첩 레코드의 spine을 다시 만들고, 값이 유일 소유 상태라면 각 재구성이 방금 분해한 셀을 재사용하므로 함수형 업데이트가 포인터 쓰기로 컴파일됩니다. optic 타입은 할당되지 않고, 런타임에 아무것도 합성되지 않으며, 경로는 그냥 주소들입니다. 전체 optics 생태계, van Laarhoven 인코딩, profunctor 동물원, 고양이가 키보드 위를 걸어간 것 같은 연산자들, 그 모든 것이 여기서는 하나의 문법 규칙과 하나의 메모리 규율로 무너져 내립니다. 그리고 정말로 접근자를 인자로 넘겨야 할 때는 deriving (Lens)가 score_of와 with_score를 평범한 함수로 만들어 줍니다.
let g3 = with_score(g2, 200) -- score_of(g3) == 200
이 함수들은 지루한 함수들입니다. 함수형 프로그래밍에서 이보다 더 큰 칭찬은 없습니다!
가변 상태는 글 서두의 var입니다. 각 var는 get과 set 연산을 가진 비공개 효과로 디슈가되며, 그 블록 끝에 설치된 핸들러가 이를 해소합니다. 상태는 절대 바깥으로 빠져나가지 않으며, 그것을 몰래 빼내려는 클로저는 분석 단계에서 거부되고, 바깥 함수를 둘러싼 row는 빈 상태로 남습니다. 이것은 Python에서 쓰고 싶은 루프를, Haskell에서 원할 법한 시그니처와 함께, 그 사이의 State 모나드 배관 공사 없이 쓰는 방식입니다.
실패는 가장 재미있습니다. 함수형 논리 프로그래밍이 효과 row를 통해 슬그머니 들어오기 때문입니다. 익명 Fail 효과는 “이 표현식은 값을 만들어 내지 못할 수도 있다”를 타입 시스템이 이미 말할 수 있는 개념으로 만듭니다. fail()은 그것을 수행하고, guard(cond)는 조건이 거짓일 때 그것을 수행하며, 소비자 측 문법은 소원 목록처럼 보입니다.
let port = cfg.at_map("port") ?? cfg.at_map("https") ?? 443
let off = customer?.tier?.discount ?? 0
let bill = [item for item in sof(cart), if prices.at_map(item) > 4]
??는 왼쪽이 실패하면 대체값으로 넘어갑니다. ?.는 option을 따라가며 단락 평가합니다. comprehension의 guard는 실패한 원소를 충돌 없이 걸러냅니다. 그리고 var 자체도 핸들러 문법 설탕일 뿐이므로, 블록 전체를 트랜잭션으로 만들 수도 있습니다. transact는 살아 있는 모든 변수를 스냅샷하고, 본문을 실패 문맥에서 실행한 뒤, 실패하면 모든 것을 되돌립니다. 그래서 잔고 부족 계좌는 구매가 아예 없었던 것처럼 동작합니다.
transact
balance := balance - price
guard(balance >= 0)
balance
else
0
다섯 가지 기능. 하나의 바탕 메커니즘. 다섯 차원의 프리즘을 통해 바라본 모습입니다. 그리고 그 아름다운 아이디어가 바로 이름의 유래이기도 합니다.
지금까지 타입 시그니처를 많이 보지 못했는데, 그게 요점입니다. 대부분의 경우 거의 Python처럼 생긴 코드를 쓰면, 통상적인 complete-and-easy Dunfield-Krishnaswami 알고리즘을 통해 추론이 결정 가능하고 예측 가능합니다. 진짜로 higher-rank 영역에 들어갈 때만 주석을 달면 되는데, 그런 경우는 드뭅니다. 그리고 이 알고리즘은 바로 그 경계에서 정확히 당신을 맞이합니다. 함수는 binder에 forall을 선언함으로써 진짜 다형적 인자를 요구할 수 있고, 그러면 본문 하나 안에서 그것을 여러 타입으로 사용할 수 있습니다.
fn pick(g : forall a. (a) -> a) : Int =
if g(true) then
g(10)
else
g(20)
fn main() =
println(pick(\(x) -> x))
g는 다형적이어야 하므로, pick은 같은 숨결 안에서 그것을 Bool에도 적용하고 Int에도 적용할 수 있습니다. 그래서 main은 항등 함수만 넘길 수 있고, 예를 들어 숫자는 넘길 수 없습니다. Damas-Milner 코어였다면 첫 번째 호출에서 a를 Bool과 unify하고 두 번째를 거부했겠지만, 여기서는 forall이 인자 안에 살아남습니다.
임시적 다형성은 타입 클래스이지만, Lean 풍입니다. 인스턴스는 전역 탐색이 익명으로 불러내는 마법이 아니라, 이름 붙은 값이며, 직접 가리킬 수 있습니다. 딕셔너리를 요구할 때는 given Ord(a)를 씁니다. 어떤 타입에 대해 둘 이상의 인스턴스가 스코프에 있으면 하나를 canonical로 표시하므로, 암시적 해석이 동전 던지기가 되지 않습니다. 다른 인스턴스는 호출 지점에서 using으로 명시합니다.
instance ordDesc : Ord(Int) {
fn cmp(x, y) = int_cmp(y, x)
}
canonical Ord(Int) = ordInt -- 두 인스턴스가 같은 head를 공유하므로 기본값에 이름을 준다
sort_by_ord(xs) -- canonical Ord(Int)
sort_by_ord(xs, using ordDesc) -- 이것, 역순
신경 쓰고 싶지 않은 인스턴스는 직접 쓰지 않아도 됩니다. 타입 선언 뒤에 deriving 절 하나만 붙이면 지루한 것들은 자동 합성되고, 필드 접근자도 함께 나옵니다.
type Vec2 = Vec2 { x: Int, y: Int } deriving (Eq, Ord, Show, Lens)
with_x(v, 7) -- 파생된 setter, 그리고 v가 유일하면 FBIP 재사용 대상이 된다
클래스는 패턴 매칭에도 관여하는데, 이 부분에서 PL 쪽 사람들은 보통 눈을 번쩍 뜹니다. pattern은 클래스 메서드를 자신의 view로 이름 붙일 수 있고, 그러면 그 하나의 패턴이 인스턴스를 가진 모든 타입을 분해합니다. 메서드 호출과 똑같이 딕셔너리로 디스패치됩니다.
pattern First(n) for Peek = view peek
fn head_or(x : c, d : Int) : Int given Peek(c) =
match x of
First(n) => n
_ => d
First(n)은 Box, Range, 혹은 Peek인 다른 어떤 것과도 매칭되며, head_or는 그 모두에 대해 한 번에 일반화됩니다. 패턴은 그것을 둘러싼 함수만큼 다형적입니다.
어떤 임시적 다형성은 아예 클래스도 필요 없습니다. show는 타입 지향적입니다. 컴파일러가 인자의 정적 타입을 추론하고, 실제 생성자 이름을 바탕으로 구조적 프린터를 합성하며, 필드 안으로 재귀합니다. 인스턴스를 쓸 필요도 없고, 런타임 타입 디스패치도 없습니다. 프린터는 정적 타입에서 monomorphize되므로, 출력 방법을 결정하려고 런타임 태그를 읽을 일도 없습니다.
show(42) -- "42"
show([1, 2, 3]) -- "[1, 2, 3]"
show((7, false)) -- "(7, false)"
show(Node(Leaf, 1, Leaf)) -- "Node(Leaf, 1, Leaf)"
그리고 세 번째 축은 사실 이 글 전체의 진짜 주제입니다. 효과를 조합 가능하게 만드는 바로 그 row 변수가, 효과를 다형적으로도 만듭니다. 다음은 인자를 두 번 호출하고 결과를 더하는 고차 함수입니다. 인자의 효과 row는 변수 e이며, 즉 twice는 f가 무엇을 하든 상관하지 않고, 오직 Int를 반환하기만 하면 됩니다.
fn twice(f : (Unit) -> Int ! {| e}) = f(()) + f(())
{| e}는 “이 row와, 그 밖의 무엇이든”이라는 뜻입니다. 각 호출 지점은 e를 자신이 넘기는 thunk의 실제 row와 unify합니다. 이것이 전부입니다. 하나의 정의가 순수한 인자, 효과가 있는 인자, 그리고 전혀 다른 효과를 가진 인자까지 모두 처리합니다. 오버로드도 없고 래핑도 없습니다.
fn pure_use() =
twice() fn(u)
21
여기서 e는 빈 row {}와 unify합니다. 어떤 효과도 수행되지 않으므로 핸들러가 필요 없고, 결과는 그냥 42입니다. 이제 같은 twice가 효과를 통과시키도록 강제해 보겠습니다.
fn tick_use() =
handle twice(\(u) -> tick(())) with
tick(u, k) => \(n) -> k(n)(n + 1)
return r => \(n) -> r
이 thunk는 Tick을 수행하므로 e는 {Tick}과 unify되고, 바깥 handle은 정확히 그 라벨 하나만 해소합니다. 대신 Say를 수행하는 thunk를 넣으면 e는 {Say}가 됩니다. twice 자체는 전혀 바뀌지 않습니다. 핸들러는 언제나 자신이 원하는 라벨만 이름 붙이고, e는 나머지 모든 것을 조용히 끌고 갑니다. 이것이 이 함수들이 transformer stack 없이도 조합되는 이유입니다.
같은 메커니즘이 세 번 등장한 것입니다. 하나의 정의가 타입에 대해, 딕셔너리에 대해, 그리고 효과에 대해 추상화됩니다.
이쯤 되면 냉소적인 독자(안녕하세요 Hacker News!)는 우아한 추상화에 대해 흔히 하는 질문을 떠올릴 것입니다. 좋다, 그런데 실제 비용은 무엇인가? 대수적 효과에는 평판이 있습니다. 교과서적인 구현은 전체 계산을 free monad로 구체화합니다. “여기 연산 하나가 있고, 그 결과에 대해 무엇을 할지 정하는 함수가 있다”라는 트리입니다. 그런 다음 인터프리터가 그 트리를 걸으며 연산마다 작은 셀 하나를 할당합니다. 아름답지만, yield마다 힙 할당 하나입니다.
Prism은 중요한 경로에서 그렇게 하지 않습니다. 빠른 경로는 Koka 계열의 evidence passing이며, 중요한 차이점만 제 식으로 바꾸었습니다. 계산을 구체화해서 핸들러를 찾아가는 대신, 활성 핸들러 절을 각 연산 지점에 평범한 매개변수로 실어 나릅니다. do op는 직접 호출이 됩니다. 따라서 트리도, 인터프리터 루프도, 셀도 필요 없습니다. 할당은 핸들러를 설치할 때 핸들러당 클로저 하나뿐입니다. 즉 O(operations)가 아니라 O(handlers)입니다. 정확히 한 번 할당된 핸들러 아래에서 yield를 10억 번 수행할 수 있습니다.
물론 free monad는 완전히 사라진 것이 아닙니다. 어떤 패턴은 진짜로 그것이 필요합니다. 데이터 구조로 빠져나가는 계산, 진짜 multishot resumption, masked handler 같은 것들입니다. 하지만 그것은 기본값이 아니라 폴백이며, 컴파일러는 현재 어느 쪽에 속하는지 증명합니다.
이제 이것을 앞의 스트림 파이프라인에 적용해 봅시다.
for n in srange(1, 11).smap(square).skeep(even) do
print(n)
인터프로시저 플로 분석은 함수 경계를 가로질러 각 생산자와 변환기가 정확히 어떤 효과 evidence를 필요로 하는지 계산하고, 그것을 스레딩합니다. 전체 체인은 중간 리스트 0개, 연산당 셀 0개인 단일 루프로 낮아집니다. 본질적으로 Haskell식 stream fusion이지만, Haskell이 올바른 import를 들고 정확한 방향으로 바람이 불며 Mercury가 역행 중일 때만 발동하는 rewrite rule로 성취하는 것, 그리고 Rust가 iterator adapter들을 타입 수준에서 서로에게 monomorphize함으로써 이루는 그것입니다. 여기서는 효과 컴파일러에서 자연스럽게 흘러나옵니다. emit이 알려진 절에 대한 직접 호출이 되는 순간, 절을 생산자 안으로 인라인하는 것은 그냥 인라인이기 때문입니다.
한편 정리는, 앞에서 예고했던 좋은 부분이며, 가비지 컬렉터가 아닙니다. Prism은 Perceus 참조 계수를 사용합니다. 모든 힙 셀은 정적으로 알려진 지점에서 결정론적으로 해제되며, 일시 정지도 없고 tracing도 없습니다. 그리고 여기서 영리한 아이디어는 frame-limited reuse입니다. 패턴 매칭에서 방금 분해한 셀을 화살표 반대편 생성자에게 곧바로 되돌려 주므로, 유일 소유 리스트에 대한 map은 서류상으로는 새 리스트를 반환하는 순수 함수이면서 실제로는 리스트를 제자리에서 바꿉니다. 렌즈 업데이트가 포인터 쓰기로 컴파일되는 것도 같은 메커니즘입니다. fib의 루프가 할당하지 않는 것도 마찬가지입니다. 순수성과 변경은 결국 소유권 분석의 양 끝에서 본 같은 것임이 드러납니다. 이것이 계산의 본질에 대한 깊은 통찰인지, 아니면 아주 평범한 이야기인지는 저도 잘 모르겠습니다.
Perceus 참조 계수가 익숙하게 들린다면, 그래야 합니다. Lean 4가 사용하는 바로 그 메모리 규율이고, 이유도 같습니다. 종속 타입 증명 도우미는 게임 루프 못지않게 GC 정지를 감당할 수 없습니다. Lean은 C로 컴파일하고, 계수를 처리하는 작은 런타임을 링크합니다. Prism도 구조적으로 같은 일을 합니다. 다만 LLVM IR을 내보내고(inkwell을 통해), 같은 프로그램에 대해 텍스트 MLIR 모듈도 내보낸 뒤, 결과를 clang에 넘겨 손으로 쓴 단일 C 런타임 prism_rt.c와 링크합니다. 이 파일은 2천 줄에 조금 못 미칩니다.
그 런타임은 의도적으로 아주 작습니다. 힙 셀은 네 단어 이상, 즉 { refcount, tag, arity, fields... }이고, 파일 전체는 할당기, 컴파일러가 코드 곳곳에 뿌리는 rc_inc/rc_dec 쌍, FBIP 패스가 겨냥하는 제자리 재사용 할당기, 그리고 큰 정수와 문자열 기본 연산으로 이루어져 있습니다. 컬렉터 스레드도 없고, 카드 테이블도 없고, safepoint도 없고, 당신의 코드가 돌고 있지 않을 때 돌아가는 어떤 것도 없습니다. 참조 계수는 런타임이 런타임에 제공하는 서비스가 아닙니다. 컴파일러가 이미 당신의 프로그램 안에 써 넣은 코드이고, C 파일은 그 코드가 호출하는 네다섯 개 연산이 우연히 들어 있는 장소일 뿐입니다.
기본적으로는 평범한 libc malloc에 링크합니다. 벤치마크용으로 선택적 mimalloc 스위치가 있긴 하지만, 전체 논지는 “할당하지 말자”이고, 빠른 할당기는 제거하지 못한 할당을 숨길 뿐입니다. live-cell oracle이 종료 시 힙이 0으로 균형을 이루는지 검사하므로, “garbage free”는 README의 주장이라기보다 테스트 스위트가 확인하는 속성입니다.
인터프리터는 최상단에 Lean 4가 있는 증명 사슬의 맨 아래에 놓여 있습니다. 그것은 CEK 머신, 즉 고전적인 control/environment/continuation 머신을 강화한 친척이며, 그 머신은 Lean 4 모델(models/Prism.lean) 안에 그대로 대응되어 있습니다. 그리고 그 안에는 그 소단계 관계가 결정론적이라는 기계 검증 정리가 들어 있습니다. 프로그램은 정확히 하나의 답으로 진행하며, 흔들릴 여지가 없습니다. 그리고 같은 머신은 Rust 구현으로 내려와 differential oracle 역할도 겸합니다. 코퍼스의 모든 프로그램은 인터프리터와 세 개의 네이티브 백엔드, 즉 LLVM, MLIR, C 링크 바이너리 모두를 거치며, 네 결과가 바이트 단위로 완전히 같지 않으면 빌드는 계속 빨간 상태입니다. 결정론은 위쪽에서 Lean으로 한 번 증명되고, 아래로는 그 증명된 결정론적 머신과 컴파일된 코드가 일치하도록 강제함으로써 기계적으로 유지됩니다.
이 기반이 다음 단계를 가능하게 합니다. 여기서 저는 약간 공상과학 같은 비전을 즐길 수 있습니다. 프로그램이 결정론적임을 증명하고, 읽는 모든 입력을 고정할 수 있다면, 실행을 기록했다가 비트 단위로 재생할 수 있습니다. 이것이 미래 버전으로 구상 중인 재생 가능하고 durable-execution인 Prism의 전제입니다. 여기서는 “충돌 후에도 안전하게 재생 가능하다”가 컴파일러가 검사하는 타입 속성이 됩니다. 되감고, 재부팅을 넘어 이어서 실행하고, 떠났던 것과 정확히 같은 우주에 착지할 것이라 믿을 수 있는 프로그램입니다. 저렴한 결정론 정리 하나로 얻는 시간 여행인 셈입니다.
차등 오라클 역할을 하는 바로 그 인터프리터는 wasm으로 컴파일되므로, 설치 없이 Prism을 입력하고 실행할 수 있는 playground가 있습니다. 프로그램은 worker 안에서 실행되고, 옆의 버튼을 누르면 추론된 타입 시그니처들(효과 row 포함)과 낮아진 코어 IR을 덤프해 주므로, var 루프나 스트림 파이프라인이 실제로 무엇으로 컴파일되는지 직접 볼 수 있습니다. 이 글의 모든 예제는 드롭다운 안에 들어 있습니다. 효과 row를 이것저것 찔러 보세요. 그게 핵심입니다. 전체 소스, Lean 모델, C 런타임은 모두 GitHub의 prism 저장소에 있습니다.
완결성을 위해 덧붙이자면, 여기까지 읽으셨다면 삶의 선택에 꽤 심각한 의문이 있는 것이 분명하니(안녕하세요, 동지여!) 이제 PL 괴짜용 내용을 적겠습니다.
instance ordInt : Ord(Int)), 겹치는 인스턴스를 일관되게 유지하는 canonical 지정, 명시적 override(sort_by_ord(xs, using ordRev)), 그리고 deriving (Eq, Ord, Show).xs.over(f).keep(g).sum()), continuation-passing 코드를 위한 with 문법 설탕, 문자열 보간, 효과 row 별칭.그리고 진짜로 깊이 앓고 계신 분들을 위해, 전체 지적 계보도 적어 두겠습니다. 당연히 수많은 FP 거인들의 연구 위에 서 있지만, Prism 설계에 가장 직접적으로 영감을 준 것들은 다음과 같습니다.
pattern 형태는 view pattern과 GHC의 Pattern Synonyms (2016)을 교차시킨 것입니다.final ctl 핸들러만으로 완전히 복원했습니다.models/Prism.lean)에 대응되어 있고 기계 검증된 결정론 정리를 포함합니다. 세 백엔드는 인터프리터를 differential oracle로 취급함으로써 바이트 단위 동일성을 유지합니다.이 장난감 프로젝트가 감히 논제 같은 것을 가질 수 있다면, 그것은 “순수 함수형”이라는 이름이 사실 언제나 조금 방어적인 표현이었다는 점입니다. 좋은 아이디어의 핵심은 효과가 보이고, 타입이 붙고, 조합 가능해야 한다는 것입니다. 그러려면 효과를 금지할 필요가 없습니다. 추적하면 됩니다. 그리고 정직하게 추적하기 시작하면, 컴파일러는 그것들을 공짜로 만들 만큼 충분한 정보를 얻게 됩니다. 이것이야말로 순수성 서사가 약속해 주지 못했던 부분입니다. 너무 바빠서 IO 모나드와 눈도 못 마주치고 있었기 때문입니다.
이 컴파일러는 본질적으로 2010~20년대의 옛 함수형 프로그래밍 시대에 바치는 저의 연애편지입니다. 그 시절은 훨씬 단순하고 행복한 시간이었습니다. 아니면 ZIRP 시대 청춘의 장밋빛 안경일지도 모르겠지만요. 이 컴파일러는 장난감입니다. 모든 실질적 목적에서 쓸모없고, 아마 트랜스포머 시대 이전 프로그래밍의 어떤 예술품 같은 것에 더 가깝습니다. 우리가 향하는 세상은 이제 이런 것의 자리를 별로 남겨 두지 않습니다. 최대한 확률적이고 우스울 정도로 흥미 없는 Typescript가 점점 더 많은 세계를 돌리고, 우리는 토큰 압출기를 돌보는 사이 경제와 시장은 점점 더 에이전트에 의해 자동화되고 있습니다. 이런 흐름이 저를 조금 슬프게 만들기는 하지만, 그렇다고 이런 종류의 것을 그냥 재미로 만들 수 없다는 뜻은 아닙니다. 그래서 저는 여기서 그걸 했습니다. 함수형 프로그래밍 언어의 미래는 점점 더 틈새적이고 경제적으로는 무관한 무언가가 되어, 그 밑바탕 아이디어의 지적 아름다움을 여전히 사랑하는 소수만의 취미에 가까워질지도 모릅니다. 그래도 저는 만들었습니다. 실제로 돌아가고, 만드는 내내 정말 즐거웠습니다. 어쩌면 이 용감한 소프트웨어 신세계에서는, 그것만으로도 충분할지 모릅니다.