Проверка и вывод типов: системы типов, унификация, Хиндли-Милнер

В прошлой статье мы научили компилятор отвечать на вопрос «что означает это имя»: построили таблицу символов, разрешили области видимости, связали каждый Var с местом объявления. Теперь у нас есть AST, в котором нет висящих имён.

Но программа let x = 1; let y = true; x + y; проходит все предыдущие фазы без единой жалобы. Лексер выдал корректные токены, парсер построил дерево, резолвер нашёл оба объявления. И только на этапе выполнения окажется, что складывать число с булевым значением бессмысленно — либо рантайм упадёт, либо (что хуже) молча вернёт мусор.

Задача этой статьи — научиться отвечать на вопрос «имеет ли эта программа смысл» до запуска. Мы разберём, что такое система типов с точки зрения теории, напишем проверяющий алгоритм для Mini с аннотациями, а затем уберём аннотации и заставим компилятор выводить типы самостоятельно — через унификацию и алгоритм Хиндли — Милнера. К концу статьи fn(f, g) fn(x) f(g(x)) будет получать тип ('a -> 'b, 'c -> 'a) -> ('c -> 'b) без единой подсказки от программиста.

Что такое тип и зачем он компилятору

С первых принципов: тип — это конечное описание бесконечного множества значений плюс набор операций, которые над ними определены. Int — это «все целые числа, и над ними работают +, -, <». (Int) -> Bool — это «все функции, которые съедают целое и возвращают булево». Тип не описывает значение полностью (Int не говорит, что число положительное), он его аппроксимирует.

Аппроксимация — ключевое слово. Точный ответ на вопрос «упадёт ли эта программа» неразрешим (теорема Райса, см. вычислимость). Значит, любая система типов обязательно неточна. Выбор один: ошибаться в сторону лишних отказов (отвергать корректные программы) или в сторону пропусков (принимать падающие). Практически все статические системы типов выбирают первое и называются консервативными — они отвергают программы, которые «на самом деле» работали бы.

Классическая формулировка цели принадлежит Робину Милнеру (1978): «Well-typed programs cannot go wrong» — корректно типизированные программы не могут пойти вразнос. «Пойти вразнос» здесь — технический термин: означает застрять в состоянии, для которого не определён следующий шаг вычисления. Формально это разбивается на две теоремы:

• Progress (продвижение). Если $\vdash e : \tau$ и $e$ — не значение, то существует $e’$ такое, что $e \to e’$. Иначе говоря, типизированное выражение никогда не застревает.
• Preservation (сохранение). Если $\vdash e : \tau$ и $e \to e’$, то $\vdash e’ : \tau$. Вычисление не меняет тип.

Вместе они дают soundness (безопасность типов): типизированная программа либо считает вечно, либо приходит к значению правильного типа, но никогда не оказывается в состоянии «не знаю, что делать». Эта пара доказательств — стандарт для любого нового языка со времён работы Райта и Фелляйзена «A Syntactic Approach to Type Soundness» (1994).

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

Оси проектирования: как языки различаются

Четыре независимые оси, которые часто путают:

1. Статическая или динамическая. Когда проверяются типы — при компиляции или при исполнении. В Python типы есть, они просто проверяются в момент операции.
2. Сильная или слабая. Насколько система позволяет обойти себя. В C (int)ptr разрешено, в Haskell — нет (без unsafeCoerce). Ортогонально первой оси: Python динамический, но сильный.
3. Номинальная или структурная. Совпадают ли типы по имени (class Meters ≠ class Feet, даже если оба обёртки над float) или по структуре ({ x: number } совместим с { x: number, y: number }). Java номинальная, TypeScript и Go-интерфейсы — структурные.
4. Явная или выводимая. Пишет ли программист аннотации или компилятор их восстанавливает. Это и есть тема второй половины статьи.

Подробнее про то, как разные парадигмы обходятся с типизацией, — в статье «Обобщённое программирование и метапрограммирование».

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

Правила типизации: формальный язык для «это выражение корректно»

Компилятор не может рассуждать о типах словами. Ему нужны правила, машинно применимые к каждому узлу AST. Стандартная форма записи — суждение типизации (typing judgment):

$$\Gamma \vdash e : \tau$$

Читается: «в контексте $\Gamma$ выражение $e$ имеет тип $\tau$». Контекст $\Gamma$ — это в точности та таблица символов, которую мы построили на прошлом шаге, только вместо «где объявлено» она хранит «какого типа». Правила записываются дробью: над чертой — посылки, под чертой — вывод.

$$\dfrac{}{\Gamma \vdash n : \mathtt{Int}} \quad (\text{T-Int}) \qquad \dfrac{x : \tau \in \Gamma}{\Gamma \vdash x : \tau} \quad (\text{T-Var})$$

