Система Хиндли — Милнера

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

Как удержать полиморфизм типов и не свалиться обратно в неразрешимость System F? Хиндли и Милнер решают это ограничением мест, где может стоять квантор, разнося типы на два этажа: внизу — монотипы $\tau$ — типы без кванторов: атомарные $\alpha$, применения конструкторов типов $C\,\tau_1 \ldots \tau_n$ (так строятся, например, списки и пары) и стрелки. Наверху — схемы (политипы) $\sigma$ — монотипы, накрытые сверху кванторами:

Кванторы разрешены только снаружи, в самом начале типа (пренексная форма): $\forall \alpha.\, \alpha$ $\to \alpha$ — законная схема, а $(\forall \alpha.\, \alpha \to \alpha)$ $\to \beta$ — уже нет: здесь квантор забрался внутрь, слева от стрелки. Разрешить такое — получить полную System F с неразрешимым выводом; запретить — потерять немного выразительности, но превратить вывод типов в алгоритм. Весь фокус HM — в этом ограничении.

Между этажами два перехода, рассмотрим оба. Вниз — инстанцирование (Inst): из схемы делают монотип $\sigma[\alpha := \tau]$, подставляя вместо связанной переменной любой монотип. Вверх — обобщение (Gen): если переменная $\alpha$ осталась в выведенном типе, но не встречается свободно ни в одном предположении контекста ($\alpha$ $\notin \mathrm{free}(\Gamma)$), то ничто снаружи её не ограничивает — на неё можно навесить квантор:

Зачем эти переходы, видно из правила для $\mathbf{let}$ — сердца всей системы. Связывая имя $x$ значением $e_0$, мы обобщаем его тип до схемы $\sigma$, а дальше каждое использование $x$ в теле $e_1$ инстанцирует эту схему заново и независимо от остальных:

У аргумента λ такой привилегии нет. Обобщение происходит только в правиле Let, а параметр функции в него не попадает: когда мы типизируем тело, функция ещё ни к чему не применена, и что придёт ей на вход — неизвестно; всё, что можно сделать, — выдать аргументу одну типовую переменную, общую для всех его использований в теле. Разница видна на двух почти одинаковых термах. Терм $\mathbf{let}\;id$ $= \lambda y.\,y\;\mathbf{in}\;(id\;\overline{3},\, id\;\mathbf{true})$ типизируется: $id$ связан через $\mathbf{let}$, обобщён до схемы $\forall\alpha.\,\alpha$ $\to\alpha$, и каждое из двух использований инстанцирует её своим типом. Терм $(\lambda id.\,(id\;\overline{3},\, id\;\mathbf{true}))\,(\lambda y.\,y)$ — тот же по смыслу — уже не типизируется: здесь $id$ — аргумент λ, схемы у него нет, а один монотип не может быть одновременно типом функции над числами и над булевыми значениями.

В Haskell аннотации типов, конечно, есть — сигнатуры можно (и принято) выписывать. Но они необязательны: даже если бы их не было вовсе, компилятор восстановил бы все типы сам — это делает алгоритм W (Дамас — Милнер). Он обходит терм, выдаёт каждому подвыражению свежую типовую переменную, а на каждой аппликации записывает уравнение: тип функции обязан быть стрелкой из типа аргумента в тип результата. Накопленные уравнения решает унификация Робинсона — механическое сопоставление двух типов: чтобы $\alpha$ $\to \beta$ совпало с $(\gamma\to\gamma)$ $\to \delta$, достаточно подстановки $\alpha :$ $= \gamma$ $\to\gamma$, $\beta :$ $= \delta$. Компилятору хватает голого кода:

compose f g x = f (g x)

-- вывод без единой подсказки:
-- compose :: (b -> c) -> (a -> b) -> a -> c

Теперь мы понимаем, почему не получается использовать комбинаторы $\mathrm{Y}$, $\Theta$ и $\mathrm{Z}$ в языке Haskell. Все они построены на самоаппликации $x\,x$ — попробуем вывести её тип. Пусть $x : \alpha$; раз $x$ применяется к самому себе, $\alpha$ обязан быть стрелкой из $\alpha$ в какой-то $\beta$ — получаем уравнение $\alpha$ $= \alpha$ $\to \beta$. Подставим правую часть вместо $\alpha$ — и $\alpha$ снова внутри: $(\alpha\to\beta)$ $\to\beta$, $((\alpha\to\beta)\to\beta)$ $\to\beta$, … — подстановка зацикливается, тип растёт до бесконечности. Именно это пресекает occurs check — запрет переменной встречаться в типе, который за неё подставляют: без рекурсивных типов у уравнения решения нет. Поэтому рекурсию в Haskell заводят примитивом $\mathtt{fix}$ и рекурсивными определениями.