Typechecker Zoo
재미 삼아 진행한 사이드 프로젝트로, Milner의 W 알고리즘(Algorithm W)부터 현대의 의존 타입 시스템에 이르기까지 50년에 걸친 타입 이론 연구를 아우르는 리터러트(literate) Rust 구현 네 가지를 만들었습니다. 각 구현은 코드 전반에 걸친 상세한 설명과 주석을 곁들여 최대한 읽기 쉽고 이해하기 쉽게 만들고자 했으며, 또한 람다 큐브 위 어딘가에 놓이는 어떤 종류의 시스템이든 만들 때 출발점으로 삼아 여러분의 프로젝트에 가져다 쓸 수 있도록 최대한 간결하고 짧게 만들고자 했습니다.
- Github 저장소 | 문서
-동물원이니만큼, 각 구현마다 이를 대표하는 귀여운 동물 마스코트도 붙여 주었습니다:
 |
W 알고리즘(Algorithm W, Hindley-Milner 타입 시스템) 구조적 재귀를 사용하여 Milner가 1978년에 제시한 단일화 기반 타입 추론을 구현합니다. 이 알고리즘은 식을 순회하는 동안 타입 변수들 사이의 제약을 생성한 다음, Robinson의 단일화 알고리즘으로 이 제약들을 풉니다. 명시적인 타입 표기 없이도 랭크-1 다형 타입 추론을 가능하게 하는 let-다형성을 갖추고 있습니다. 이 구현은 고전적인 occurs check 처리와 타입 환경을 통한 치환 전파를 보여 줍니다. 참고 문헌: 프로그래밍에서의 타입 다형성 이론(A Theory of Type Polymorphism in Programming) 저자: Robin Milner. |
 |
System F (2차 람다 대수) 양방향 타입 검사를 사용하는, 매개변수 다형성을 갖춘 2차 람다 대수입니다. 전칭 양화를 갖춘 System F를 위해 Dunfield-Krishnaswami 알고리즘을 구현한 양방향 타입 검사기입니다. 타입 검사를 합성(⇒) 모드와 검사(⇐) 모드로 나누어, 존재 변수 풀이를 통한 다형 타입 추론을 가능하게 합니다. 전칭 타입(∀α. τ)을 통해 매개변수 다형성을 처리하며, 타입 변수의 스코프를 위해 컨텍스트를 세심하게 관리합니다. 존재 변수에 대한 포괄적인 제약 풀이와 다형 타입 사이의 서브타이핑 관계를 포함합니다. 참고 문헌: 고계 다형성을 위한 완전하고 쉬운 양방향 타입 검사(Complete and Easy Bidirectional Typechecking for Higher-rank Polymorphism) 저자: Dunfield, Krishnaswami. |
 |
System F-ω (고차 카인드 다형성) 축소판 Haskell-lite입니다. System F에 타입 생성자와 카인드 검사를 더해 확장하며, 대수적 데이터 타입과 함께 고랭크 다형성을 구현합니다. 타입 추론과 더불어 카인드 추론을 갖추고 있으며, 타입 수준 환경과 카인드 수준 환경을 모두 관리합니다. 타입 생성자 적용과 다형 카인드 할당을 지원합니다. 고차 카인드 단일화 문제를 위한 제약 생성을 구현하여, 카인드 시스템이 잘못된 형태의 타입 적용을 어떻게 막는지 보여 줍니다. 고차 카인드 타입, DK 양방향 타입 검사, 존재 타입 변수, 다형 생성자 적용, 패턴 매칭, 타입 추론을 갖춘 람다 식을 포함하는 System F-ω의 완전한 구현입니다. 참고 문헌: 고계 다형 타입 추론의 기계적 형식화 Joshua Dunfield 저. |
 |
구성의 계산 (의존 타입) 비누적 유니버스 계층과 귀납 타입을 갖춘 구성의 계산입니다. 타입과 항을 하나로 통합하는 완전한 의존 타입 시스템으로, 제약 기반 추론을 통해 유니버스 다형성을 구현합니다. 귀납 타입 정의, 의존 함수 타입(Pi 타입, Sigma 타입), 유니버스 다형성을 갖추고 있습니다. Miller 패턴 기법을 사용하여 고차 단일화 문제를 부분적으로 해결하기 위해 메타 변수 풀이를 사용합니다. 참고 문헌: 유니버스 다형적 타입 시스템 Vladimir Voevodsky 저. |
예제들은 larlpop, logos, ariande 등 일반적인 컴파일러 라이브러리를 사용하여 상당히 관용적인 Rust로 구현되어 있으며, 완전한 파서와 테스트 스위트를 갖추고 있습니다(다만 평가기는 없습니다). 쉽게 이해하고 수정할 수 있도록 전체 구현을 단순화하고 코드 골프 방식으로 압축한 버전임은 분명합니다. 그래도 각각 10만 줄이 훌쩍 넘는 Haskell이나 Coq의 타입 검사기를 읽으려고 애쓰는 것보다는 훨씬 더 이해하기 쉬울 것입니다. 이제 막 언어에 관심을 키워 가는 젊은 애호가들에게 도움이 되기를 바랍니다. 10년 전 이 주제들을 공부할 때 이런 자료가 있었다면 좋았겠다는 생각이 들어, 다른 사람들이 그렇게까지 고생하지 않도록 제가 원했을 법한 자료를 직접 만들어 보기로 했습니다!