$$\dfrac{\Gamma \vdash e_1 : \mathtt{Int} \quad \Gamma \vdash e_2 : \mathtt{Int}} {\Gamma \vdash e_1 + e_2 : \mathtt{Int}} \quad (\text{T-Add}) \qquad \dfrac{\Gamma \vdash c : \mathtt{Bool} \quad \Gamma \vdash e_1 : \tau \quad \Gamma \vdash e_2 : \tau} {\Gamma \vdash \texttt{if } c \texttt{ then } e_1 \texttt{ else } e_2 : \tau} \quad (\text{T-If})$$

$$\dfrac{\Gamma, x : \tau_1 \vdash e : \tau_2} {\Gamma \vdash \texttt{fn}(x)\ e : \tau_1 \to \tau_2} \quad (\text{T-Abs}) \qquad \dfrac{\Gamma \vdash e_1 : \tau_1 \to \tau_2 \quad \Gamma \vdash e_2 : \tau_1} {\Gamma \vdash e_1(e_2) : \tau_2} \quad (\text{T-App})$$

Три наблюдения, из-за которых эта нотация стоит того, чтобы её выучить.

Первое. В T-If тип $\tau$ встречается три раза — в двух посылках и в выводе. Это и есть формальная запись требования «обе ветки одного типа», и именно из такого совпадения переменных в правиле потом родится унификация.

Второе. В T-Abs тип $\tau_1$ появляется в посылке из ниоткуда. При проверке его берут из аннотации, при выводе — придумывают свежую типовую переменную и надеются, что дальше она определится. Вся разница между checking и inference прячется в этой строчке.

Третье. Правила буквально совпадают с правилами натуральной дедукции из логики: T-Abs — это введение импликации, T-App — modus ponens. Это соответствие Карри — Ховарда: типы суть утверждения, программы суть доказательства (логика и доказательства, типизированное лямбда-исчисление).

Дерево вывода для fn(x) x + 1 читается снизу вверх — ровно так его и обходит рекурсивная функция проверки:

                        x : Int ∈ {x:Int}          
                       ─────────────── T-Var    ────────────── T-Int
   {x:Int} ⊢ x : Int                             {x:Int} ⊢ 1 : Int
   ────────────────────────────────────────────────────────────── T-Add
                     {x:Int} ⊢ x + 1 : Int
   ─────────────────────────────────────────── T-Abs
       {} ⊢ fn(x) x + 1 : Int -> Int

Представление типов в компиляторе

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

from dataclasses import dataclass
from itertools import count

class Type: pass

@dataclass
class TCon(Type):              # конструктор типа: Int, Bool, List[Int], Pair[A, B]
    name: str
    args: tuple = ()

@dataclass
class TFun(Type):              # функция; параметры списком — так проще с арностью
    params: list
    ret: Type

@dataclass(eq=False)           # eq=False: переменные сравниваем по identity!
class TVar(Type):
    id: int
    ref: Type = None           # подстановка живёт здесь, а не в отдельном словаре
    level: int = 0             # глубина let-вложенности, нужна для обобщения

T_INT, T_BOOL = TCon("Int"), TCon("Bool")

_ids = count(1)
def new_var(level: int) -> TVar:
    return TVar(next(_ids), None, level)

eq=False у TVar — не мелочь. Две разные типовые переменные с одинаковыми полями обязаны считаться разными; если оставить структурное сравнение датакласса, весь алгоритм тихо сломается.

Проверка типов: бидирекциональный алгоритм

Начнём с более простой задачи: программист пишет аннотации, компилятор их проверяет. Наивная реализация — одна функция «дай мне тип узла». Она ломается на первой же лямбде: чтобы вывести тип fn(x) x + 1, нужно знать тип x, а он ниоткуда не следует.

Правильный ответ, ставший индустриальным стандартом, — бидирекциональная типизация: не одна функция, а две, работающие в разных направлениях.

• synth(Γ, e) -> τ — синтез, тип рождается из самого выражения и едет наверх ($\Rightarrow$).
• check(Γ, e, τ) — проверка, ожидаемый тип спускается сверху и сверяется ($\Leftarrow$).

Распределение ролей простое и почти механическое: интродукции (лямбда, литерал списка, конструктор) идут в check — они не знают своего типа, но легко проверяются против заданного; элиминации (вызов, доступ к полю, применение оператора) идут в synth — тип извлекается из головы конструкции. Аннотация (e : τ) — единственный мост из check в synth, а правило смены режима (subsumption) — единственный мост обратно.

К узлам AST из прошлой статьи добавляем один — Ann(expr, ty) для записи (e : T); у Fn в этом разделе params — список пар (имя, аннотация | None), потому что аннотация каждого параметра необязательна. env здесь отображает имя прямо в тип, без схем: полиморфизма пока нет.

