Типы как фундамент языков и доказательств

Где именно работают типы — от автодополнения в редакторе до доказанной корректности ядра ОС.

Система типов — это формальный аппарат, единый для проверки программ и (через соответствие Карри — Говарда) математических доказательств.

Типы внутри компилятора

Любой типизированный компилятор имеет фазу type checking между парсингом и генерацией кода. На ней строится вывод типов для всего дерева программы. Результат фазы двойной: либо набор ошибок типов с точными позициями, либо аннотированное дерево, где у каждого узла известен тип. Эта аннотация — топливо для последующих фаз: выбор перегрузки, мономорфизация дженериков, оптимизации, генерация эффективного машинного кода.

Мы уже встречали эти фазы в курсах «Компиляторы» и «Теория автоматов»: лексер → парсер → семантический анализ (здесь живут типы) → IR → кодоген. Теория типов — это формальная теория именно семантического анализа.

Типы внутри инструментов разработчика

Автодополнение, переход к определению, безопасный рефакторинг «переименовать символ», подсветка ошибок на лету — всё это работает поверх информации о типах. Когда IDE предлагает методы после точки, она спрашивает у системы типов: «какой тип у этого выражения и какие операции для него определены?». Без типов инструмент гадает; с типами — знает.

Типы как доказательства

Самое поразительное: тот же аппарат проверяет математические доказательства. Соответствие Карри — Говарда утверждает, что типы — это утверждения, а программы — доказательства. Проверить, что программа имеет тип A -> B — то же самое, что проверить доказательство импликации «из A следует B». На этом стоят Coq, Lean, Agda, Idris: в них пишут программы, а получают проверенные теоремы.

Это не игрушка. На Coq доказана корректность компилятора C (проект CompCert), на seL4 — корректность микроядра ОС относительно спецификации. «Доказано системой типов» здесь означает машинно-проверенную гарантию, которой не даст ни один объём тестов.

Маленький мост к доказательствам

Идею «тип = утверждение» можно нащупать руками. Тип-произведение (A, B) соответствует конъюнкции «A и B»: чтобы построить пару, нужны обе части. Тип-функция A -> B соответствует импликации. Проверим конъюнкцию как «у нас есть оба доказательства».

# пара значений = доказательство конъюнкции "A и B"
def and_intro(a, b):
    return (a, b)            # чтобы доказать A и B, нужны обе части

def proj_left(pair):        # из "A и B" следует A
    return pair[0]

proof_AB = and_intro("док-во A", "док-во B")
print("есть пара  :", proof_AB)
print("извлекли A :", proj_left(proof_AB))

Вывод:

есть пара  : ('док-во A', 'док-во B')
извлекли A : док-во A

Структура программы (построили пару — извлекли часть) дословно повторяет структуру доказательства (ввели конъюнкцию — применили правило исключения). Это и есть Карри — Говард в зародыше.

Как работает под капотом

Под «проверкой» и в компиляторе, и в Coq лежит один механизм — проверка вывода по правилам в контексте Γ ⊢ e : T. Разница лишь в выразительности системы: у языка общего назначения она проще (чтобы вывод был быстрым и автоматическим), у систем доказательств — богаче (зависимые типы), ценой того, что часть проверки человек ведёт вручную.

Частые ошибки

• Считать типы «фичей языка», а не теорией. Один и тот же формализм переиспользуется компиляторами, IDE и пруверами — это общематематический инструмент.
• Думать, что верификация заменяет спецификацию. Доказывается соответствие спецификации; если спецификация неверна, доказанная программа всё равно делает не то.
• Путать «прошло тесты» и «доказано». Тесты проверяют конечное число случаев; типовое доказательство — все.

Итоги

• Проверка типов — отдельная фаза компилятора, дающая аннотированное дерево для кодогена.
• Инструменты разработчика (автодополнение, рефакторинг) опираются на типовую информацию.
• Через Карри — Говарда тот же аппарат проверяет математические доказательства.
• На системах типов построены машинно-проверенные компиляторы и ядра ОС.