Milner의 Algorithm W부터 현대의 의존 타입 시스템까지, 50년에 걸친 타입 이론 연구를 아우르는 네 가지 문서화된 Rust 구현을 소개한다.
재미있는 사이드 프로젝트로, 저는 타입 이론 연구 50년을 가로지르는 네 가지 문서화된(literate) Rust 구현을 만들었습니다. Milner의 Algorithm W부터 현대의 의존 타입 시스템까지를 포함합니다. 각 구현은 코드 전반에 걸친 자세한 설명과 주석을 통해 가능한 한 읽기 쉽고 이해하기 쉽도록 만들었고, 또한 가능한 한 간결하고 짧게 만들어서, 람다 큐브 어딘가에 있는 어떤 종류의 시스템이든 구축할 때 출발점으로 여러분의 프로젝트에 그대로 가져다 쓸 수 있도록 했습니다.
-동물원이니, 각각을 대표하는 귀여운 동물 마스코트도 붙였습니다:
 | Algorithm W (Hindley-Milner 타입 시스템) 구조적 재귀를 사용해 Milner의 1978년 단일화 기반 타입 추론을 구현합니다. 알고리즘은 표현식을 순회하는 동안 타입 변수들 사이의 제약을 생성한 뒤, Robinson의 단일화 알고리즘으로 이 제약들을 풉니다. 명시적 타입 애노테이션 없이도 랭크-1 다형적 타입 추론을 가능하게 하는 let-다형성을 제공합니다. 구현은 고전적인 occurs check 처리와 타입 환경을 통한 치환 전파를 보여줍니다. 참고: Robin Milner의 A Theory of Type Polymorphism in Programming. PDF |
 | System F (2차 람다 대수) 양방향 타입 검사를 사용한 매개변수적 다형성을 갖는 2차 람다 대수. 전칭 양화를 갖는 System F를 위해 Dunfield-Krishnaswami 알고리즘을 구현한 양방향 타입 체커입니다. 타입 검사를 합성(⇒)과 검사(⇐) 모드로 분리하여, 존재 변수 해를 구하는 방식으로 다형적 타입 추론을 가능하게 합니다. 타입 변수 스코핑을 위한 신중한 문맥 관리를 통해 전칭 타입()으로 매개변수적 다형성을 처리합니다. 존재 변수 및 다형 타입 사이의 서브타이핑 관계에 대해 포괄적인 제약 해결을 포함합니다. 참고: Dunfield와 Krishnaswami의 Complete and Easy Bidirectional Typechecking for Higher-rank Polymorphism. PDF |
 | System F-ω (고차 종(kind) 다형성) 미니어처 Haskell-lite. 타입 생성자와 kind 검사를 추가하여 System F를 확장하고, 대수적 데이터 타입과 함께 고랭크 다형성을 구현합니다. 타입 추론과 함께 kind 추론을 제공하며, 타입 수준과 kind 수준 환경을 모두 관리합니다. 타입 생성자 적용과 다형적 kind 할당을 지원합니다. 고차 kind 단일화 문제에 대한 제약 생성을 구현하여, kind 시스템이 잘못된 타입 적용을 어떻게 방지하는지 보여줍니다. 고차 kind 타입, DK 양방향 타입 검사, 존재 타입 변수, 다형적 생성자 적용, 패턴 매칭, 그리고 타입 추론이 있는 람다 표현식을 포함한 System F-ω의 완전한 구현입니다. 참고: Joshua Dunfield의 A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference. PDF |
 | Calculus of Constructions (의존 타입) 비누적(non-cumulative) 유니버스 계층과 귀납 타입을 갖는 Calculus of Constructions. 타입과 항을 통합하는 완전한 의존 타입 시스템으로, 제약 기반 추론을 통한 유니버스 다형성을 구현합니다. 귀납 타입 정의, 의존 함수 타입(Pi 타입, Sigma 타입), 그리고 유니버스 다형성을 갖습니다. Miller 패턴 기법을 사용해 고차 단일화 문제를 부분적으로 해결하기 위한 메타-변수 해법을 사용합니다. 참고: Vladimir Voevodsky의 A universe polymorphic type system. PDF |
예제들은 전체 파서와 테스트 스위트(다만 평가기는 없음)를 갖춘, 꽤 관용적인 Rust로 구현되어 있으며 larlpop, logos, ariande 등의 일반적인 컴파일러 라이브러리를 사용합니다. 이들은 전체 구현의 분명 단순화되고 코드 골프된 버전이어서 쉽게 이해하고 수정할 수 있습니다. 하지만 Haskell이나 Coq 타입체커를 읽어보려는 시도(각각 쉽게 100k+ LOC)에 비하면 훨씬 더 이해하기 쉬울 것입니다. 언어에 관심을 갖기 시작한 젊은 열정가들에게 도움이 되기를 바랍니다. 제가 10년 전에 이런 주제를 배울 때 이 자료가 있었더라면 좋았을 텐데, 그래서 다른 사람들이 그렇게 고생하지 않도록 제가 원하던 리소스를 직접 만들기로 했습니다!