def synth(env, e):
    """Стрелка вверх: тип выводится из формы выражения."""
    match e:
        case Num():   return T_INT
        case Bool():  return T_BOOL
        case Var(n):
            if n not in env: raise TypeErr(f"неизвестное имя: {n}")
            return env[n]
        case Ann(expr, ty):                    # (e : T) — мост check -> synth
            check(env, expr, ty)
            return ty
        case Call(callee, args):               # элиминация: тип берём из головы
            ft = synth(env, callee)
            if not isinstance(ft, TFun):
                raise TypeErr(f"вызов не-функции: {show(ft)}")
            if len(ft.params) != len(args):
                raise TypeErr("неверное число аргументов")
            for a, pt in zip(args, ft.params):
                check(env, a, pt)              # аргументы — уже сверху вниз
            return ft.ret
        case Fn(params, body) if all(t is not None for _, t in params):
            inner = {**env, **{n: t for n, t in params}}
            return TFun([t for _, t in params], synth(inner, body))
        case Binary(op, l, r):
            lt, rt, res = BINOPS[op]
            check(env, l, lt); check(env, r, rt)
            return res
    raise TypeErr("не хватает аннотации: тип нельзя вывести из самого выражения")


def check(env, e, expected):
    """Стрелка вниз: ожидание известно, сверяем."""
    match e:
        case Fn(params, body):                 # интродукция: разбираем ожидание на части
            exp = expected
            if not isinstance(exp, TFun) or len(exp.params) != len(params):
                raise TypeErr(f"лямбда не подходит под {show(exp)}")
            inner = dict(env)
            for (n, ann), pt in zip(params, exp.params):
                if ann is not None and not eq_ty(ann, pt):
                    raise TypeErr(f"аннотация {show(ann)} не совпадает с ожидаемым {show(pt)}")
                inner[n] = pt                  # тип параметра приехал сверху — вот и всё
            return check(inner, body, exp.ret)
        case If(c, t, f):                      # обе ветки проверяются против одного ожидания
            check(env, c, T_BOOL)
            check(env, t, expected)
            check(env, f, expected)
            return
    got = synth(env, e)                        # правило смены режима
    if not eq_ty(got, expected):
        raise TypeErr(f"ожидался {show(expected)}, получен {show(got)}")

Прогон:

(fn(x) x + 1 : (Int)->Int)     : (Int) -> Int
apply(inc, 1)                  : Int
fn(x) x  без аннотации         ! не хватает аннотации: тип нельзя вывести из самого выражения
(fn(x) x + 1 : (Bool)->Int)    ! ожидался Int, получен Bool

Сложность. Каждый узел AST посещается ровно один раз, eq_ty сравнивает типы за время, линейное от их размера. Итого $O(n \cdot t)$ по времени, где $n$ — число узлов, $t$ — максимальный размер типа, и $O(d)$ по памяти на стек рекурсии ($d$ — глубина дерева). На практике $t$ мал и константен, так что проверка типов линейна — она не бывает узким местом компиляции.

Почему бидирекциональность выиграла отрасль? Три причины. Она тривиально расширяется: добавили подтипы, GADT, зависимые типы — правило смены режима остаётся точкой стыка. Она даёт локальные сообщения об ошибках: ожидание всегда известно, поэтому виноватый узел находится сразу. И она предсказуема для программиста: правило «аннотируй границы модулей и функций, внутри пиши без аннотаций» ровно про неё. Так устроены TypeScript, Scala 3, Rust внутри тел функций и локальный вывод в GHC. Каноничный обзор — Dunfield & Krishnaswami, «Bidirectional Typing» (ACM Computing Surveys, 2021).

Вывод типов: убираем аннотации

Аннотации утомляют. fn(f, g) fn(x) f(g(x)) имеет единственный разумный тип, и заставлять человека его выписывать — расточительство. Возникает вопрос: можно ли восстановить типы полностью автоматически?

Для просто типизированного лямбда-исчисления — да, и ответ был известен ещё Хиндли (1969). Ключевое понятие — главный тип (principal type): такой тип, что любой другой корректный тип выражения получается из него подстановкой. У fn(x) x главный тип — $\alpha \to \alpha$, а Int -> Int и Bool -> Bool — его частные случаи. Существование главного типа означает, что компилятору не нужно перебирать варианты: есть один максимально общий ответ, и алгоритм его найдёт.

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

Для fn(f, g) fn(x) f(g(x)) система выглядит так:

f : α          g : β          x : γ
из g(x):   β = γ -> δ         (δ — свежая, результат g)
из f(...): α = δ -> ε         (ε — свежая, результат f)
ответ:     (α, β) -> (γ -> ε)
подставив: (δ -> ε, γ -> δ) -> (γ -> ε)

Унификация

