Вывод типов: Hindley-Milner

Как Haskell понимает тип выражения без единой аннотации? За этим стоит алгоритм 1982 года - Algorithm W Дамаса-Милнера, - который до сих пор является основой вывода типов в Haskell, OCaml, Rust и десятках других языков.

• **Haskell / OCaml:** полный вывод типов - можно писать целые программы без аннотаций, компилятор выведет всё сам
• **Rust:** borrow checker использует унификацию для вывода времён жизни (lifetimes), а trait bounds расширяют HM constraints
• **TypeScript:** `const x = [1, 2, 3].map(n => n * 2)` - тип `number[]` выведен автоматически через flow-анализ, вдохновлённый HM

Hindley-Milner: алгоритм вывода типов без аннотаций

В 1969 году математик Дж. Роджер Хиндли доказал теорему о наиболее общем типе для комбинаторной логики. В 1978 году Робин Милнер независимо разработал систему типов ML с выводом и let-полиморфизмом. Алгоритм W - практическая реализация Милнера. Луис Дамас в 1982 году завершил формализацию. Hindley-Milner лежит в основе OCaml, Haskell, SML, Elm, F#, Rust (частично). TypeScript выбрал bidirectional type checking вместо HM из-за совместимости с JavaScript. Алгоритм позволяет писать код без единой аннотации типа и получать корректную типизацию - фундаментальный результат теории типов.

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

• Static vs Dynamic Typing

Unification - решение уравнений типов

Когда код пишете `f(x) = x + 1`, компилятор должен определить тип `f` без единой аннотации. Как? Он строит **уравнения типов** и решает их - точно так же, как код решаете систему уравнений в алгебре.

**Unification** (унификация) - это алгоритм нахождения подстановки (substitution), которая делает два типа равными. Если `τ₁ = α → Int` и `τ₂ = Bool → β`, то подстановка `{α ↦ Bool, β ↦ Int}` унифицирует их: оба становятся `Bool → Int`.

Формально, подстановка (substitution) - это отображение `S: TypeVar → Type`. Применение подстановки `S` к типу `τ` записывается как `S(τ)`. Унификация двух типов `τ₁` и `τ₂` ищет такую `S`, что `S(τ₁) = S(τ₂)`.

**Occurs check** - ключевая проверка при унификации. Если переменная `α` встречается внутри типа `τ`, то уравнение `α = τ` не имеет конечного решения. Например, `α = List α` потребовало бы бесконечный тип `List (List (List ...))`. Без occurs check алгоритм зациклится.

Let-полиморфизм

Рассмотрим функцию идентичности: `let id = λx.x`. Какой у неё тип? Она принимает что угодно и возвращает то же самое. Интуитивно тип - `∀a. a → a` (для любого типа `a`, принимает `a` и возвращает `a`). Это **полиморфный** тип.

Но полиморфизм возникает не везде. **Let-полиморфизм** (также Дамаса-Милнера) говорит: тип обобщается (generalization) только при `let`-привязке. Переменные, связанные через `λ`, остаются **мономорфными** внутри тела λ.

**Правило generalization:** после вывода типа `τ` для `let x = e`, все свободные переменные типов в `τ`, которые НЕ встречаются в окружении (context), обобщаются квантором `∀`. Так `id: α → α` становится `id: ∀α. α → α`.

Constraint Solving - генерация и решение ограничений

Вывод типов можно разделить на два этапа: **(1) генерация ограничений** (constraints) из выражения и **(2) решение** этих ограничений через унификацию. Такое разделение делает алгоритм модульным и расширяемым.

На первом этапе мы обходим AST выражения, назначаем свежие переменные типов и генерируем уравнения вида `τ₁ = τ₂`. На втором - последовательно унифицируем все уравнения, накапливая подстановку.

**Constraint-based подход** используется в современных компиляторах (GHC, OCaml, Rust) вместо чистого Algorithm W, потому что он лучше масштабируется: constraints можно собирать параллельно, а решать - в оптимальном порядке. Также ошибки типов становятся более информативными.

Algorithm W Дамаса-Милнера

**Algorithm W** - формальный алгоритм вывода типов, опубликованный Луисом Дамасом и Робином Милнером в 1982 году. Он объединяет генерацию constraints и unification в единую рекурсивную процедуру, обходящую AST выражения.

Ключевое свойство Algorithm W: он всегда находит **principal type** (наиболее общий тип). Если выражение имеет тип `Int → Int`, но также `∀a. a → a`, алгоритм вернёт `∀a. a → a` - любой другой допустимый тип является подстановкой principal type.

**Generalize** в Case 4 (Let) - это то, что отличает `let` от `λ`. Свободные переменные типов в `τ₁`, не встречающиеся в контексте `Γ`, обобщаются квантором `∀`. Именно поэтому `let id = λx.x` даёт полиморфный `∀a. a→a`, а `λf. f 1; f true` - ошибку.

Algorithm W используется (с расширениями) в **Haskell** (GHC - OutsideIn с type classes), **OCaml**, **Rust** (частично, с trait bounds), **F#**, **Elm**, **PureScript**. TypeScript вдохновлён HM, но использует структурную типизацию и bidirectional inference.

**Сложность Algorithm W:** O(n) в типичных случаях, но теоретически может быть экспоненциальным (DEXPTIME-complete). На практике это не проблема - патологические случаи требуют глубоко вложенных let-выражений, которые редко встречаются в реальном коде.

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

• **Unification** решает уравнения типов через подстановку - если `α = Int → β` и `β = Bool`, то `α = Int → Bool`
• **Occurs check** предотвращает бесконечные типы: `α = List α` не имеет конечного решения
• **Let-полиморфизм** обобщает типы только при `let`-привязке - λ-bound переменные остаются мономорфными
• **Algorithm W** рекурсивно обходит AST и гарантирует нахождение **principal type** - наиболее общего типа выражения
• Современные компиляторы используют **constraint-based** вариант HM для лучшей диагностики ошибок и расширяемости

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

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

• Системы типов — HM - конкретная система типов с полной инференцией; более сильные системы (System F, зависимые типы) требуют аннотаций
• Лямбда-исчисление — HM типизирует simply-typed λ-calculus с let-полиморфизмом - это формальная основа ML-семейства
• Generics и параметрический полиморфизм — Let-полиморфизм HM - это и есть параметрический полиморфизм; generics в Java/C# вдохновлены этой идеей

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

• Почему разработчики Hindley-Milner выбрали let-полиморфизм вместо полного полиморфизма System F? Какой компромисс за этим стоит?
• Если Algorithm W находит principal type, почему в реальном коде всё равно рекомендуют писать аннотации типов для top-level функций?
• TypeScript использует структурную типизацию и bidirectional inference вместо классического HM. Какие преимущества и недостатки это даёт по сравнению с OCaml/Haskell?

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

• plt-03-static-vs-dynamic
• plt-02-type-systems
• plt-05-gradual
• plt-07-algebraic-types
• alg-21-dp