Сильный вывод типов: Хиндли — Милнер

Главная суперсила OCaml: статическая типизация без единой аннотации типа благодаря алгоритму Хиндли — Милнера.

Вывод типов (type inference) — способность компилятора самостоятельно определить тип каждого выражения, не требуя писать типы вручную.

Многие думают, что статическая типизация — это компромисс: надёжность в обмен на многословие. OCaml показывает, что компромисса нет. Вы пишете код почти так же лаконично, как в Python, но получаете полную статическую проверку типов. Секрет — алгоритм Хиндли — Милнера (алгоритм W), который выводит типы автоматически.

Как это выглядит

utop # let double x = x * 2 ;;
val double : int -> int = <fun>

utop # let first (a, b) = a ;;
val first : 'a * 'b -> 'a = <fun>

В первом случае компилятор увидел x * 2, понял, что * работает с int, и заключил: double принимает int и возвращает int. Во втором — функция возвращает первый элемент пары, не глядя на содержимое, поэтому вывелся полиморфный тип 'a * 'b -> 'a: «для любых типов 'a и 'b».

Принцип: самый общий тип

Хиндли — Милнер выводит не какой-то тип, а самый общий (principal type) — наиболее полиморфный из возможных. Если функция не накладывает ограничений на тип аргумента, он останется переменной типа 'a. Значит, одну функцию можно применять к разным типам без перегрузок и шаблонов.

utop # let id x = x ;;
val id : 'a -> 'a = <fun>

utop # id 5 ;;
- : int = 5
utop # id "текст" ;;
- : string = "текст"

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

Алгоритм действует в два этапа. Первый — сбор ограничений. Компилятор присваивает каждому подвыражению свежую переменную типа и обходит дерево, выписывая уравнения. Второй — унификация. Алгоритм решает эту систему, подставляя одни типы в другие, пока не останется согласованное решение. Если уравнения противоречивы (нужно, чтобы узел был и int, и string), компилятор сообщает об ошибке типа — ещё до запуска. Унификация гарантирует, что найденное решение — самое общее.

(* Схема вывода для  let f x = x +. 1.0  *)
x        : 'a              (* свежая переменная *)
(+.)     : float -> float -> float
=>  'a = float             (* унификация *)
=>  f : float -> float

Когда аннотации всё же нужны

Аннотации помогают в трёх случаях: зафиксировать публичный интерфейс модуля, разрешить неоднозначность при работе с записями с одинаковыми именами полей, и получить более понятное сообщение об ошибке. Синтаксис — (выражение : тип):

let square (x : float) : float = x *. x

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

Ожидать перегрузку как в C++/Java. В OCaml нет перегрузки по типам: + только для int, +. только для float.
Считать 'a «любым типом во время выполнения». Это не Object: тип фиксируется в каждой точке применения при компиляции.
Удивляться «слишком общему» типу. Значит, вы не использовали операцию, ограничивающую тип.

Итоги

Алгоритм Хиндли — Милнера выводит типы автоматически, без аннотаций.
Выводится самый общий (полиморфный) тип; неограниченные параметры остаются 'a.
Вывод работает через сбор ограничений и унификацию на этапе компиляции.