Унификация — задача из автоматического доказательства теорем: даны два терма с переменными, найти подстановку, делающую их синтаксически равными. Алгоритм предложил Джон Алан Робинсон в работе «A Machine-Oriented Logic Based on the Resolution Principle» (1965), эффективные варианты — Мартелли и Монтанари (1982) и Патерсон — Вегман (линейный, 1978).

Псевдокод, который стоит понять до строчки:

unify(a, b):
    a ← prune(a);  b ← prune(b)        # разыменовать уже связанные переменные
    если a и b — один и тот же объект: успех
    если a — переменная:
        occurs_check(a, b)             # a не должна встречаться внутри b
        a.ref ← b                      # СВЯЗЫВАНИЕ: подстановка записана
        успех
    если b — переменная: unify(b, a)   # симметрия
    если a = C(a1..an) и b = C(b1..bn):  # одинаковый конструктор и арность
        для i от 1 до n: unify(ai, bi)
    иначе: ОШИБКА «несовместимые типы»

Три места, где обычно ошибаются.

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

Второе: occurs check. Попытка унифицировать $\alpha$ с $\alpha \to \mathtt{Int}$ даёт бесконечный тип $((\ldots \to \mathtt{Int}) \to \mathtt{Int})$. Без проверки алгоритм построит циклический граф и зациклится при первой же печати типа. Классический источник — fn(x) x(x): терм, который в нетипизированном лямбда-исчислении прекрасно живёт (редукции), а в HM отвергается именно occurs check’ом. Интересно, что языки с рекурсивными типами (OCaml с флагом -rectypes) осознанно его отключают.

Третье: связывание необратимо. a.ref ← b — деструктивная операция без отката. Поэтому HM-вывод работает без бэктрекинга: любой найденный ответ окончателен. Это и источник скорости, и источник плохих сообщений об ошибках — к этому вернёмся.

Реализация — прямой перевод псевдокода:

def prune(t: Type) -> Type:
    """Разыменовать цепочку ref до конца, попутно сжав путь."""
    if isinstance(t, TVar) and t.ref is not None:
        t.ref = prune(t.ref)          # path compression
        return t.ref
    return t

def occurs_check_and_adjust(v: TVar, t: Type) -> None:
    """Проверить, что v не внутри t, и заодно опустить level переменных t."""
    t = prune(t)
    if t is v:
        raise TypeErr(f"бесконечный тип: {show(v)} входит в самого себя")
    if isinstance(t, TVar):
        t.level = min(t.level, v.level)   # см. раздел про уровни
    elif isinstance(t, TFun):
        for p in t.params:
            occurs_check_and_adjust(v, p)
        occurs_check_and_adjust(v, t.ret)
    elif isinstance(t, TCon):
        for a in t.args:
            occurs_check_and_adjust(v, a)

def unify(a: Type, b: Type) -> None:
    a, b = prune(a), prune(b)
    if a is b:
        return
    if isinstance(a, TVar):
        occurs_check_and_adjust(a, b)
        a.ref = b                      # подстановка = одно присваивание
        return
    if isinstance(b, TVar):
        return unify(b, a)
    if isinstance(a, TFun) and isinstance(b, TFun):
        if len(a.params) != len(b.params):
            raise TypeErr(f"разное число аргументов: {show(a)} и {show(b)}")
        for x, y in zip(a.params, b.params):
            unify(x, y)
        return unify(a.ret, b.ret)
    if isinstance(a, TCon) and isinstance(b, TCon) \
            and a.name == b.name and len(a.args) == len(b.args):
        for x, y in zip(a.args, b.args):
            unify(x, y)
        return
    raise TypeErr(f"несовместимые типы: {show(a)} и {show(b)}")

Сложность унификации. Наивная реализация с явным словарём подстановки и её применением ко всему терму — $O(n^2)$ и хуже. Вариант со ссылками, который выше, амортизированно $O(n \cdot \alpha(n))$ по времени — практически линеен. Ловушка — occurs check: он обходит весь терм, и если делать его на каждом связывании честно, худший случай снова квадратичен. Промышленные компиляторы либо откладывают occurs check (OCaml проверяет отложенно), либо используют пометки посещённых узлов. Память — $O(n)$ на сами узлы типов плюс $O(d)$ на рекурсию.

Хиндли — Милнер: полиморфизм, который вкручивается в let

Унификации достаточно для просто типизированного языка. Но она недостаточна для такого кода:

let id = fn(x) x in
    if id(true) then id(1) else id(2)

Если у id один-единственный тип $\alpha \to \alpha$, то первое использование свяжет $\alpha = \mathtt{Bool}$, а второе упадёт. Между тем программа очевидно корректна. Нужен полиморфизм: id должна иметь не тип, а схему типа $\forall \alpha.\ \alpha \to \alpha$, из которой на каждом использовании выдаётся свежая копия.

