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.
Комментарии (24)
- Пользователи хвалят Elaboration Zoo как полезный ресурс для изучения нормализации по вычислению и вывода неявных переменных.
- Просят аналогичный «зоопарк» для линейных типов и предлагают добавить быстрый вариант Hindley–Milner из OCaml.
- Автору советуют включить тёмную тему для блоков кода и рассмотреть простой однонаправленный type-checker в духе Featherweight Java.
- Уточняют, что присутствие индуктивных типов делает реализацию ближе к CIC, но Lean всё же сильнее за счёт аксиомы выбора.
- Картинки с животными вызывают путаницу; большинство считают их просто AI-орнаментом без смысловой нагрузки.