Теория языков программирования

Зависимые типы

Что если компилятор мог бы доказать: «эта функция никогда не получит пустой список», «этот индекс всегда в границах массива», «этот файл открыт перед чтением»? Не через тесты, не через assertions - а как математическую теорему при компиляции. Зависимые типы делают именно это: типы становятся спецификациями, программа - доказательством.

**Аэрокосмос (Airbus, NASA):** верификация критического ПО через Coq и Agda - зависимые типы как формальные доказательства корректности
**Liquid Haskell в Jane Street:** финансовый код с refinement types - доказанное отсутствие divide-by-zero и out-of-bounds доступа
**Rust const generics:** `[T; N]` - массив ровно N элементов, прямой потомок идей зависимых типов, уже в production

Зависимые функции и Π-типы

Обычная функция `length : List a -> Int` возвращает одинаковый тип `Int` при любом аргументе. **Зависимая функция** (Π-тип) позволяет типу результата зависеть от *значения* аргумента. Например, `replicate : (n : Nat) -> a -> Vect n a` возвращает вектор *ровно n элементов* - и это гарантировано на уровне типа, не теста.

Запись `(n : Nat) -> Vect n a` читается: «для каждого натурального числа n - тип Vect n a». Тип результата буквально содержит переменную `n`. Это и есть Π-тип (Pi-type): обобщение типа функции, в котором кодомен зависит от значения аргумента.

**Π-тип vs параметрический полиморфизм:** `List a` - одна реализация для любого `a`, тип не меняется. `Vect n a` - каждое значение `n` порождает *разный тип*. Это на уровень выразительнее generics.

Функция `head : Vect (S n) a -> a` принимает вектор типа `Vect (S n) a`. Что означает `S n` в типе?

Propositions as Types: изоморфизм Карри-Говарда

В 1934 году Карри заметил: комбинаторы в логике соответствуют типам в лямбда-исчислении. Говард формализовал это в 1969-м. Результат - **изоморфизм Карри-Говарда**: логические утверждения и типы - одно и то же, а доказательства и программы - тоже одно и то же.

Следствие: если программа компилируется - она уже является доказательством утверждения, соответствующего её типу. В зависимо-типизированных языках типы могут выражать произвольные математические утверждения, а компилятор проверяет их корректность.

**Практическое следствие:** системы вроде Agda, Coq, Lean 4, Idris используют этот изоморфизм для верификации программ. Доказать теорему = написать функцию нужного типа.

По изоморфизму Карри-Говарда, чему соответствует функция типа `A -> B`?

Idris 2: зависимые типы на практике

Idris 2 - язык с полноценными зависимыми типами, ориентированный на практику, а не только на теорию. Его автор Эдвин Брейди называет цель «программирование с доказательствами». В отличие от Agda или Coq, Idris компилирует в исполняемый код и имеет нотацию, близкую к Haskell.

Особенно полезна идиома **state machines через типы**: состояние объекта кодируется в его типе. Файл `File Open` и `File Closed` - разные типы, и `read` принимает только открытый. Протокол использования ресурса становится частью системы типов.

**Holes и интерактивная разработка:** Idris поддерживает `?hole` в коде - компилятор покажет, какой тип нужно построить в этом месте. Это делает написание доказательств интерактивным процессом.

В Idris типы `File Open` и `File Closed` являются разными типами. Что это позволяет гарантировать?

Refinement Types: Liquid Haskell

Полные зависимые типы требуют доказательств вручную. **Refinement types** - практичный компромисс: базовый тип уточняется логическим предикатом, а SMT-решатель (Z3) проверяет корректность автоматически. Программист пишет аннотации, компилятор доказывает.

Liquid Haskell работает поверх обычного Haskell - никакой новой системы типов. Аннотации не влияют на runtime, но дают компилятору дополнительную информацию для проверки. SMT-решатель Z3 автоматически находит доказательства простых арифметических свойств.

**Ограничения refinement types:** SMT-решатель справляется со многими случаями автоматически, но не со всеми. Сложные доказательства (например, коммутативность умножения натуральных чисел) требуют ручных лемм. Зависимые типы в Idris/Agda выразительнее, но трудоёмче.

Зависимые типы - академическая экзотика без практического применения

Refinement types (Liquid Haskell) используются в production Haskell. Идеи зависимых типов влияют на TypeScript (template literal types), Rust (const generics), Scala (singleton types).

Полные зависимые типы действительно редки в production, но их упрощённые формы проникают в mainstream языки и устраняют целые классы багов на уровне компиляции.

Чем Liquid Haskell отличается от полных зависимых типов (Idris)?