Prism: 타입 지정 효과를 갖춘 비순수 함수형 언어

 (stephendiehl.com)
1P by GN⁺ | ★ favorite | 댓글 1개
  • Prism은 가변 변수, 예외, 스트림 같은 효과를 숨기지 않고 타입에 드러내면서도, 외부에 관찰되지 않는 지역 변경은 Int -> Int 같은 순수 타입으로 유지하는 실험적 컴파일러임
  • 핵심은 대수적 효과 핸들러와 행 다형성(row polymorphism)으로, 효과가 함수 타입의 행에 합쳐지고 핸들러는 필요한 라벨만 처리한 뒤 나머지를 전달함
  • 같은 효과 시스템이 예외, 제너레이터/스트림, 렌즈, var 상태, fail/guard 흐름을 표현하며, 일부 경로는 중간 리스트나 런타임 합성 없이 낮아짐
  • 성능 쪽은 evidence passing과 Perceus 참조 카운팅을 결합해 효과 호출당 할당을 피하고, 고유 소유 값의 함수형 갱신을 제자리 변경으로 최적화함
  • Prism은 LLVM IR, MLIR, C 런타임, Rust 인터프리터, Lean 4 모델, WASM 플레이그라운드를 함께 제공해 타입 추론과 lowering 결과를 직접 확인할 수 있음

외부에 보이지 않는 변경과 타입 지정 효과

  • Prism의 출발점은 내부에서 var와 대입을 쓰는 fib 함수도 외부 관찰자에게는 순수 함수처럼 보일 수 있다는 점임
    • 예시 fib는 두 변수를 제자리에서 갱신하지만 함수 밖으로 상태를 노출하지 않음
    • 타입은 Int -> Int이며, 효과가 타입에 나타나지 않음
  • Prism은 지난 3년간 개발된 개념 증명 함수형 컴파일러로, OCaml 5, Haskell, Koka 계열의 현대 타입 아이디어를 바탕으로 효과를 모델링함
  • 핵심 방향은 효과를 피하는 것이 아니라, 효과를 타입 시스템에 넣고 컴파일러가 비용을 없애도록 최적화하는 데 있음

효과는 인터페이스처럼 동작함

  • Prism의 효과는 연산을 선언하고, 핸들러가 그 연산의 의미를 부여하는 대수적 효과 핸들러 방식임
    • effect Gen { ctl yield(Int) : Unit }는 yield 연산을 선언함
    • fn produce(n) : !{Gen} Unit의 !{Gen}은 함수가 yield를 수행한다는 사실을 타입에 표시함
  • 같은 생산자라도 continuation인 k를 어떻게 다루느냐에 따라 다른 의미로 해석됨
    • total은 yield 값을 더함
    • count는 yield 횟수를 셈
    • k를 버리면 예외, 한 번 호출하면 상태나 제너레이터, 여러 번 호출하면 탐색 동작이 됨
  • Amb 효과 예시는 choose와 reject로 피타고라스 삼쌍 탐색을 표현함
    • choose(n)은 0..n-1 범위 값을 제공함
    • 핸들러는 후보마다 같은 continuation을 재개해 탐색 트리를 만듦
  • OCaml 5와 달리 Prism은 효과를 타입에 포함하며, Haskell의 모나드 트랜스포머 스택처럼 계층을 수동으로 올릴 필요가 없음
    • 효과 행은 호출을 거치며 구조적으로 합쳐짐
    • 스택이 아니라 라벨의 집합처럼 동작함