Милнер (1978) и затем Дамас с Милнером (1982, «Principal type-schemes for functional programs») нашли точку, в которой полиморфизм можно ввести, не потеряв разрешимость вывода. Точка эта — let. Отсюда термин let-полиморфизм и два ключевых оператора:

• generalize (обобщение) — на let превратить тип в схему, навесив $\forall$ на те типовые переменные, которые «принадлежат» только этому определению.
• instantiate (конкретизация) — на каждом упоминании имени заменить квантифицированные переменные схемы на свежие.

$$\dfrac{\Gamma \vdash e_1 : \tau_1 \quad \Gamma, x : \mathrm{gen}(\Gamma, \tau_1) \vdash e_2 : \tau_2} {\Gamma \vdash \texttt{let } x = e_1 \texttt{ in } e_2 : \tau_2} \quad (\text{T-Let})$$

Разница с обычным связыванием принципиальна: в T-Abs параметр лямбды получает монотип, в T-Let имя получает схему. Поэтому

let id = fn(x) x in id(id)(1)          -- корректно, тип Int
(fn(id) id(id)(1))(fn(x) x)            -- ошибка: бесконечный тип

Один и тот же по смыслу код принимается или отвергается в зависимости от того, let это или применение лямбды. Это самая известная асимметрия HM, и она следствие теоремы: вывод для полного System F (полиморфизм где угодно) неразрешим — доказал Уэллс в 1994. let — ровно та граница, до которой можно дойти, оставшись автоматическим.

Как понять, какие переменные можно обобщать

Наивное правило: обобщить все свободные переменные типа. Оно неверно. Рассмотрим:

fn(x) let y = x in y

Тип x — свежая $\alpha$. Тип y — та же $\alpha$. Если обобщить её в схему $\forall \alpha.\ \alpha$, получится, что y имеет любой тип, и функция типизируется как $\alpha \to \beta$ — заведомая дыра в безопасности. Правильное правило: обобщать можно только те переменные, которые не свободны в окружении $\Gamma$:

$$\mathrm{gen}(\Gamma, \tau) = \forall \bar{\alpha}.\ \tau, \quad \bar{\alpha} = \mathrm{ftv}(\tau) \setminus \mathrm{ftv}(\Gamma)$$

Буквальная реализация требует обходить всё окружение на каждом let — это $O(|\Gamma|)$ на операцию и на глубоких вложенностях даёт квадратичное поведение. Дидье Реми предложил трюк с уровнями: каждая типовая переменная помнит глубину let-вложенности, на которой родилась; внутрь let заходим с level + 1; обобщать разрешено ровно те переменные, у которых level > текущего. Унификация обязана понижать уровень (это делает occurs_check_and_adjust), иначе переменная «убежит» из своей области. Получается тот же ответ за $O(1)$ проверки на переменную. Разбор с доказательством — у Олега Киселёва, «Efficient and Insightful Generalization»; именно так устроен typechecker OCaml.

@dataclass
class Scheme:
    vars: list      # квантифицированные переменные (forall)
    body: Type

def generalize(t: Type, level: int) -> Scheme:
    """Навесить forall на переменные, родившиеся глубже текущего уровня."""
    acc = []
    def walk(t):
        t = prune(t)
        if isinstance(t, TVar):
            if t.level > level and t not in acc:   # t not in acc — сравнение по identity
                acc.append(t)
        elif isinstance(t, TFun):
            for p in t.params: walk(p)
            walk(t.ret)
        elif isinstance(t, TCon):
            for a in t.args: walk(a)
    walk(t)
    return Scheme(acc, t)

def instantiate(s: Scheme, level: int) -> Type:
    """Свежая копия схемы: forall a. a -> a  =>  'n -> 'n со свежей 'n."""
    if not s.vars:
        return s.body                       # мономорфный случай — копировать нечего
    m = {id(v): new_var(level) for v in s.vars}
    def copy(t):
        t = prune(t)
        if isinstance(t, TVar):
            return m.get(id(t), t)          # свободные переменные окружения не трогаем
        if isinstance(t, TFun):
            return TFun([copy(p) for p in t.params], copy(t.ret))
        return TCon(t.name, tuple(copy(a) for a in t.args))
    return copy(s.body)

Алгоритм W целиком

Теперь infer — обход AST, на каждом узле применяющий соответствующее правило типизации. Обратите внимание, насколько код структурно повторяет формальные правила: это не совпадение, а прямая трансляция.

BINOPS = {
    "+": (T_INT, T_INT, T_INT),   "-": (T_INT, T_INT, T_INT),
    "*": (T_INT, T_INT, T_INT),   "/": (T_INT, T_INT, T_INT),
    "<": (T_INT, T_INT, T_BOOL),  ">": (T_INT, T_INT, T_BOOL),
    "&&": (T_BOOL, T_BOOL, T_BOOL), "||": (T_BOOL, T_BOOL, T_BOOL),
}

