Hacker News Digest

Кандидат на собеседовании решает задачу FizzBuzz с помощью комбинаторной логики и лямбда-исчисления в JavaScript, используя лишь базовые комбинаторы S, K и I. Интервьюер всё больше недоумевает, наблюдая, как соискатель последовательно реализует сложнейшие математические операции и структуры данных через композицию этих комбинаторов, включая числа Чёрча, арифметические операции и даже Y-комбинатор для рекурсии.

Кандидат оправдывает свой подход тем, что "JavaScript слишком раздут", и переключается на "ленивый" вариант JavaScript под названием Skoobert, чтобы избежать переполнения стека. В итоге он реализует всё необходимое для FizzBuzz — от сложения и вычитания до списков и операций над ними — исключительно через комбинаторы, демонстрируя глубокое, но совершенно не практичное знание теоретических основ программирования.

• Обсуждение началось с критики формата технического собеседования, где кандидат вместо решения задачи пишет «рассказ о лямбда-исчислении» и тем самым «проходит» тест.
• Дискуссия быстро перешла к тому, что автор статьи, возможно, сам не до конца понял, что именно он хотел показать читателям, и что именно они должны вынести из этого урока.
• Участники треда начали спорить о том, насколько полезно знание комбинаторной логики в повседневной работе программиста, и стоит ли вообще изучать её.
• Некоторые комментаторы отметили, что статья не дала никакого практического обоснования, почему стоит изучать эту тему.
• В итоге, обсуждение сошлось на то, что если кто-то и найдёт в этом какой-то практический смысл, то это будет уже его заслуга, а не автора статьи.

Конструктивная теория типов объединяет логику и программирование в единую систему, где разработка и верификация программ происходят одновременно. Она представляет собой функциональный язык с уникальными чертами: тотальностью функций, зависимыми типами, позволяющими тип результата определять значением аргумента, а также продвинутыми модулями с логическими утверждениями в интерфейсах. Программы можно извлекать непосредственно из доказательств, что открывает возможности для автоматизированного создания корректного кода.

Книга служит введением и углублённым курсом, начиная с основ логики, λ-исчисления и функционального программирования, затем детально представляет систему теории типов с примерами. Она также критически анализирует предложения по расширению системы, такие как подавление свидетельствующей информации в подтипах или добавление коиндуктивных типов для работы с бесконечными потоками, сохраняя при этом свойства завершаемости. Практическая реализация системы помогла прояснить тонкие аспекты, например роль предположений.

• Обсуждается перспектива широкого внедрения функционального программирования благодаря его теоретической основе, аналогично устойчивости реляционных баз данных и SQL.
• Поднимается вопрос о применении теории типов в императивных языках, с примерами из Rust и C++, где типы улучшают безопасность и выразительность.
• Высказывается критика функционального программирования как сложного и непрактичного, порождающего "ужасный код", в противовес его восприятию как более безопасного и элегантного.
• Участники делятся рекомендациями по литературе для изучения темы (TTOP, Types and Programming Languages) и отмечают её сложность, но ценность.
• Отмечается, что чистые функциональные языки непопулярны (TIOBE), но их идеи (лямбды, монады) проникают в мейнстрим (например, для асинхронного программирования).

Лямбда-исчисление — это минималистичный формализм для представления функций и их применения, основанный на двух ключевых операциях: абстракции (создание функции через λx.M) и аппликации (применение функции к аргументу, записывается как MN). Его синтаксис крайне лаконичен, но он позволяет выражать любые вычисления через правила подстановки.

Центральное правило — β-редукция: (λx.M)N сводится к M[x:=N], то есть замене всех вхождений x в M на N. Это отражает идею вычисления через подстановку аргумента. Например, (λx.x²−2x+5)2 даёт 2²−2·2+5=5. Важно, что функции здесь трактуются не как множества пар, а как правила преобразования, что делает теорию неэкстенсиональной.

Лямбда-исчисление легло в основу теории вычислений, логики и программирования, демонстрируя, как простые синтаксические правила могут порождать богатую семантику. Оно показывает, что даже в такой скудной нотации можно выразить всю вычислимую математику.