하나의 메커니즘으로 표현되는 기능들

  • 예외

    • Prism에서 예외는 continuation을 버리는 핸들러임
    • final ctl 절은 k를 폐기하고 해당 본문 값을 핸들러 결과로 삼음
    • Result를 전파하거나 호출 스택에 ?를 흩뿌리는 방식이 아님
    • 예외는 효과 행의 라벨이므로 확장 가능한 예외로 합성됨
    • 각 실패는 별도 연산이며, 함수 타입의 행은 밖으로 빠져나갈 수 있는 예외를 표시함
    • Abort와 Timeout 예시에서 fetch는 !{Abort, Timeout}을 가짐
    • with_default는 Timeout만 처리해 fallback "cached"를 반환하고, 처리 후 타입에는 !{Abort}만 남음
    • Java의 checked exception과 달리 클래스 계층에 묶이지 않고 열린 구조적 집합으로 동작함

  • 제너레이터와 스트림

    • 스트림은 emit을 수행하는 생산자, 이를 잡아 다시 내보내는 변환자, fold하는 소비자로 구성됨
    • 파이프라인은 하나의 생산자 주변에 핸들러를 중첩한 형태라서 중간 리스트가 구조적으로 생기지 않음
    • 예시: srange(1, n).smap(square).skeep(even).stake(5).ssum()
    • stake(5) 같은 조기 중단은 필요한 값을 얻은 뒤 continuation을 버리는 핸들러임
    • 스트림 라이브러리는 Haskell의 pipes와 conduit에서 영향을 받음

  • 렌즈

    • Prism의 렌즈는 별도 라이브러리가 아니라 레코드 갱신 경로와 메모리 모델의 조합임
    • 중첩 레코드에서 하나의 경로 표현식으로 깊은 필드를 여러 개 갱신할 수 있음
    • 예시: { g | player.pos.x = 30, player.hp = 95, score = 110 }
    • 중첩 레코드의 spine을 다시 만들되, 값이 고유하게 소유된 경우 분해한 셀을 재사용함
    • 이 구조 덕분에 함수형 갱신이 포인터 쓰기로 컴파일될 수 있음
    • 런타임에 optic 타입을 할당하거나 합성하지 않음
    • deriving (Lens)는 score_of, with_score 같은 평범한 함수 접근자를 만들어줌

  • 가변 상태

    • var는 private effect의 get/set 연산으로 desugar됨
    • 블록 끝에 설치된 핸들러가 이 효과를 처리함
    • 클로저 탈출 분석은 상태가 밖으로 빠져나가는 경우를 거부함
    • enclosing 함수는 빈 효과 행을 유지할 수 있음

  • 실패

    • 실패는 익명 Fail 효과로 표현되며, “이 표현식이 값을 만들지 못할 수 있음”을 타입 시스템이 다룸
    • fail()은 실패를 수행하고, guard(cond)는 조건이 거짓일 때 실패함
    • ??는 왼쪽이 실패할 때 fallback을 사용함
    • ?.는 옵션 체인을 따라가다 짧게 중단함
    • comprehension guard는 실패한 원소를 crash 대신 가지치기함
    • var도 핸들러 sugar이므로 transact 블록은 live 변수를 스냅샷하고 실패 시 롤백할 수 있음

현대적 타입 기능

  • Prism은 대부분의 코드에서 타입 서명을 적지 않아도 되도록 Dunfield-Krishnaswami 계열의 bidirectional higher-rank 타입 추론을 사용함
  • 고차 다형성이 필요한 경계에서는 forall로 바인더를 명시함
    • pick(g : forall a. (a) -> a)는 g를 Bool과 Int에 모두 적용할 수 있음
    • Damas-Milner core라면 첫 호출에서 a가 Bool로 통합되어 두 번째 호출이 거부될 상황임
  • 임시 다형성은 Lean 스타일의 타입 클래스로 표현됨
    • 인스턴스는 이름 있는 값임
    • given Ord(a)는 딕셔너리를 요구함
    • 여러 인스턴스가 있을 때는 하나를 canonical로 표시하고, 다른 것은 using으로 명시함
  • deriving은 Eq, Ord, Show, Lens 같은 반복적인 인스턴스와 필드 접근자를 생성함
  • 패턴 매칭도 클래스와 연결됨
    • pattern First(n) for Peek = view peek는 클래스 메서드를 view로 쓰는 패턴임
    • head_or는 Peek 인스턴스가 있는 여러 타입에 대해 같은 패턴을 사용할 수 있음
  • show는 별도 클래스 없이 타입 지향으로 동작함
    • 컴파일러가 정적 타입에서 구조적 printer를 합성함
    • 런타임 타입 태그를 읽어 출력 방식을 결정하지 않음
  • 효과 행도 다형적임
    • fn twice(f : (Unit) -> Int ! {| e})는 인자로 받은 함수의 효과 행 e가 무엇이든 결과를 더함
    • 순수 thunk에서는 e가 빈 행 {}와 통합됨
    • Tick이나 Say 같은 효과를 수행하는 thunk에서는 해당 행을 그대로 전달함

