Математическая логика
Теория типов
Rust отклоняет программы с use-after-free до запуска, Agda доказывает теоремы как часть кода. За этим стоит изоморфизм Карри-Говарда 1969 года: типы - это утверждения, программы - это доказательства. Одна идея уничтожила границу между математикой и программированием.
- Rust: система владения - применение теории линейных типов для безопасности памяти
- Haskell GHC: System F - полиморфная типизация для 40M строк промышленного кода
- Lean 4: формальная верификация математики - 300 страниц за 0.1 секунды
- CompCert: верифицированный C-компилятор без багов оптимизации (NASA, Airbus)
- seL4: верифицированное ядро ОС для дронов и автономных систем
- Agda/Coq: зависимые типы для верификации криптографических протоколов
Rust отклоняет программу с use-after-free до компиляции. Haskell выводит тип без единой аннотации. Agda доказывает коммутативность сложения как часть программы. Всё это - одна идея: **тип программы = математическое утверждение о её поведении**. Теория типов стирает границу между кодом и доказательством.
**О чём этот урок на самом деле:** не о синтаксисе типов, а о том, что система типов - это логическая система. Писать типизированный код = делать математически строгие утверждения. Компилятор - proof checker. Баг - логическое противоречие.
Просто типизированное лямбда-исчисление
STLC - минимальная система, где типы предотвращают бессмысленные применения. Тип τ ::= Base | τ₁ → τ₂. Три правила: переменная, абстракция, применение. Главное свойство - **нормализация**: все хорошо типизированные программы завершаются. Цена: не тьюринг-полна.
System F и параметричность
System F добавляет ∀α. Тип ∀α. α → α населён единственной функцией - identity. Тип ∀α. α населён нулём функций (Bottom в Haskell). **Теорема параметричности Рейнольдса**: тип полностью определяет поведение. Функция ∀α. [α] → [α] может только переставлять элементы.
Curry-Howard: программы как доказательства
Зависимые типы в промышленности
**CompCert** - C-компилятор без единого найденного бага оптимизации, доказанный в Coq. Используется в авиационном ПО. **Fiat Cryptography** - криптографический код для Chrome/Firefox, сгенерированный из Coq-доказательств. **seL4** - ядро ОС для дронов и медицинского оборудования, верифицированное в Isabelle/HOL.
**Теория типов в индустрии** От академических систем до production-компиляторов • **Haskell / GHC** (System F + extensions): System F с rank-N polymorphism, GADTs (ограниченные зависимые типы), type families. Используется в финтехе (Jane Street, Standard Chartered) • **Rust** (Линейные типы + lifetimes): Borrow checker = линейная логика. [u8; N] = ограниченные зависимые типы. Memory safety без GC, используется в ядре Linux 6.1+ • **Coq / Rocq** (CIC = зависимые типы + индукция): CompCert, seL4, математика (4-color theorem, Feit-Thompson). Extraction в OCaml/Haskell. • **Agda** (Чистая MLTT): Pattern matching, без тактик. Используется для верификации криптографических протоколов и формализации математики. • **Lean 4** (Математическая библиотека Mathlib)
Просто типизированное лямбда-исчисление
Rust не даёт скомпилировать программу, которая использует освобождённую память. Haskell выводит тип функции без единой аннотации. GHC отклоняет программу с "could not match type Int with Bool" до запуска. Это всё - **просто типизированное лямбда-исчисление (STLC)** в действии: система типов как статический доказатель свойств.
STLC добавляет типы к лямбда-исчислению Чёрча. Тип задаётся грамматикой: τ ::= Base | τ₁ → τ₂. Ключевое свойство: **нормализация** - все хорошо типизированные программы завершаются. Это значит, что STLC не тьюринг-полна - зато все программы в ней корректны.
Контр-интуиция: STLC **сильнее** нетипизированного лямбда-исчисления в одном смысле - гарантирует завершение. Но **слабее** в другом - нельзя написать произвольную рекурсию. Haskell обходит это добавляя fix-point комбинатор как примитив.
Какой тип имеет терм λf:(Int→Int). λx:Int. f (f x) в STLC?
λf принимает функцию типа Int→Int, λx принимает Int. Тело f(f x) имеет тип Int, поэтому весь терм имеет тип (Int→Int) → Int → Int.
System F: параметрический полиморфизм
Жан-Ив Жирар (1972) и Джон Рейнольдс (1974) независимо открыли System F. Она лежит в основе Haskell, ML, Scala, Rust generics. Ключевая идея: функция может быть обобщена по типам через квантификатор ∀α. Тип ∀α. α → α описывает **единственную** возможную функцию - identity. Это параметричность Рейнольдса: тип говорит всё о поведении.
**Теорема параметричности (Рейнольдс):** тип функции полностью определяет её поведение. Функция типа ∀α. [α] → [α] может только переставлять элементы - она не может создать элемент нового типа α или заглянуть в значения. Это мощный инструмент для рассуждения о коде.
Сколько различных функций типа ∀α. α → α → α существует в System F?
Параметричность System F исключает все варианты кроме const (вернуть первый) и flip-const (вернуть второй) - никаких инспекций типа α нет.
Изоморфизм Карри-Говарда
1934 год: Хаскелл Карри замечает, что типы комбинаторов соответствуют аксиомам интуиционистской логики. 1969 год: Уильям Говард делает это точным. Результат: **каждый тип - это теорема, каждая программа - доказательство**. Написать функцию типа A → B значит доказать импликацию A → B. Это не метафора - это точный изоморфизм.
**seL4** - ядро операционной системы, работающее на спутниках NASA и медицинском оборудовании, доказано корректным в Isabelle/HOL через изоморфизм Карри-Говарда. Если компилируется - то математически корректно.
По изоморфизму Карри-Говарда, какую теорему доказывает программа типа A×B → A?
Произведение A×B соответствует конъюнкции A∧B, проекция fst: A×B→A - это доказательство того, что из A∧B следует A.
Зависимые типы: типы зависят от значений
Функция конкатенации списков в Haskell имеет тип [a] → [a] → [a]. Она не знает длины. В Agda та же функция имеет тип Vec n a → Vec m a → Vec (n+m) a - компилятор **доказывает** арифметическое равенство длин. Вызов head [] - ошибка компиляции, не рантайм. Это зависимые типы: типы, зависящие от значений.
**Rust** реализует ограниченные зависимые типы: `[u8; 32]` vs `[u8; 64]` - разные типы. Borrow checker - это линейная логика (каждый ресурс используется ровно один раз). Lifetimes - это ограниченные зависимые типы над временными регионами. Rust доказывает memory safety статически.
Что принципиально отличает зависимые типы от System F?
В System F ∀α зависит только от типов. В зависимых типах тип Vec n a зависит от значения n - это позволяет статически проверять размерности массивов.
Терм: λf:(Int→Int). λx:Int. f (f x) Шаг 1: контекст Γ = {f: Int→Int, x: Int} Шаг 2: f : Int→Int, x : Int => f x : Int (применение) Шаг 3: f : Int→Int, (f x) : Int => f(f x) : Int (применение) Шаг 4: λx:Int. f(f x) : Int→Int (абстракция по x) Шаг 5: λf:(Int→Int). λx:Int. f(f x) : (Int→Int) → Int → Int (абстракция по f)
| Логика (интуиционистская) | Теория типов | Программирование |
|---|---|---|
| Пропозиция P | Тип T | Спецификация |
| Доказательство P | Терм t : T | Программа |
| A ∧ B | A × B | Tuple/пара |
| A ∨ B | A + B | Either/union |
| A → B | A → B | Функция |
| ⊥ (ложь) | Void/Never | Бесконечный цикл |
| ∀x:A. P(x) | Π(x:A). P(x) | Зависимая функция |
| ∃x:A. P(x) | Σ(x:A). P(x) | Зависимая пара |
Упражнения
- Что такое изоморфизм Карри-Говарда и почему он важен практически? — Типы = пропозиции, программы = доказательства; Написать функцию f:A→B = доказать теорему A→B; Compilers как proof checkers: CompCert, seL4; Практически: статический анализ = формальная верификация
- Чем зависимые типы мощнее параметрического полиморфизма (System F)? — System F: типы зависят от типов (∀α); Dependent types: типы зависят от значений (Π, Σ); Vec n A - длина в типе; head безопасен статически; Rust [u8; N] - ограниченный вариант зависимых типов
Ключевые идеи
- STLC: типы = статические гарантии; нормализация = все программы завершаются (цена: не тьюринг-полна)
- System F: ∀α даёт параметрический полиморфизм; параметричность Рейнольдса - тип определяет поведение
- Curry-Howard: тип = теорема, программа = доказательство; компилятор - это proof checker
- Зависимые типы: Π(x:A).B(x) = ∀, Σ(x:A).B(x) = ∃; Vec n A гарантирует длину статически
- Rust: borrow checker = линейная логика; lifetimes = ограниченные зависимые типы
- CompCert, seL4, Fiat Crypto - промышленные верифицированные системы на зависимых типах
Связанные темы
Теория типов объединяет логику, программирование и математику
- Конструктивная математика и MLTT — Следующий урок: зависимые типы полностью, BHK-интерпретация, Agda/Coq на практике
- Теория категорий и логика — CCC = STLC; топосы = логика высшего порядка; Curry-Howard-Lambek
- Естественный вывод — Правила вывода STLC изоморфны правилам естественного вывода