Typechecker Zoo
Проект «Zoo» — мини-реализации самых влиятельных статических систем типов последних 50 лет. Начнём с простых и дойдём до зависимых типов. Всё пишем на Rust — просто потому что удобно и забавно строить чисто функциональные языки на не-функциональном.
Это не учебник, а выходные развлечение. За теорией и доказательствами смотрите TAPL, ATTAPL, PFPL и оригинальные статьи (ссылки в приложении). Здесь же — грязные детали реализации: структуры данных, AST, логика, всё, что можно осилить за уик-энд.
Код — идиоматичный Rust с полноценным парсером и тестами (lalrpop, logos, ariadne). Примеры урезаны, но понятнее продакшен-реализаций. Парсинг и MLIR считаем решёнными задачами, поэтому не фокусируемся на них.
Четыре «зверька»:
- Algorithm W (775 строк) — классический Hindley–Milner, полиморфный λ-исчисление.
- System F (1090 строк) — второе λ-исчисление, параметрический полиморфизм, Mini-OCaml.
- System F-ω (3196 строк) — высшие рода, паттерн-матчинг, дататипы, Haskell-lite.
- Calculus of Constructions (6000 строк) — иерархия универсумов, индуктивные типы, крошечный Lean.
MIT-лицензия, хобби-проект. Нашли опечатку — присылайте pull-request.