효과 비용을 줄이는 컴파일 방식

  • 교과서적 대수적 효과 구현은 계산을 free monad 형태의 트리로 재구성하고, 연산마다 작은 셀을 할당할 수 있음
  • Prism의 빠른 경로는 Koka 계열의 evidence passing임
    • 계산을 재구성해 핸들러를 찾는 대신, 활성 핸들러 절을 일반 매개변수처럼 각 연산 지점에 전달함
    • do op는 직접 호출로 낮아짐
    • 핸들러 설치 시 클로저 하나만 할당하므로 비용은 O(handlers)이고, 연산 횟수에 비례하지 않음
  • free monad 인코딩은 fallback으로 남아 있음
    • 데이터 구조로 빠져나가는 계산
    • 진정한 multishot resumption
    • masked handler 같은 패턴이 대상임
  • 스트림 파이프라인은 interprocedural flow analysis로 필요한 effect evidence를 함수 경계 너머까지 계산함
    • 생산자와 변환자에 evidence를 스레딩함
    • 전체 체인은 단일 루프로 낮아짐
    • 중간 리스트와 연산당 셀 할당이 없음
  • 이 방식은 Haskell의 stream fusion이나 Rust iterator adapter의 단일화와 비슷한 결과를 효과 컴파일러에서 얻는 구조임

메모리 모델과 런타임

  • Prism은 Perceus 참조 카운팅을 사용함
    • 힙 셀은 정적으로 알려진 지점에서 결정적으로 해제됨
    • pause나 tracing이 없음
  • frame-limited reuse는 패턴 매치로 방금 분해한 셀을 생성자 쪽에 다시 넘김
    • 고유 소유 리스트에 대한 map은 새 리스트를 반환하는 순수 함수처럼 보이지만 실제로는 제자리 변경될 수 있음
    • 렌즈 갱신이 포인터 쓰기로 컴파일되는 것도 같은 메커니즘임
  • 런타임 구조는 Lean 4의 메모리 규율과 유사하지만, Prism은 LLVM IR을 방출함
    • LLVM IR은 inkwell을 통해 생성됨
    • 같은 프로그램에 대해 텍스트 MLIR 모듈도 생성함
    • 결과는 clang으로 손으로 작성한 C 런타임 prism_rt.c와 링크됨
  • prism_rt.c는 약 2천 줄 규모의 작은 런타임임
    • 힙 셀은 { refcount, tag, arity, fields... } 형태의 4개 이상 word 구조임
    • allocator, rc_inc/rc_dec, 제자리 재사용 allocator, bignum과 문자열 primitive가 포함됨
    • collector thread, card table, safepoint가 없음
  • 기본 allocator는 libc malloc이며, 벤치마킹용 opt-in mimalloc 설정이 있음
  • live-cell oracle은 종료 시 heap balance가 0인지 assert해 테스트 스위트가 garbage-free 속성을 확인함

Lean 모델과 백엔드 검증

  • Prism 인터프리터는 CEK machine 계열이며, 이 기계는 Lean 4 모델 models/Prism.lean에 반영됨
  • Lean 4 모델은 small-step relation이 결정적이라는 기계 검증 정리를 가짐
    • 프로그램은 정확히 하나의 다음 상태로 진행함
  • Rust 구현의 인터프리터는 differential oracle로도 사용됨
    • corpus의 모든 프로그램은 인터프리터와 LLVM, MLIR, C-linked binary 백엔드를 모두 통과함
    • 네 결과의 출력이 byte-identical해야 빌드가 통과함
  • 결정성은 replayable durable execution의 기반이 됨
    • 입력을 고정하고 실행을 기록하면 bit-for-bit 재생이 가능하다는 구상임
    • 향후 버전에서는 crash 이후 replay 안전성을 타입 속성으로 검사하는 Prism이 그려져 있음