• Обсуждаются различные подходы к изучению и объяснению λ-исчисления, включая книги, статьи и аналогии с языками программирования.
• Участники делятся ресурсами для изучения темы, такими как книги "Type Theory and Formal Proof" и блог-пост с введением в λ-исчисление на Python.
• Поднимаются вопросы о сложности восприятия материала и даются советы, как преодолеть первоначальное непонимание.
• Высказываются идеи о применении λ-исчисления и комбинаторной логики как общей семантической основы для языков и систем.
• Обсуждается связь λ-исчисления с формальными доказательствами и системами типов, а также его практическая полезность.

• Критика стиля и содержания поста Вольфрама: много визуализаций без ясной цели, изобретение непонятного термина "ruliology", самопрезентация автора.
• Положительные отзывы: пост как хорошее введение в лямбда-исчисление, демонстрация ценности визуализации даже абстрактных концепций, стимулирующий и ясный стиль написания.
• Сравнение с другими систематическими работами: упоминание функционального аналога "занятого бобра" (A333479) и вопроса о простоте анализа по сравнению с машинами Тьюринга.
• Обсуждение целевой аудитории: пост написан не для инженеров-программистов, а для физиков и математиков, изучающих вычисления.
• Упоминание концепций Вольфрама: "ruliad" (вселенная как программа) и "ruliology" как их изучение, переоткрытие тезиса Чёрча-Тьюринга.

Репозиторий показывает, как в Racket писать анонимные рекурсивные функции без letrec и имен.
Ключевая идея — Y-комбинатор: лямбда получает себя как аргумент и вызывает его для следующего шага.

(define Y
  (λ (f)
    ((λ (x) (x x))
     (λ (x) (f (λ (a) ((x x) a)))))))

((Y (λ (fact)
      (λ (n)
        (if (zero? n) 1 (* n (fact (sub1 n)))))))
 5) ; 120

Такой приём работает для любой рекурсии: факториал, fib, обход списков и т.д.

• Обсуждение началось с примера анонимной рекурсии на Racket; оказалось, что код совместим с любым R6RS-Scheme, включая проект scheme-rs.
• Участники сравнили подходы: в Clojure нужен явный recur, в Racket хвостовые вызовы оптимизируются автоматически.
• Кто-то спросил, стоит ли брать Racket для повторного изучения ФП; советуют почитать «zen of Racket» и быть готовым к узкой, но мощной экосистеме.
• Появились порты идеи на Python и Go (через Y-комбинатор), но часть людей предпочла бы обычный цикл для отладки.
• Сообщество предупреждает: в нишевых языках придётся уметь докручивать библиотеки «с нуля» и держать редких специалистов.

LISP FROM NOTHING
344 стр., 2025, Lulu Press, 6"×9", 19 иллюстраций, код бесплатно.

Купить: мягкий переплёт | твёрдый | PDF
Исходники | Превью (PDF) | Опечатки | Видео-обзор

Книга исследует минимальный LISP, способный интерпретировать и компилировать себя, и показывает, каким был хакинг в эпоху перфокарт и мейнфреймов. Во втором издании добавлена глава о связи LISP с λ-исчислением, улучшены макросы и стиль.

Примеры кода

• Метациркулярный интерпретатор: CL, Scheme
• Компилятор (~400 строк): liscmp.lisp.html
• Система: lisp.lisp.html
• Сборщик мусора: gc.lisp.html

Весь код книги (~100 КБ)
λ-исчисление в Scheme (~6 КБ)
Генератор перфокарт Postscript
Обложка главы «Let There Be LISP»

• Читатели восторженно отзываются о сайте и книгах Нильса М. Хольма, называя их «личной поэзией» и «культурными артефактами», созданными ради самого процесса.
• Автор подтверждает: главное для него — красота и простота изложения, а не практическая польза или научная новизна.
• Покупатели жалуются на выбор: «хочется всё сразу», но автор советует начать с одной книги и прислал шпаргалку «какую выбрать».
• Обсуждаются входные требования: книга не для новичков; рекомендуют The Little Schemer, ANSI Common Lisp и A Gentle Introduction.
• Возник спор о названии «Lisp from Nothing» при пометке «не вводная книга»; автор уточняет, что «nothing» значит «с нуля», а не «для нулевых».

Проект «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-орнаментом без смысловой нагрузки.