def infer(env: dict, e, level: int = 0) -> Type:
    match e:
        case Num():                                   # T-Int
            return T_INT
        case Bool():
            return T_BOOL
        case Var(name):                               # T-Var + instantiate
            if name not in env:
                raise TypeErr(f"неизвестное имя: {name}")
            return instantiate(env[name], level)
        case Fn(params, body):                        # T-Abs: параметры мономорфны
            # аннотации здесь уже не нужны: params — просто список имён
            pts = [new_var(level) for _ in params]
            inner = dict(env)
            for p, t in zip(params, pts):
                inner[p] = Scheme([], t)              # пустой forall = монотип
            return TFun(pts, infer(inner, body, level))
        case Call(callee, args):                      # T-App через уравнение
            ft = infer(env, callee, level)
            ats = [infer(env, a, level) for a in args]
            rt = new_var(level)
            unify(ft, TFun(ats, rt))                  # "callee обязан быть такой функцией"
            return rt
        case If(c, t, f):                             # T-If: три уравнения
            unify(infer(env, c, level), T_BOOL)
            tt = infer(env, t, level)
            ff = infer(env, f, level)
            unify(tt, ff)
            return tt
        case Binary(op, l, r):
            lt, rt, res = BINOPS[op]
            unify(infer(env, l, level), lt)
            unify(infer(env, r, level), rt)
            return res
        case Let(name, value, body):                  # T-Let: обобщение
            vt = infer(env, value, level + 1)         # внутрь — на уровень глубже
            return infer({**env, name: generalize(vt, level)}, body, level)
        case LetRec(name, value, body):               # рекурсия: имя видно внутри себя
            self_t = new_var(level + 1)
            inner = {**env, name: Scheme([], self_t)} # ВНУТРИ — мономорфно!
            vt = infer(inner, value, level + 1)
            unify(self_t, vt)
            return infer({**env, name: generalize(self_t, level)}, body, level)
    raise TypeErr(f"не умею выводить тип для {e}")

Ключевая тонкость в LetRec: внутри собственного тела рекурсивное имя связано мономорфно, и только снаружи обобщается. Если разрешить полиморфное использование внутри — это называется полиморфной рекурсией — вывод становится неразрешимым (Kfoury, Tiuryn, Urzyczyn, 1993). Поэтому Haskell требует явную сигнатуру для полиморфно-рекурсивных функций, и это не каприз, а следствие теоремы.

Прогон (show печатает свежие переменные как 'a, 'b, …):

