Hacker News Digest

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

Исследования показывают, что некоторые языки с зависимыми типами, такие как Idris, сохраняют часть информации о типах во время выполнения. Это позволяет выполнять проверки типов во время выполнения, открывая новые возможности для метапрограммирования и рефлексии. Однако такая сохранение типов увеличивает размер исполняемых файлов и может снижать производительность.

• Обсуждение показало, что зависимые типы (dependent types) — это не только академическая концепция, но и практически применимы в языках вроде Zig и TypeScript, хотя с ограничениями.
• Участники обсуждали, что в TypeScript условные типы и в Zig comptime демонстрируют схожие с зависимыми типами идеи, но не покрывают полный спектр возможностей зависимых типов.
• Были подняты вопросы о том, что такое "зависимые типы" и как они отличаются от обычных обобщённых типов, с упором на то, что в большинстве языков нет полной поддержки зависимых типов.
• Обсуждались примеры, где тип возвращаемого значения может зависеть от входного значения, и как это может быть реализовано в разных языках.
• Также обсуждались границы между статическим и динамическим анализом типов, и как они влияют на возможность компилятора вычислять и оптимизировать код.

Автор объясняет, что Isabelle сознательно отказалась от объектов доказательств, которые являются неотъемлемой частью обычных теорий типов. Это сделано потому, что объекты доказательств не нужны и занимают много места. Вместо этого Isabelle использует архитектуру LCF, где проверка типов осуществляется в языке реализации, а не в логике, что гарантирует легитимность шагов доказательства. Robin Milner имел это фундаментальное понимание 50 лет назад.

Лоуренс Полсон рассказывает о своем опыте работы с AUTOMATH и Martin-Löf type theory. Первоначально Isabelle была реализацией Martin-Löf type theory, которая до сих пор включена в дистрибутив как Isabelle/CTT. Однако автор переключился на более общий подход, вдохновленный AUTOMATH - "большим рестораном, который обслуживает любую кухню". В итоге Isabelle/HOL стала доминирующей, хотя де Брёйн не одобрял растущую мощь теорий типов и презирал теорию множеств.

• Обсуждение показало, что вопрос не в «плохих» зависимых типах, а в том, что они не нужны для большинства задач и не оправдывают свою сложность.
• Участники обсуждали, что отсутствие зависимых типов не мешает Isabelle/HOL доказать критически важные части математики, и что вместо этого важнее автоматизация и библиотеки.
• Сообщество отметило, что даже в языках без зависимых типов можно выразить «матрица 10×5 из float32», если размеры известны на этапе компиляции, и что это покрывает большинство практических случаев.
• Несколько участников поделились личным опытом, что попытка использовать зависимые типы в продакшене привела к тому, что команды отказались их использовать из-за кривой кривой обучения и отсутствия инструментальной поддержки.
• В итоге автор статьи подытожил, что выбор между зависимыми типами и другими системами типов часто сводится к личным предпочтениям и доступным инструментам, а не к объективным преимуществам.

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

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

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