Типизированное лямбда-исчисление и соответствие Карри-Ховарда

К этому моменту трека у нас на руках полноценный язык программирования, собранный из трёх конструкций. В нём есть логика, арифметика, структуры данных, рекурсия и стратегии вычисления. Он полон по Тьюрингу. Казалось бы, чего ещё желать.

Проблема в том, что он полон по Тьюрингу слишком буквально. В нём можно написать всё — включая полную бессмыслицу, и никто вас не остановит.

Мир, в котором можно всё

Вот три совершенно легальных бестиповых терма:

TRUE 3           -- применяем «истину» к тройке
(λx. x x) 5      -- применяем пятёрку к пятёрке
Ω = (λx. x x) (λx. x x)

Первый терм — TRUE 3 — не ошибка синтаксиса. TRUE = λx. λy. x, значит TRUE 3 бета-редуцируется в λy. 3. Это работает, просто смысла в этом ноль: мы применили булево значение как функцию к числу. В бестиповом мире у термов нет «сорта», всё есть функция, поэтому всё применимо ко всему.

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

(λx. x x) (λx. x x)
  -- подставляем x := (λx. x x) в тело x x
→ (λx. x x) (λx. x x)
  -- получили ровно то же самое
→ (λx. x x) (λx. x x)
→ ...

Нормальной формы нет. Вычисление никогда не заканчивается, и заранее по виду терма определить это в общем случае невозможно — это проблема остановки, о которой подробнее в треке mathematics.

Обе беды — и TRUE 3, и Ω — лечатся одним лекарством. Нужно ввести понятие «сорта» значения и запретить применять функцию к аргументу не того сорта. Сорт называется типом, а получившаяся система — простым типизированным лямбда-исчислением (simply typed lambda calculus, λ→). Придумал его сам Чёрч в 1940 году, через шесть лет после бестиповой версии.

Забегая вперёд: платить придётся полнотой по Тьюрингу. Взамен вы получите гарантию завершения любой программы и — совершенно неожиданно — работающий язык математических доказательств.

Типы: всего два правила

Типы строятся так же минималистично, как и сами термы. Нужны ровно две вещи.

Типы:  T ::= A | B | C | ...     базовые типы (примитивы: Bool, Nat, String)
            | T -> T             тип функции: берёт T, возвращает T

Всё. Никаких классов, интерфейсов, generic-ов — пока. Стрелка правоассоциативна, ровно как каррирование в термах:

A -> B -> C   читается как   A -> (B -> C)

То есть «функция, которая берёт A и возвращает функцию из B в C». Это ровно то же соглашение, что в TypeScript и Haskell, и ровно та же логика, что при чтении аппликации слева направо.

Термы почти не меняются — добавляется одна вещь: у параметра абстракции теперь есть аннотация типа.

Термы: t ::= x                переменная
            | λx:T. t         абстракция С УКАЗАННЫМ ТИПОМ параметра
            | t t             аппликация

Сравните живьём. Было:

const twice = f => x => f(f(x));

Стало (TypeScript — это буквально типизированное лямбда-исчисление с сахаром):

const twice = (f: (a: number) => number) => (x: number): number => f(f(x));

from typing import Callable

def twice(f: Callable[[int], int]) -> Callable[[int], int]:
    return lambda x: f(f(x))

Терм на языке λ→:

λf:(Nat -> Nat). λx:Nat. f (f x)

Тип этого терма: (Nat -> Nat) -> Nat -> Nat. Ниже разберём, откуда он берётся, по шагам.

Три правила типизации — и больше ничего

Чтобы говорить о типах переменных, нужен контекст — список «какая переменная какого типа». Обозначается греческой Γ (гамма) и читается как обычный словарь: f : A->B, x : A.

Запись Γ |- t : T читается вслух так: «в контексте Γ терм t имеет тип T». Значок |- называется турникетом. Ничего мистического: это просто «⟹ выводимо».

Правил ровно три — по одному на каждую конструкцию языка.

                x : T содержится в Γ
(VAR)         ───────────────────────
                    Γ |- x : T


                  Γ, x : A  |-  t : B
(ABS)        ───────────────────────────────
              Γ  |-  (λx:A. t)  :  A -> B


           Γ |- f : A -> B        Γ |- a : A
(APP)     ──────────────────────────────────────
                    Γ  |-  f a  :  B

Черта — это правило вывода: над ней посылки, под ней заключение. Читается снизу вверх: «чтобы доказать нижнее, докажи верхнее».

