Теория категорий и теория типов

Coq, Agda и Lean - это не просто «языки программирования с умными типами». Они реализуют точное математическое утверждение: программа = доказательство, тип = теорема. Если программа компилируется в Coq, она одновременно является математическим доказательством корректности. Соответствие Карри - Говарда - Ламбека - это та самая идея, доведённая до предела.

• Coq, Agda, Lean: пруф-ассистенты, основанные на CHL; формальная верификация математики и программ
• Rust borrow checker: зависимые типы в production (lifetime = зависимый тип над временем жизни)
• Идрис 2: зависимо типизированный язык общего назначения

Предварительные знания

• ∞-Categories: Morphisms Between Morphisms

Соответствие Карри - Говарда - Ламбека

Карри заметил аналогию типов и доказательств в 1934 году, Говард распространил её на интуиционистскую логику в 1969 году, а Ламбек замкнул треугольник декартово замкнутыми категориями в 1980 году. Итог: 3 независимо разработанных формализма оказались одним и тем же. **Соответствие Карри - Говарда - Ламбека** (CHL) - фундаментальный триединый изоморфизм: типы соответствуют логическим формулам и объектам категории; программы (термы) - доказательствам и морфизмам; выполнение программы - нормализации доказательства (reduction). Это не метафора, а точное математическое утверждение о трёх изоморфных формализмах.

**История CHL:** Хаскелл Карри заметил соответствие между комбинаторами и аксиомами логики (1934). Уильям Говард явно сформулировал соответствие типов и доказательств (1969, опубликовано 1980). Ламбек добавил категорную часть: декартово замкнутые категории - семантика типизированного λ-исчисления. Это три независимых открытия одного и того же.

Декартово замкнутые категории и λ-исчисление

**Декартово замкнутая категория (CCC)** - категория с конечными произведениями и степенными объектами B^A. Теорема Ламбека - Скотта: категорная семантика типизированного λ-исчисления - в точности CCC. Каждый терм λ-исчисления - морфизм, каждое правило вывода - категорная конструкция.

**Нормализация = вычисление:** Теорема нормализации для просто типизированного λ-исчисления: каждая типизированная программа завершается. Категорно: это следует из того, что CCC имеет начальную алгебру. Это обосновывает корректность всех программ в Coq/Agda - они гарантированно завершаются.

Зависимые типы и локально декартово замкнутые категории

**Зависимые типы** - типы, зависящие от значений: Vec n A = «вектор длины n». Их семантика - **локально декартово замкнутые категории (LCCC)**. В LCCC срезовые категории C/A замкнуты декартово, что даёт семантику для Π (зависимое произведение) и Σ (зависимая сумма). HoTT добавляет путевые типы, превращая типы в ∞-группоиды.

**Martin-Löf Type Theory и LCCC:** Пер Мартин-Лёф разработал зависимую теорию типов (MLTT) как основание конструктивной математики. Сеймур Сеймур и Мартин Хофманн показали, что семантика MLTT - в точности LCCC. Это открыло путь к Coq, Agda и Lean, где «программа = доказательство» в буквальном смысле.

Ключевые идеи

• CHL: типы=формулы=объекты, термы=доказательства=морфизмы, β-редукция=cut elimination
• CCC = семантика просто типизированного λ-исчисления (Ламбек - Скотт)
• LCCC = семантика зависимых типов: Π_f ⊣ f* ⊣ Σ_f в срезовых категориях
• HoTT: типы = ∞-группоиды; унивалентность (A≃B) ≃ (A=B)

Связанные темы

Теория типов связывает категорную алгебру с основаниями математики.

• Топосы — Топос = категория с внутренней теорией типов; internal language топоса = интуиционистская TT
• Пределы и копределы — Σ (зависимая сумма) = копредел; Π (зависимое произведение) = предел в срезовой категории
• ∞-категории — HoTT: путевые типы = морфизмы в ∞-группоиде; унивалентность = Гротендик-гипотеза

Вопросы для размышления

• Что означает «программа завершается» в контексте теоремы нормализации? Почему это связано с существованием начальной алгебры?
• Как тип Vec n A кодирует инвариант длины? Что произойдёт, если попытаться написать небезопасный head для Vec 0 A?
• В чём принципиальная разница между System F (полиморфизм) и зависимыми типами? Какие утверждения выражимы в одном, но не в другом?

Связанные уроки

• plt-02-type-systems
• plt-09-dependent-types