Hacker News Digest

Программа должна оставаться валидной по мере набора.
Python-списковые включения плохи: пока вы не допишете for line in text.splitlines(), редактор не знает тип line, не может подсказать split() и даже не понимает, существует ли переменная.
В Rust text.lines().map(|line| line.split_whitespace()) строится слева-направо: сразу после line. доступны методы, и код всё время «жив».

Принцип progressive disclosure: сложность появляется ровно тогда, когда нужна. В C функции для FILE* начинаются на f; вводишь f и видишь сотни вариантов, не понимая, какой подходит. В идеале file. показал бы read, close и т. д. прямо во время набора.

Python и JS:

map(len, text.split())

— неясно, как называется длина (len, length, size?).

text.split(" ").map(w => w.length)

— length и map подсказываются сразу после точки.

С ростом логики читаемость падает:

len(list(filter(lambda line: all([abs(x) >= 1 and abs(x) <= 3 for x in line]) ...

• Обсуждение крутится вокруг того, что синтаксис многих языков (Python, SQL, JS) не «слева-направо», поэтому автодополнение работает плохо.
• Участники жалуются на право-левый порядок вложенных вызовов f(g(h(x))), хвалят pipe-оператор |> из F#, Rust, OCaml и ждут его в JS/TS.
• Кто-то считает проблему надуманной: мол, надо просто знать язык, а не подстраиваться под автокопмлит.
• Другие предлагают IDE-шаблоны, структурное редактирование или даже использование LLM, чтобы «писать, не думая о синтаксисе».
• В целом спор свёлся к вопросу: оптимизировать ли язык и среду под скорость написания или под читаемость и понимание кода.

Проект «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.

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