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

> Clean Markdown view of GeekNews topic #30911. Use the original source for factual precision when an external source URL is present.

## Metadata

- GeekNews HTML: [https://news.hada.io/topic?id=30911](https://news.hada.io/topic?id=30911)
- GeekNews Markdown: [https://news.hada.io/topic/30911.md](https://news.hada.io/topic/30911.md)
- Type: GN+
- Author: [neo](https://news.hada.io/@neo)
- Published: 2026-06-29T00:12:51+09:00
- Updated: 2026-06-29T00:12:51+09:00
- Original source: [stephendiehl.com](https://www.stephendiehl.com/posts/prism/)
- Points: 1
- Comments: 1

## Topic Body

- **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](https://hackage.haskell.org/package/pipes)와 [conduit](https://hackage.haskell.org/package/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](https://sdiehl.github.io/prism/)에서 설치 없이 Prism 코드를 실행할 수 있음
- 플레이그라운드는 worker에서 프로그램을 실행함
- 버튼으로 추론된 타입 서명, effect row, lowered core IR을 덤프할 수 있음
  - `var` 루프나 스트림 파이프라인이 실제로 어떤 형태로 낮아지는지 볼 수 있음
- 본문의 예제는 dropdown에 포함됨
- 전체 소스, Lean 모델, C 런타임은 [prism repository on GitHub](https://github.com/sdiehl/prism)에 있음

### 구현 계보와 프로젝트 성격
- Prism의 core IR은 Levy의 [*Call-by-Push-Value: A Functional/Imperative Synthesis*](https://scholar.google.com/scholar?q=Call-by-Push-Value+A+Functional+Imperative+Synthesis)에 기반한 call-by-push-value 계열임
- 빠른 효과 경로는 Xie와 Leijen의 [*Generalized Evidence Passing for Effect Handlers*](https://scholar.google.com/scholar?q=Generalized+Evidence+Passing+for+Effect+Handlers), [*Effect Handlers, Evidently*](https://scholar.google.com/scholar?q=Effect+Handlers+Evidently)에 가까움
- 메모리 모델은 [*Perceus: Garbage Free Reference Counting with Reuse*](https://scholar.google.com/scholar?q=Perceus+Garbage+Free+Reference+Counting+with+Reuse), [*Reference Counting with Frame-Limited Reuse*](https://scholar.google.com/scholar?q=Reference+Counting+with+Frame-Limited+Reuse), [*FP^2: Fully in-Place Functional Programming*](https://scholar.google.com/scholar?q=FP2+Fully+in-Place+Functional+Programming)에 기반함
- 효과 행은 row polymorphism과 scoped labels 계열이며, 핸들러는 Plotkin과 Pretnar의 [*Handlers of Algebraic Effects*](https://scholar.google.com/scholar?q=Handlers+of+Algebraic+Effects)를 Eff와 Koka를 거쳐 받아들인 형태임
- 패턴 매칭은 decision tree와 usefulness matrix 기반이며, `pattern` 형식은 view pattern과 GHC의 [*Pattern Synonyms*](https://scholar.google.com/scholar?q=Pattern+Synonyms+Haskell)의 조합임
- 실패 계층은 [*The Verse Calculus*](https://scholar.google.com/scholar?q=The+Verse+Calculus+A+Core+Calculus+for+Deterministic+Functional+Logic+Programming)를 `final ctl` 핸들러로 회수한 형태임
- Prism의 방향은 “순수 함수형”보다 **효과를 보이게 하고, 타입화하고, 합성 가능하게 추적하는 것**에 가까움
- 프로젝트 자체는 실용 도구라기보다 장난감이자 예술적 작업에 가까우며, 함수형 프로그래밍 아이디어의 지적 아름다움을 위해 만든 컴파일러로 정리됨

## Comments



### Comment 60617

- Author: neo
- Created: 2026-06-29T00:12:52+09:00
- Points: 1

###### [Lobste.rs 의견들](https://lobste.rs/s/bgnc5q/prism_impure_functional_language_with) 
- 렌즈가 효과와 무슨 관련이 있는지 모르겠음. 글에서 렌즈를 언급할 때마다 “한 가지 트릭을 다섯 방식으로” 아래에 묶인 것 말고는 서로 무관해 보임  
  그리고 `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](https://github.com/sdiehl/write-you-a-haskell)” 프로젝트가 몇 년 전 멈춘 게 늘 좀 아쉬웠음. Prism에 대해서는 **튜토리얼급 구현 설명**이 나오면 좋겠음

- 이 언어에서 무엇이 “불순”한지 궁금함. 그 단어는 제목에만 나오고 본문에는 다시 안 나옴  
  모든 효과가 추적되는 것처럼 보이니, 효과가 없는 함수는 여전히 수학적 함수임. 뭔가 놓친 건가?
  - 주어진 `fib` 정의처럼 함수 정의 안에서 **지역 가변 변수**를 쓰는 것과 관련 있어 보임. `var x`는 불순한 가변 변수이고, `let x`는 순수한 불변 변수임

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