WASM 플레이그라운드와 소스

  • 같은 인터프리터는 WASM으로 컴파일되어 playground에서 설치 없이 Prism 코드를 실행할 수 있음
  • 플레이그라운드는 worker에서 프로그램을 실행함
  • 버튼으로 추론된 타입 서명, effect row, lowered core IR을 덤프할 수 있음
    • var 루프나 스트림 파이프라인이 실제로 어떤 형태로 낮아지는지 볼 수 있음
  • 본문의 예제는 dropdown에 포함됨
  • 전체 소스, Lean 모델, C 런타임은 prism repository on GitHub에 있음

구현 계보와 프로젝트 성격

함께 보면 좋은 글 β

GN⁺   [-]
Lobste.rs 의견들

  • 렌즈가 효과와 무슨 관련이 있는지 모르겠음. 글에서 렌즈를 언급할 때마다 “한 가지 트릭을 다섯 방식으로” 아래에 묶인 것 말고는 서로 무관해 보임
    그리고 tick_use()가 대체 뭘 하려는 건지도 모르겠음. 독자가 설명 없이 이렇게 꼬인 예제를 이해하길 기대하는 건가? 타입 주석이 있었으면 도움이 됐을 듯

    • 렌즈에 대해서는 여기서 더 설명함: https://sdiehl.github.io/prism/spec.html#86-optic-paths
      그래도 은유적인 수준 말고는 렌즈가 효과와 무슨 관련이 있는지 잘 안 보임. 저자는 이렇게 씀:

      This is the language’s “effects instead of monads” stance applied to optics, paths instead of optic combinators.
      즉 은유는 이렇다고 봄: 모나드는 값이지만 효과는 값이 아니라 일종의 제어 구조임. 마찬가지로 렌즈는 값이지만 Prism의 optic paths는 값이 아니라, 하드코딩된 문법을 가진 제어 구조에 가까움

  • 더 시간을 들여 이해해야겠지만, 정말 아름다워 보임

  • 정말 인상적임. 오히려 그래서 Diehl이 글 끝에서 컴파일러를 장난감이라고 부르는 이유가 궁금함. 새로운 수준의 우아함을 보여주는 성공적인 개념 증명처럼 보임

  • call-by-push-value 중간 표현이 실제로 어떻게 생겼는지 더 자세히 보고 싶음. 특히 합류 지점(join point)을 처리하는지가 궁금함
    CBPV에 효과를 붙이는 이론을 다룬 논문들은 있었음. 계산에는 효과 타입이 있고 값에는 없다고 말하는 건 꽤 자연스럽지만, Koka의 증거 전달에 바로 적용할 만큼 구체화된 건 보지 못해서 흥미로움
    전반적으로 Koka와 비교해 어떤 위치인지 알고 싶음. FBIP, Perceus, 증거 전달을 보면 Koka 작업에서 강하게 영감을 받은 게 분명하고, 동시에 중간 표현에 CBPV를 쓰니 확실히 다르기도 함. 다만 얼마나 다른지는 잘 보이지 않음

  • 내가 계속 시간 내서 만들어보려던 것과 많이 닮아 보임. 좋다!

  • 주제에서 살짝 벗어나지만, Stephen의 “write you a haskell” 프로젝트가 몇 년 전 멈춘 게 늘 좀 아쉬웠음. Prism에 대해서는 튜토리얼급 구현 설명이 나오면 좋겠음

  • 이 언어에서 무엇이 “불순”한지 궁금함. 그 단어는 제목에만 나오고 본문에는 다시 안 나옴
    모든 효과가 추적되는 것처럼 보이니, 효과가 없는 함수는 여전히 수학적 함수임. 뭔가 놓친 건가?

    • 주어진 fib 정의처럼 함수 정의 안에서 지역 가변 변수를 쓰는 것과 관련 있어 보임. var x는 불순한 가변 변수이고, let x는 순수한 불변 변수임

  • 보통 언어의 기능으로 다뤄지던 것들, 예를 들어 X 언어의 yield, Y 언어의 throw 같은 것을 또 하나의 인터페이스로 구현했다는 점이 정말 멋짐
    부작용, 예외, 연속 같은 여러 제어 흐름을 하나의 추상화 위에 만들 수 있다는 건 설계 질문 전체를 새롭게 보는 흥미로운 방식이고, 더 많은 탐색과 혁신을 돕거나 자극하길 기대함. 앞으로도 영감을 얻으러 여러 해 동안 다시 보게 될 것 같음

답변달기