Учебник Теория типов для начинающих

Программа курса

1. 1 Что такое теория типов и зачем она

   1. Что такое тип на самом деле

      Тип — не «целое» или «строка», а множество значений с операциями и обещание, которое компилятор проверяет до запуска программы.

   2. Типы как спецификация и предотвращение ошибок

      Сигнатура функции — это контракт. Чем выразительнее тип, тем больше неверных программ он отвергает ещё до запуска.

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

      Системы типов лежат в основе компиляторов, IDE и формальной верификации: один и тот же аппарат проверяет программы и доказательства.

2. 2 История и мотивация: парадоксы

   1. Парадокс Рассела и кризис оснований

      Парадокс Рассела о «множестве всех множеств, не содержащих себя» пошатнул основания математики и породил теорию типов как лекарство.

   2. Типы как лекарство от парадоксов

      Теория типов Рассела ввела иерархию уровней: объект всегда ниже коллекции, а самоприменение запрещено — парадокс исчезает.

   3. Краткая история систем типов

      От Чёрча и STLC через Хиндли — Милнера, System F и Карри — Говарда к зависимым типам и языкам вроде Rust и Coq.

3. 3 Нетипизированное лямбда-исчисление

   1. Синтаксис лямбда-исчисления

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

   2. Связанные и свободные переменные, альфа-эквивалентность

      Имя переменной — лишь ярлык: связанные имена можно переименовывать (альфа-эквивалентность), а свободные несут смысл из контекста.

   3. Бета-редукция: вычисление как переписывание

      Единственное правило вычисления: подставить аргумент в тело функции. Реализуем безопасную подстановку и нормализацию на Python.

   4. Лямбда как модель вычислений: числа Чёрча

      Без чисел, булевых и циклов — только функции. Кодируем натуральные числа и сложение, исполняем интерпретатор и получаем 2+3=5.

4. 4 Простое типизированное лямбда-исчисление

   1. Зачем типизировать лямбда-исчисление

      Нетипизированное исчисление допускает бессмысленные и незавершающиеся термы. Типы отсекают их и гарантируют завершаемость STLC.

   2. Типы-функции и контекст типизации

      Стрелочный тип A -> B и контекст Г связывают переменные с типами. Учимся читать суждение Г |- e : T.

   3. Правила типизации STLC

      Три правила — переменная, абстракция, аппликация — полностью задают типизацию STLC. Реализуем чекер на Python.

   4. Чтение дерева вывода типов

      Дерево вывода (derivation) — формальное доказательство, что терм имеет тип. Учимся строить и читать его на ASCII.

5. 5 Вывод типов: Хиндли — Милнер

   1. Проверка против вывода типов

      Type checking требует аннотаций и проверяет их; type inference выводит типы сам. В чём разница и почему вывод сложнее.

   2. Типовые переменные и унификация

      Унификация решает уравнения между типами, находя подстановку переменных. Реализуем алгоритм с occurs-check на Python.

   3. Алгоритм W: вывод как в Haskell и OCaml

      Algorithm W обходит терм, порождает уравнения и решает их унификацией. Собираем мини-движок вывода типов на Python.

   4. Let-полиморфизм и обобщение

      Чтобы одна let-привязка работала на разных типах, её тип обобщают в схему forall. Так id применяется и к числу, и к строке.

6. 6 Полиморфизм и алгебраические типы

   1. Параметрический полиморфизм и параметричность

      Одна функция forall a. для всех типов сразу. Параметричность даёт «бесплатные теоремы»: по типу можно угадать поведение.

   2. Алгебраические типы: суммы и произведения

      Произведения (кортежи, записи) и суммы (варианты) — два кирпича данных. Их «алгебра» считает число обитателей типа.

   3. Ad-hoc полиморфизм, перегрузка и субтипизация

      Кроме параметрического есть ad-hoc полиморфизм (перегрузка, классы типов) и полиморфизм подтипов. Разбираем три вида и их различия.

   4. Алгебраические типы как логика

      Произведение — конъюнкция, сумма — дизъюнкция, функция — импликация, Void — ложь. Первый взгляд на соответствие типов и логики.

7. 7 Карри — Говард и классы типов

   1. Соответствие Карри — Говарда

      Глубочайшая идея теории типов: типы — это утверждения, программы — доказательства, а проверка типов — проверка доказательства.

   2. Классы типов и словари

      Type classes Haskell — дисциплинированная перегрузка. Под капотом они компилируются в передачу словарей методов. Моделируем механизм.

   3. Пропозиции как типы на практике: Coq и Lean

      Как доказывают теоремы и верифицируют программы в Coq, Agda, Lean: тактики, проверенное ядро, реальные результаты вроде CompCert.

8. 8 Зависимые типы, реальные языки и горизонты

   1. Зависимые типы: типы, зависящие от значений

      Vector длины n, where n — значение в типе. Зависимые типы позволяют доказывать свойства программ: Agda, Idris, Coq.

   2. Системы типов реальных языков и продвинутые возможности

      Компромиссы Haskell, Rust, TypeScript, Scala и продвинутые механизмы: GADT, higher-kinded types, линейные типы, эффекты.

   3. Границы вывода, практическая польза и связь с категориями

      Вывод vs проверка vs реконструкция, почему полный вывод бывает неразрешим, как типы улучшают любой код и обзор связи с теорией категорий.