По-человечески:

• VAR: тип переменной берём из контекста. Если её там нет — терм не типизируется (свободная переменная неизвестного типа).
• ABS: чтобы узнать тип λx:A. t, кладём x : A в контекст, узнаём тип тела t — пусть это B — и склеиваем в A -> B.
• APP: аппликация f a законна, только если f — функция, и её входной тип в точности совпадает с типом a. Результат — выходной тип функции.

Правило APP — это и есть тот самый запрет, ради которого всё затевалось. TRUE 3 не типизируется: TRUE : A -> B -> A, значит вход должен быть типа A, а 3 : Nat. Если A не Nat — отказ. И даже если подобрать типы так, чтобы прошло, результат окажется осмысленным, а не мусором.

Полный вывод типа, шаг за шагом

Разберём λf:A->B. λx:A. f x — композицию в чистом виде. Ни одного «очевидно», все шаги подряд.

Шаг 1. Начинаем с пустого контекста. Внешняя абстракция, применяем ABS: кладём f : A->B в контекст, теперь надо узнать тип тела λx:A. f x.

Контекст: f : A->B
Цель:     λx:A. f x  :  ?

Шаг 2. Снова абстракция, снова ABS: кладём x : A, узнаём тип тела f x.

Контекст: f : A->B,  x : A
Цель:     f x  :  ?

Шаг 3. Аппликация, применяем APP. Нужны типы обеих частей.

Шаг 3а. Левая часть — f. Правило VAR: смотрим в контекст, находим f : A->B. Это функция — хорошо, APP применимо.

Шаг 3б. Правая часть — x. Правило VAR: в контексте x : A.

Шаг 3в. Проверка APP: входной тип функции — A, тип аргумента — A. Совпали. Значит f x : B.

Шаг 4. Возвращаемся в шаг 2. Тело имеет тип B, параметр объявлен как A, по ABS собираем: λx:A. f x : A -> B.

Шаг 5. Возвращаемся в шаг 1. Тело имеет тип A -> B, параметр объявлен как A->B, по ABS собираем:

|-  λf:A->B. λx:A. f x  :  (A -> B) -> A -> B

Готово. Вот это дерево целиком:

Обратите внимание на скобки в итоговом типе: (A -> B) -> A -> B, а не A -> B -> A -> B. Первый аргумент — сам функция, поэтому его тип обязан быть в скобках. Правоассоциативность стрелки без скобок прочитала бы это иначе.

Тайпчекер на 40 строк

Правила выше настолько механические, что переводятся в код почти дословно. Вот работающий тайпчекер λ→ на Python.

from dataclasses import dataclass

# ---------- Типы ----------
@dataclass(frozen=True)
class Base:
    """Базовый тип: A, Nat, Bool..."""
    name: str
    def __str__(self):
        return self.name

@dataclass(frozen=True)
class Arrow:
    """Тип функции src -> dst"""
    src: object
    dst: object
    def __str__(self):
        # слева скобки нужны: стрелка правоассоциативна
        left = f"({self.src})" if isinstance(self.src, Arrow) else str(self.src)
        return f"{left} -> {self.dst}"

# ---------- Термы ----------
@dataclass(frozen=True)
class Var:
    name: str

@dataclass(frozen=True)
class Lam:
    param: str
    ty: object      # аннотация типа параметра — то самое ":T"
    body: object

@dataclass(frozen=True)
class App:
    fn: object
    arg: object

class TypeErr(Exception):
    pass

def typecheck(term, env=None):
    """Возвращает тип терма или бросает TypeErr."""
    env = {} if env is None else env

    if isinstance(term, Var):                       # правило VAR
        if term.name not in env:
            raise TypeErr(f"переменная {term.name} не найдена в контексте")
        return env[term.name]

    if isinstance(term, Lam):                       # правило ABS
        inner = {**env, term.param: term.ty}        # Γ, x:A
        body_ty = typecheck(term.body, inner)       # выводим B
        return Arrow(term.ty, body_ty)              # склеиваем A -> B

    if isinstance(term, App):                       # правило APP
        fn_ty = typecheck(term.fn, env)
        arg_ty = typecheck(term.arg, env)
        if not isinstance(fn_ty, Arrow):
            raise TypeErr(f"применяем не функцию, а значение типа {fn_ty}")
        if fn_ty.src != arg_ty:
            raise TypeErr(f"ожидался аргумент {fn_ty.src}, получен {arg_ty}")
        return fn_ty.dst

    raise TypeErr("неизвестная конструкция")