fn(x) x                            : ('a) -> 'a
fn(f,g) fn(x) f(g(x))              : (('a) -> 'b, ('c) -> 'a) -> ('c) -> 'b
let id = fn(x) x in id(id)(1)      : Int
(fn(id) id(id)(1))(fn(x) x)        ! бесконечный тип: 'a входит в самого себя
fn(b) if b then 1 else 2           : (Bool) -> Int
1 + true                           ! несовместимые типы: Bool и Int
fn(x) x(x)                         ! бесконечный тип: 'a входит в самого себя
letrec fact = ... in fact          : (Int) -> Int
fn(x) let y = x in y               : ('a) -> 'a

Обратите внимание на предпоследнюю строку: fn(x) let y = x in y получил честный $\alpha \to \alpha$, а не дырявый $\alpha \to \beta$ — механика уровней сработала.

Сложность, границы и почему это всё равно быстро

Теоретическая оценка вывода в HM неприятна: задача DEXPTIME-полна. Доказал Хэрри Мэйрсон, «Deciding ML typability is complete for deterministic exponential time» (POPL 1990). Причина — не сам алгоритм, а размер ответа: тип может расти двойной экспонентой от длины программы. Классический пример на нашей же реализации:

let x1 = fn(y) pair(y, y) in
let x2 = fn(y) x1(x1(y)) in
let x3 = fn(y) x2(x2(y)) in ... in xN

Каждый следующий let возводит размер типа в квадрат. Замеры на коде из этой статьи:

Шестой шаг уже не помещается в память. Но программисты так не пишут: реальный код имеет ограниченную глубину вложенности let и ограниченный размер типов, поэтому на практике вывод ведёт себя как $O(n \cdot \alpha(n))$ — линейно. То же противоречие «страшная теория, приятная практика» встречается в SAT-решателях и в анализе алиасов (оптимизации).

По памяти: $O(n)$ на узлы типов плюс размер окружения. Классическая ловушка реализации — копировать словарь окружения на каждом узле ({**env, ...}, как в коде выше). Для статьи это читаемо, для компилятора — $O(n^2)$; в проде используют персистентные отображения или стек с откатом (персистентные структуры).

Где HM ломается в реальных языках

Чистый HM красив, но ни один промышленный язык не реализует его в чистом виде. Разберём главные причины.

Изменяемое состояние ломает безопасность. Знаменитая дыра ML:

let r = ref []           (* по чистому HM: forall a. a list ref *)
let () = r := [1]        (* используем как int list ref *)
let b : bool = List.hd !r  (* и как bool list ref — segfault *)

Обобщение легально по правилу T-Let, но ячейка-то одна. Лечение — value restriction (Эндрю Райт, «Simple Imperative Polymorphism», 1995): обобщать разрешено только если правая часть let — синтаксическое значение (литерал, переменная, лямбда), а не вызов. ref [] — вызов, значит обобщения нет. Правило грубое, но работает и стоит в стандарте SML и в OCaml (с послаблением «relaxed value restriction»).

Подтипы плохо дружат с унификацией. Унификация решает уравнения $\tau_1 = \tau_2$, а подтипы требуют неравенств $\tau_1 \le \tau_2$. Это уже не унификация, а решение системы ограничений, и полный вывод для системы с подтипами и полиморфизмом снова неразрешим. Отсюда — компромиссы: TypeScript вообще не делает глобальный вывод, а комбинирует структурные подтипы с локальным бидирекциональным выводом; Scala 3 и Kotlin выводят типы только «снизу вверх» внутри выражений.

Перегрузка и классы типов. Что за тип у (+), если он работает и на Int, и на Double? Haskell отвечает $\forall a.\ \mathtt{Num}\ a \Rightarrow a \to a \to a$ — тип с ограничением. Вывод превращается в сбор ограничений и их отложенное решение. Современный GHC использует OutsideIn(X) (Vytiniotis, Peyton Jones, Schrijvers, Sulzmann, JFP 2011) — фреймворк, где сбор ограничений отделён от решателя. Расплата: при GADT и локальных равенствах типов вывод отказывается работать и требует сигнатуру.

Как это выглядит в конкретных языках:

Показательно: единственные языки с полным выводом — потомки ML. Как только в систему добавляют подтипы или перегрузку, вывод становится локальным. Это фундаментальный, а не инженерный предел.

Диагностика: почему сообщения вывода типов такие плохие

Знаменитая проблема HM: ошибка сообщается не там, где она сделана. Алгоритм идёт слева направо и падает на первом уравнении, которое не сошлось, — а виновата могла быть строка выше. В Haskell типичное «Couldn’t match expected type Int with actual type [Char]» указывает на последнее использование, а не на опечатку в определении.

Причины структурные:

1. Отсутствие бэктрекинга. Связывание переменной необратимо, поэтому алгоритм не может «передумать» и поискать другой источник конфликта.
2. Асимметрия обхода. Порядок унификации задаёт, какой из двух конфликтующих типов окажется «ожидаемым», а какой «полученным». Меняешь порядок — меняется формулировка ошибки.
3. Отсутствие привязки к исходнику. Типовая переменная не помнит, из какого узла AST родилась.

Что с этим делают на практике:

• Хранить происхождение (provenance). Каждая типовая переменная и каждое уравнение помнят спан токена, который их породил. Тогда можно сказать «Int пришёл отсюда, Bool — оттуда» и показать обе позиции. Это дорого по памяти, но GHC, Rust и Elm это делают.
• Отдавать предпочтение аннотациям. Если один из конфликтующих типов пришёл из явной аннотации, а другой выведен, «ожидаемым» назначают аннотацию — человек скорее ошибся в коде, чем в сигнатуре.
• Type error slicing. Вместо одной точки показать весь набор мест, участвовавших в противоречивом уравнении, и предложить убрать любое из них.
• Продолжать после ошибки. Подставить «тип-ошибку» в место сбоя и не считать его виновным дальше — иначе одна опечатка вызывает лавину сообщений. Приём тот же, что при восстановлении парсера в синтаксическом анализе.

Ориентир качества — сообщения компилятора Elm: подсветка обоих участков, человеческая формулировка, конкретное предложение по исправлению. Подробнее про эргономику ошибок — в статье «Проектирование языков и DSL».

Типичные ошибки реализации

Список собран из граблей, на которые наступают почти все, кто пишет свой typechecker.

1. Забыть prune. Сравниваете TVar, у которой уже есть ref, — получаете «переменную» там, где давно Int. Правило: каждая функция, работающая с типом, начинается с prune.
2. Структурное равенство у TVar. Датакласс по умолчанию сравнивает по полям; две разные переменные становятся «равными». Обязательно eq=False или явный __eq__ по identity.
3. Пропустить occurs check. Программа не упадёт сразу — она построит цикл в графе типов и зависнет при печати или при следующем обходе. Отладить это мучительно.
4. Обобщить переменные окружения. Разбирали выше: fn(x) let y = x in y мгновенно ловит такую ошибку, держите его в тестах.
5. Забыть понижать level в occurs check. Переменная «убегает» из области видимости и обобщается там, где не должна. Тест: fn(x) let f = fn(y) x in f.
6. Обобщать на letrec до унификации с телом. Обобщать нужно self_t после unify(self_t, vt), иначе рекурсивное имя получит слишком общую схему.
7. Копировать окружение на каждом узле. Читаемо, но квадратично. В проде — персистентная структура или стек областей видимости.
8. Терять позиции. Тип без спана исходника делает диагностику бесполезной. Спаны в узлы AST мы клали ещё в парсере — используйте их.
9. Считать проверку типов чистой функцией. Она мутирует ref и level. Значит, повторный прогон по тому же AST даст другой результат; в инкрементальных компиляторах и LSP это ловушка.

Что происходит с типами дальше

Вывод типов — не конец, а поставщик информации для всех последующих фаз. Из типизированного AST получают:

• Разрешение перегрузки и диспетчеризацию. Какой конкретно + вызывать, какой метод интерфейса. В Haskell это dictionary passing, в Rust — мономорфизация трейтов.
• Выбор представления данных. Int → машинное слово, Bool → байт, сумма типов → тег плюс полезная нагрузка. Дальше это станет разметкой в IR.
• Мономорфизацию против boxing. Один из главных архитектурных выборов: генерировать отдельный код на каждый набор типовых аргументов (быстро, раздувает бинарник — C++, Rust) или один код с указателями (компактно, медленнее — Java, Haskell, Go до 1.18; Go выбрал гибрид с GC-shape stenciling).
• Информацию для оптимизатора. Знание, что значение точно Int, снимает проверки в рантайме и разрешает арифметику без боксинга.
• Информацию для инструментов. «Показать тип под курсором» в LSP — это тот же самый typechecker, запущенный инкрементально (инструменты языка).

Мини-итог

• Система типов — автоматический доказыватель ограниченной теоремы о программе. Её корректность формализуется парой progress + preservation; неточность неизбежна по теореме Райса.
• Суждение $\Gamma \vdash e : \tau$ и правила-дроби — это не академическое украшение, а прямая спецификация кода: каждое правило превращается в ветку match.
• Бидирекциональная типизация делит работу между check (тип спускается) и synth (тип поднимается). Линейна, даёт локальные ошибки, легко расширяется — поэтому её выбрал мейнстрим.
• Вывод типов = собрать уравнения и решить их унификацией. Три обязательные детали: prune, occurs check, необратимость связывания.
• Хиндли — Милнер добавляет полиморфизм ровно в одном месте — в let, потому что дальше (System F) вывод неразрешим. Механика: generalize на let, instantiate на упоминании, уровни вместо обхода окружения.
• Теория говорит DEXPTIME, практика показывает линейность. Ломается HM на изменяемом состоянии (value restriction), подтипах и перегрузке — отсюда все компромиссы реальных языков.
• Плохие сообщения об ошибках — следствие устройства алгоритма, а не лени авторов. Лечится хранением происхождения типов и предпочтением аннотаций.

Что почитать

• Benjamin C. Pierce, Types and Programming Languages — страница книги. Главы 9, 11, 22 покрывают ровно материал статьи, с доказательствами.
• Robin Milner, «A Theory of Type Polymorphism in Programming», JCSS 1978 — оригинал алгоритма W.
• Luis Damas, Robin Milner, «Principal type-schemes for functional programs», POPL 1982 — доказательство главных типов.
• J. A. Robinson, «A Machine-Oriented Logic Based on the Resolution Principle», JACM 1965 — унификация.
• Jana Dunfield, Neel Krishnaswami, «Bidirectional Typing», 2021 — исчерпывающий обзор.
• Oleg Kiselyov, «Efficient and Insightful Generalization» — уровни Реми с кодом.
• Stephen Diehl, «Write You a Haskell: Hindley–Milner Inference» — HM на Haskell пошагово.
• rustc dev guide: Type Inference — как это устроено в продакшн-компиляторе.
• TypeScript Handbook: Type Inference — контрастный подход без HM.
• Связанные статьи портала: типизированное лямбда-исчисление — теоретический фундамент всей статьи; подстановка и захват переменных — та же механика, что в instantiate; логика и доказательства — правила вывода и Карри — Ховард; алгебраические типы и сопоставление с образцом — что типизировать дальше; система непересекающихся множеств — структура, на которой стоит быстрая унификация.

Что дальше

Типы проверены, программа объявлена осмысленной. Теперь пора перестать думать о ней как о дереве: AST удобен для анализа, но безнадёжен для оптимизаций и генерации кода. Следующая статья вводит средний слой компилятора — промежуточное представление: почему трёхадресный код удобнее дерева, что такое SSA-форма и φ-функции, зачем нужны базовые блоки и граф потока управления, и почему модель «песочные часы» (много языков → одно IR → много архитектур) победила в LLVM.

Промежуточное представление: IR, SSA, зачем нужен средний слой