Проверяем на композиции из разбора выше:

A, B = Base("A"), Base("B")

compose = Lam("f", Arrow(A, B),
              Lam("x", A,
                  App(Var("f"), Var("x"))))

print(typecheck(compose))       # (A -> B) -> A -> B

И на заведомо кривом терме:

bad = App(Lam("x", A, Var("x")), Lam("y", B, Var("y")))
typecheck(bad)
# TypeErr: ожидался аргумент A, получен B -> B

Сложность. Каждый узел терма обходится ровно один раз, поэтому проверка — O(n) вызовов по размеру терма n. Единственная нетривиальная операция — сравнение типов fn_ty.src != arg_ty, которое стоит O(размер типа). При хеш-консинге (одинаковые типы — один объект) сравнение схлопывается до сравнения ссылок, и общая сложность становится честным O(n) по времени и O(глубина терма) по стеку. Это к вопросу, почему тайпчекинг в языках со сплошными аннотациями (Java, Go, C#) мгновенный.

Отдельная история — вывод типов, когда аннотаций нет и их надо угадать. Это стиль Карри (в отличие от стиля Чёрча, где всё аннотировано), и там работает алгоритм Хиндли-Милнера с унификацией. Он тоже почти линеен на практике, но в худшем случае DEXPTIME-полон — из-за того, что выведенный тип может расти экспоненциально в записи. Практически вы это увидите как «TypeScript задумался на 30 секунд на одном выражении».

Вот как выглядит алгоритм проверки целиком:

Что типы дают: две теоремы

Мы наложили ограничение. Что мы за это купили? Две гарантии, которые вместе называются типобезопасностью.

Сохранение типа (Preservation, она же subject reduction). Если Γ |- t : T и t → t' за одну бета-редукцию, то Γ |- t' : T. Тип не меняется в процессе вычисления. Начали с Nat — закончим на Nat, что бы ни происходило внутри.

Прогресс (Progress). Если терм типизирован и он не значение (не абстракция и не примитив), то к нему применима хотя бы одна редукция. То есть вычисление не может «застрять» в состоянии вроде 3 true — такие состояния просто не типизируются.

Вместе они дают знаменитую формулировку Робина Милнера: well-typed programs cannot go wrong. Типизированная программа не свалится в неопределённое поведение — она либо досчитает, либо будет считать дальше. Классическое доказательство в стиле «Progress + Preservation» — Wright и Felleisen, 1994; современное изложение — глава 8 книги Бенджамина Пирса Types and Programming Languages, это главная книга по теме.

Посмотрим на Preservation в действии. Возьмём число Чёрча «два», применим к тождественной функции и к z : A, и раскрутим полностью.

Терм:     (λf:A->A. λx:A. f (f x)) (λy:A. y) z
Контекст: z : A

Типы участников (проверьте по правилам сами):

λf:A->A. λx:A. f (f x)   :   (A -> A) -> A -> A
λy:A. y                  :   A -> A
z                        :   A

Первая аппликация: (A -> A) -> A -> A применяется к A -> A → результат A -> A. Вторая: A -> A применяется к A → результат A. Значит весь терм имеет тип A.

Теперь редуцируем. Полностью, без пропусков:

Шаг 0.  (λf:A->A. λx:A. f (f x)) (λy:A. y) z

Шаг 1.  Внешний левый редекс: подставляем f := (λy:A. y)
        в тело (λx:A. f (f x)).
        → (λx:A. (λy:A. y) ((λy:A. y) x)) z
        Тип промежуточного результата: (A -> A) применён к A... 
        точнее, левая часть теперь A -> A, всё выражение — A. Тип сохранён.

Шаг 2.  Редекс: (λx:A. ...) применяется к z. Подставляем x := z.
        → (λy:A. y) ((λy:A. y) z)
        Тип: A. Сохранён.

Шаг 3.  Левый внешний редекс: (λy:A. y) применяется к ((λy:A. y) z).
        Подставляем y := ((λy:A. y) z), тело — просто y.
        → (λy:A. y) z
        Тип: A. Сохранён.

Шаг 4.  Последний редекс: подставляем y := z.
        → z
        Тип: A. Сохранён.

Нормальная форма: z

Четыре шага, тип A на каждом. Это и есть Preservation — не абстрактная теорема, а наблюдаемое свойство каждой строчки.

Цена: Y-комбинатор больше не существует

Теперь главный сюрприз, ради которого стоило всё это затевать.

Теорема о сильной нормализации. Любой типизированный терм λ→ достигает нормальной формы за конечное число шагов. При любой стратегии редукции. Всегда.

Доказал Уильям Тэйт в 1967 году методом вычислимости. Следствие ошеломляющее: в λ→ невозможно написать бесконечный цикл. Ни одна программа не зависает. Halting problem для λ→ решается тривиально: ответ всегда «завершится».

Но раз так — значит, Ω не может быть типизирована. Разберём почему, до конца.

Терм: λx. x x

Пусть x : T для какого-то типа T. Смотрим на тело x x:

Шаг 1.  Это аппликация. По правилу APP левая часть обязана быть функцией.
        Левая часть — это x, значит T = P -> Q для каких-то P, Q.

Шаг 2.  Правая часть — тоже x, её тип T. По правилу APP тип аргумента
        должен совпасть с входом функции: T = P.

Шаг 3.  Подставляем P = T в равенство из шага 1:
        T = T -> Q

Шаг 4.  Уравнение T = T -> Q не имеет решения среди конечных типов.
        Раскрутим:
            T = T -> Q
              = (T -> Q) -> Q
              = ((T -> Q) -> Q) -> Q
              = (((T -> Q) -> Q) -> Q) -> Q
              = ...
        Тип бесконечно растёт влево и никогда не замыкается.

В терминах алгоритма унификации это провал occurs check: переменная типа T встречается внутри типа, которому её пытаются приравнять. Ровно та же ошибка, что вы видите в TypeScript как «Type alias circularly references itself» или в Haskell как «Occurs check: cannot construct the infinite type».

Наш тайпчекер поймает это буквально:

self_app = Lam("x", A, App(Var("x"), Var("x")))
typecheck(self_app)
# TypeErr: применяем не функцию, а значение типа A

Раз λx. x x не типизируется, то и Ω, и Y-комбинатор — он ведь построен на λx. f (x x) — тоже. Самоприменение вне закона. А вместе с ним вне закона общая рекурсия.

Разумеется, реальные языки так жить не могут — программы обязаны уметь зацикливаться, иначе не напишешь ни сервер, ни REPL. Поэтому рекурсию возвращают явно, одним из двух способов:

Способ 1: примитив fix. Добавляем в язык константу fix : (T -> T) -> T с правилом редукции fix f → f (fix f). Получается PCF — язык Плоткина, стандартный полигон теории языков программирования. Полнота по Тьюрингу восстановлена, сильная нормализация потеряна.

Способ 2: рекурсивные типы. Разрешаем типу ссылаться на себя. Тогда уравнение T = T -> Q перестаёт быть противоречием: это просто рекурсивный тип. В TypeScript такое пишется через интерфейс:

// Рекурсивный тип: функция, принимающая саму себя
interface Rec<A> {
  (self: Rec<A>): A;
}

// Y-комбинатор, который проходит тайпчек TypeScript
const Y = <A>(f: (a: A) => A): A => {
  const g = (x: Rec<A>): A => f(x(x));
  return g(g);
};

Этот код компилируется. И — при энергичном порядке вычисления JavaScript — зависает при запуске. Именно поэтому его пишут в Z-варианте с дополнительной задержкой, как в статье о комбинаторе неподвижной точки. Мораль: рекурсивные типы возвращают полноту по Тьюрингу и одновременно ломают сильную нормализацию. Одно без другого не бывает.

Запомните это, потому что через два раздела это утверждение обернётся вопросом «а какие теоремы можно доказать в вашем языке».

Соответствие Карри-Ховарда

Теперь то, ради чего люди вообще запоминают словосочетание «типизированное лямбда-исчисление».

Посмотрите ещё раз на правило ABS, но забудьте про слово «тип» и читайте стрелку как «следует»:

      Γ, x : A  |-  t : B
   ───────────────────────────
    Γ  |-  (λx:A. t)  :  A -> B

«Если, предположив A, мы получили B, то доказано: из A следует B». Это правило введения импликации из натурального вывода Генцена. Слово в слово.

А правило APP:

   Γ |- f : A -> B        Γ |- a : A
  ──────────────────────────────────────
            Γ  |-  f a  :  B

«Если известно, что из A следует B, и известно A, то B». Это modus ponens — древнейшее правило логики.

Совпадение? Хаскелл Карри заметил его в 1934-м на комбинаторах, Уильям Ховард довёл до полной формулировки в 1969-м. Это не аналогия, а изоморфизм: два исчисления, придуманные независимо для разных целей — вычисления и рассуждения — оказались одной и той же математической структурой.

Формулируется он в трёх строчках:

Типы — это утверждения. Программы — это доказательства. Вычисление программы — это упрощение доказательства.

Проверим на комбинаторах

Возьмём знакомые термы и прочитаем их типы как утверждения.

Тождественная функция I = λx:A. x. Тип: A -> A.

Как логика: «из A следует A». Тавтология, самое скучное истинное утверждение на свете. И программа, которая его доказывает, соответственно самая скучная.

const I = <A>(x: A): A => x;

def I(x): return x   # A -> A

Комбинатор K = λx:A. λy:B. x. Тип: A -> B -> A.

Как логика: «если A истинно, то из чего угодно следует A». Тоже верно: истинное утверждение следует из любых посылок.

const K = <A, B>(x: A) => (y: B): A => x;

Комбинатор S = λf. λg. λx. f x (g x). Тип: (A -> B -> C) -> (A -> B) -> A -> C.

Как логика — вторая аксиома гильбертовского исчисления высказываний. И вот здесь начинается по-настоящему красивое: S и K — это ровно две аксиомы импликационного фрагмента интуиционистской логики, а любой типизированный терм из них строится. Комбинаторная логика и аксиоматическая логика — одно и то же множество формул.

const S = <A, B, C>(f: (a: A) => (b: B) => C) =>
          (g: (a: A) => B) =>
          (x: A): C => f(x)(g(x));

Расширяем словарь

Голых стрелок мало для интересной логики. Но каждая логическая связка находит себе типовое соответствие:

Конъюнкция «A и B» — это пара [A, B]. Чтобы доказать «A и B», нужно предъявить доказательство A и доказательство B. Чтобы построить пару, нужно предъявить два значения. Одно и то же.

// A и B -> A  (правило удаления конъюнкции)
const fst = <A, B>([a, b]: [A, B]): A => a;

// A -> B -> (A и B)  (правило введения конъюнкции)
const both = <A, B>(a: A) => (b: B): [A, B] => [a, b];

Кстати, каррирование (A и B -> C) ⟺ (A -> B -> C) в логике называется законом экспортации. Вы им пользуетесь каждый день, не подозревая, что доказываете теорему.

Дизъюнкция «A или B» — это размеченное объединение. Чтобы доказать «A или B», нужно предъявить одно из двух и сказать, какое именно. Именно поэтому в конструктивной логике дизъюнкция сильнее классической: она не позволяет знать «одно из двух верно», не зная, какое.

type Either<A, B> = { tag: "left"; value: A } | { tag: "right"; value: B };

// A -> (A или B)
const inl = <A, B>(a: A): Either<A, B> => ({ tag: "left", value: a });

// (A -> C) -> (B -> C) -> (A или B) -> C   — разбор случаев
const either = <A, B, C>(f: (a: A) => C, g: (b: B) => C) =>
  (e: Either<A, B>): C =>
    e.tag === "left" ? f(e.value) : g(e.value);

Ложь — это пустой тип. Тип, у которого нет ни одного значения: never в TypeScript, Void в Haskell, ! в Rust, NoReturn в Python. Утверждение, которое невозможно доказать ⟺ тип, значение которого невозможно построить.

Отрицание «не A» — это A -> never. «Из A следует ложь». Функция, которая, получив значение типа A, обязана вернуть невозможное — значит, значений типа A ей не видать.

type Not<A> = (a: A) => never;

// Ex falso quodlibet: из лжи следует что угодно
const exFalso = <A, B>(f: Not<A>) => (a: A): B => f(a);

Кванторы — это дженерики. <A>(...) => ... в TypeScript, forall a. в Haskell — это «для любого A». Соответствующая система называется System F (о ней ниже), а логика — интуиционистская логика второго порядка.

Чего доказать нельзя

Самое интересное в соответствии — не то, что оно позволяет, а то, что запрещает. Попробуйте честно, без any и без зацикливаний, написать эти функции:

// Закон исключённого третьего: «A или не A»
declare function lem<A>(): Either<A, Not<A>>;

// Снятие двойного отрицания: «не не A -> A»
declare function dne<A>(f: Not<Not<A>>): A;

// Закон Пирса
declare function peirce<A, B>(f: (g: (a: A) => B) => A): A;

Не получится. И не потому, что вы плохо стараетесь — а потому, что это невозможно. Лямбда-исчисление соответствует интуиционистской (конструктивной) логике, в которой этих законов нет. Причина видна прямо из типов: чтобы вернуть Either<A, Not<A>>, надо решить, какую ветку возвращать, а откуда программе знать это для произвольного A?

Обратная сторона тоже забавна: закон Пирса ((A -> B) -> A) -> A всё-таки имеет реализацию — но только если добавить в язык call/cc, оператор захвата продолжения. Тимоти Гриффин показал это в A formulae-as-types notion of control (POPL 1990), и это один из самых неожиданных результатов в теории языков: операторы управления потоком — это классическая логика. try/catch, генераторы, async/await — всё это следы классических законов, которых нет в чистых типах.

Почему ваш TypeScript — противоречивая логика

Тут пора вспомнить про сильную нормализацию. Смотрите:

// «Доказательство» чего угодно
const bogus = <A>(): A => { while (true) {} };

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

Работает фокус ровно потому, что программа не завершается. Бесконечный цикл — это «доказательство», которое никогда не заканчивается, и логика такое не принимает. Отсюда правило, которое объясняет всю конструкцию систем доказательств:

Соответствие Карри-Ховарда работает только для тотальных программ — тех, что гарантированно завершаются. Общая рекурсия ломает логику.

Именно поэтому Coq (ныне Rocq), Lean, Agda и Idris требуют, чтобы все рекурсивные определения проходили проверку на завершаемость (обычно — структурная рекурсия по убывающему аргументу). Не из вредности, а потому что без этого их доказательства ничего не стоят. И потому же обычные языки — TypeScript, Haskell, Scala — как логики противоречивы: в них есть null, any, исключения и бесконечные циклы, каждый из которых даёт «доказательство» чего угодно.

Что из этого следует практически

Может показаться, что всё это красивая, но академическая история. На деле из соответствия вытекают вещи, которыми вы пользуетесь каждый день.

Сигнатура как теорема. Что может делать функция типа <A>(x: A) => A? Ровно одно: вернуть свой аргумент. Она не знает про A ничего — ни методов, ни конструкторов, — поэтому единственная возможная реализация одна. Это не эвристика, а следствие параметричности: Филип Уодлер в работе Theorems for Free! (1989) показал, как из одной только полиморфной сигнатуры механически выводить теоремы о поведении функции. Например, для любой f : <A>(xs: A[]) => A[] автоматически верно map(g, f(xs)) === f(map(g, xs)) — не глядя в код.

Практический вывод: чем уже тип, тем меньше в нём места для багов. Функция (u: User) => string может вернуть что угодно; функция <A>(xs: A[]) => A[] физически не может выдумать новые элементы.

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

type Shape =
  | { kind: "circle"; r: number }
  | { kind: "square"; a: number };

function area(s: Shape): number {
  switch (s.kind) {
    case "circle": return Math.PI * s.r ** 2;
    case "square": return s.a ** 2;
    default:
      const _exhaustive: never = s;   // не скомпилируется, если забыли кейс
      return _exhaustive;
  }
}

Присваивание в never компилируется, только когда компилятор доказал, что сюда невозможно попасть. Это буквально доказательство от противного: «допустим, мы здесь — тогда есть значение типа never — противоречие». Добавьте в Shape третий вариант, и компилятор превратится в проверяющего доказательство: он найдёт дыру.

Системы интерактивных доказательств. Раз доказательство — это программа, то доказывать теоремы можно, программируя. На этом стоят Lean, Rocq/Coq, Agda и Idris. Реальные результаты: полностью верифицированный C-компилятор CompCert, машинно-проверенное доказательство теоремы о четырёх красках, верифицированное ядро seL4. Если хочется попробовать руками — учебник Software Foundations Пирса ведёт от λ→ до верификации программ, и это, пожалуй, лучший вход в тему.

За пределами λ→: лямбда-куб

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

Что на осях:

• Термы зависят от типов — это полиморфизм. System F, она же λ2, добавляет forall. Дженерики в TypeScript, C# и Java — её ослабленная версия. Здесь Чёрчевы числа наконец получают честный тип forall A. (A -> A) -> A -> A вместо привязки к одному конкретному A, и множество представимых функций резко расширяется — до всех функций, тотальность которых доказуема в арифметике второго порядка.
• Типы зависят от типов — конструкторы типов. Array<_>, Promise<_>, Functor f — типы, параметризованные типами. Это λω и высшие роды (higher-kinded types).
• Типы зависят от термов — зависимые типы. Тип Vec 5 Int — «вектор ровно из пяти элементов», где 5 это значение, попавшее в тип. Здесь concat : Vec n A -> Vec m A -> Vec (n+m) A — сигнатура, которая уже сама по себе теорема о длинах.

Верхний угол куба, λC, объединяет все три оси. На нём построены Rocq и Lean. Оригинальная работа Барендрегта — «Introduction to Generalized Type Systems» (Journal of Functional Programming, 1991), обзорно — глава 30 TAPL.

Практическая мораль: движение по кубу — это всегда обмен. Чем выразительнее система типов, тем больше свойств вы можете зафиксировать в сигнатурах — и тем сложнее вывод типов. В λ→ вывод разрешим, в System F вывод типов неразрешим (результат Уэллса, 1994), поэтому в реальных языках используют ограниченный фрагмент (Хиндли-Милнер), где всё выводится автоматически. Это ровно та причина, по которой в Haskell иногда приходится писать аннотации руками, а в языках с зависимыми типами — почти всегда.

Типичные ошибки понимания

«Типы нужны, чтобы компилятор генерировал быстрый код». Это польза побочная и относится к типам времени выполнения. Типы λ→ полностью стираются перед исполнением (type erasure) — вычисление типизированного терма идёт по тем же правилам, что и бестипового. Типы — про то, какие термы вообще допустимы, а не про то, как они считаются.

«Раз соответствие есть, любая моя функция что-то доказывает». Только если она тотальна и не использует any, null, исключения, приведения типов и бесконечные циклы. Практически весь прикладной код доказывает лишь «истинно всё», то есть ничего.

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

«Аннотация типа параметра — формальность, компилятор и так выведет». Разница между стилем Чёрча (аннотации обязательны) и стилем Карри (выводятся) принципиальна. Некоторые термы типизируемы в стиле Карри и требуют явных аннотаций в системах побогаче — а в System F вывод вообще неразрешим. Если TypeScript просит аннотацию — часто он не ленится, а честно расписывается в неразрешимости.

«never и void — примерно одно и то же». void — тип с одним значением (undefined), логически это ИСТИНА. never — тип без значений, логически ЛОЖЬ. Перепутать их — это перепутать истину и ложь; неудивительно, что код потом ведёт себя странно.

Упражнения

Реши сам, потом сверься. Все редукции раскручивай полностью.

1. Каков тип терма λx:A. λy:B. x? Какое логическое утверждение он доказывает?

2. Каков тип терма λf:(A->A). λx:A. f (f (f x))?

3. Покажи по шагам, почему λx:A. x x не типизируется ни при каком A.

4. Приведи к нормальной форме и укажи тип на каждом шаге, при g : A->A и w : A: (λf:(A->A). λx:A. f (f x)) g w

5. Напиши на TypeScript или Python функцию, доказывающую A -> ((A -> B) -> B). Что она утверждает?

6. Каким логическим утверждением является тип функции flip, то есть (A -> B -> C) -> B -> A -> C?

7. Почему Either<A, Not<A>> невозможно населить, а Not<Not<Either<A, Not<A>>>> — возможно?

8. Сколько разных тотальных функций имеют тип <A, B>(a: A, b: B) => A? А тип <A>(a: A, b: A) => A?

Ответы

1. Тип: A -> B -> A. По ABS: кладём x:A, потом y:B, тело x имеет тип A по VAR; собираем обратно B -> A, затем A -> B -> A. Это комбинатор K. Утверждает: «если A, то из B следует A» — истинное следует из чего угодно.

2. (A -> A) -> A -> A. Тело: f : A->A применяем к x : A → A; ещё раз к результату → A; ещё раз → A. Собираем: A -> A для внутренней λ, потом (A->A) -> A -> A. Это число Чёрча «три» с фиксированным A.

3. Пусть x : A. Тело x x — аппликация, значит левый x обязан быть стрелкой: A = P -> Q. Правый x — аргумент типа A, а вход функции — P, значит A = P. Подставляем: A = A -> Q. Раскручиваем: A = (A -> Q) -> Q = ((A -> Q) -> Q) -> Q = ... — бесконечный тип. Occurs check не проходит, решения нет.

4. Все шаги:

Шаг 0.  (λf:(A->A). λx:A. f (f x)) g w                            : A
Шаг 1.  подставляем f := g
        → (λx:A. g (g x)) w                                       : A
Шаг 2.  подставляем x := w
        → g (g w)                                                 : A
Шаг 3.  редексов больше нет — g свободная переменная.
Нормальная форма: g (g w), тип A.

Тип A на каждом шаге — Preservation в чистом виде.

5.

const applyTo = <A, B>(a: A) => (f: (a: A) => B): B => f(a);

def apply_to(a):
    return lambda f: f(a)      # A -> ((A -> B) -> B)

Утверждает: «если A истинно, то из “A влечёт B” следует B». При B = ЛОЖЬ это превращается в A -> Not(Not(A)) — введение двойного отрицания. Обратите внимание: эта половина конструктивна, а обратная (Not(Not(A)) -> A) нет.

6. (A -> B -> C) -> B -> A -> C — это перестановка посылок: «если из A и B следует C, то из B и A следует C». Коммутативность конъюнкции в посылках. Тривиально верно и в классической, и в интуиционистской логике.

7. Either<A, Not<A>> — закон исключённого третьего. Чтобы его населить, надо для произвольного, ничего о себе не сообщающего A выбрать конкретную ветку — информации для выбора нет. А вот Not<Not<Either<A, Not<A>>>> населяется:

const nnLem = <A>(k: Not<Either<A, Not<A>>>): never =>
  k({ tag: "right", value: (a: A) => k({ tag: "left", value: a }) });

Читается так: «предполагая, что LEM ложен, приходим к противоречию». Двойное отрицание LEM конструктивно доказуемо — это частный случай трансляции Гливенко: любая классическая теорема становится интуиционистской, если навесить на неё двойное отрицание.

8. <A, B>(a: A, b: A) => A — ровно одна: вернуть a. Ничего другого с параметрами сделать нельзя. <A>(a: A, b: A) => A — ровно две: вернуть a или вернуть b. Число обитателей типа — это, между прочим, число различных доказательств соответствующего утверждения; конечность здесь не случайна.

Мини-итог

• Типизированное лямбда-исчисление добавляет к термам аннотации и три правила вывода — VAR, ABS, APP. Правило APP запрещает применять функцию к аргументу неподходящего типа.
• Типизированные программы обладают Preservation (тип не меняется при редукции) и Progress (не застревают). Вместе — типобезопасность.
• Цена — сильная нормализация: любой терм λ→ завершается, а значит, Ω, Y и вообще самоприменение непредставимы. Полнота по Тьюрингу возвращается через fix или рекурсивные типы — но вместе с зависаниями.
• Соответствие Карри-Ховарда: типы — утверждения, программы — доказательства, вычисление — упрощение доказательства. Не аналогия, а изоморфизм структур.
• Функции соответствуют импликации, пары — конъюнкции, размеченные объединения — дизъюнкции, пустой тип — лжи, дженерики — кванторам. Классических законов (LEM, снятие двойного отрицания, закон Пирса) в чистом виде нет — они появляются вместе с операторами управления.
• Практические следствия: параметричность и «теоремы задаром», проверка полноты через never, системы интерактивных доказательств, зависимые типы.
• Лямбда-куб задаёт три оси расширения: полиморфизм, конструкторы типов, зависимые типы. Чем выразительнее система, тем труднее вывод.

Глубже про формальную сторону — трек mathematics (логика, вычислимость, конструктивизм). Практическое применение типов в повседневном коде — треки functional-programming и typescript.

Источники:

• Benjamin C. Pierce, Types and Programming Languages — cis.upenn.edu/~bcpierce/tapl
• Philip Wadler, Propositions as Types — homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types
• Philip Wadler, Theorems for Free! (1989) — pdf
• Timothy Griffin, A Formulae-as-Types Notion of Control (POPL 1990) — dl.acm.org/doi/10.1145/96709.96714
• Software Foundations — softwarefoundations.cis.upenn.edu
• Stanford Encyclopedia of Philosophy, Intuitionistic Logic — plato.stanford.edu/entries/logic-intuitionistic

Что дальше

Мы прошли путь от трёх правил синтаксиса до систем, на которых верифицируют компиляторы. Осталось замкнуть круг и посмотреть, как всё это выглядит в языках, которыми вы пользуетесь: откуда в Lisp появились лямбды, почему map и filter устроены именно так, что общего у => в JavaScript и λ Чёрча, и какие идеи трека прямо сейчас работают в вашем редакторе.

Лямбда-исчисление в живых языках: от Lisp до современных стрелочных функций