Вывод типов при вызове обобщенных методов с лямбдами и перегрузкой функций

Алгоритм Хиндли-Милнера

Алгоритм Хиндли-Милнера предназначен для вывода типов при наличии ограничений

Для компиляции он важен когда мы выводим типы параметров в вызове обобщенной функции, при этом в качестве параметров фигурируют ляибда-выражения.

Алгоритм Хиндли-Милнера описан в Пирсе, с.343.

Его суть состоит в следующем. Имеется множество ограничений на типы C, записываемое в виде равенств вида:

C { Si = Ti }

Требуется найти для этого множества ограничений наиболее общий унификатор.

Унификатором множества ограничений

C { Si = Ti } 

называется типовая подстановка σ, такая что для каждого уравнения

S = T 

в множестве C выполняется

σ(S) = σ(T)

Напомним, что для типовой подстановки выполняется

σ(X → Y) = σ(X) → σ(Y)

Примеры

Пример 1.

C { X = int, Y = X → X } 

Нетрудно видеть, что типовая подстановка σ имеет вид:

[ X --> int, Y --> int → int ]

Пример 2.

C { X = Y → X }

Поскольку X находится и в левой и в правой части, то решения (подстановки) нет.

Пример 3.

C { X = Y → Z, Y = Z → X }

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

X = (Z → X) → Z

Поскольку X находится и в левой и в правой части, то решения (подстановки) нет.

Пример 4.

C { int → Z = X → Y }

Подстановка

σ' [ X --> int, Y --> bool, Z --> bool ]

превращает равенство в C в тождество и потому является унификатором. Но она не является наиболее общим унификатором. В данном случае наиболее общим унификатором является подстановка

σ [ X --> int, Y --> Z ]

Определение. Наиболее общим унификатором системы типовых уравнений C называется подстановка σ такая что любой другой унификатор σ' имеет вид:

σ' = γ • σ 

для некоторой подстановки γ.

В данном примере

γ = [ Z --> bool ]

Ограничения равенства при компиляции

Откуда берутся ограничения равенства при компиляции дженериков?

Рассмотрим конкретный пример

Пусть определена функция

p<X,Y>(f: X → Y, z: X)

и мы вызываем

p(x->x*x,3)

Тогда уравнения для типов возникают при сопоставлении формальных и фактических параметров.

Поскольку у лямбды типы параметров и возвращаемого значения не определены, то будем нумеровать их l1,l2 и т.д. Таким образом, тип лямбды в нашем случае - l1 → l2

Итак, в результате сопоставления формальных и фактических параметров получаем систему типовых уравнений C:

{ X → Y = l1 → l2, X = int } (*)

Нам надо вывести все неизвестные: X,Y,l1,l2, выразив их через известные типы

Упрощаем:

{ X = l1, Y = l2, X = int }

Итак, X выражено через конкретный тип, и мы можем подставить его в остальные уравнения:

{ l1 = int, Y = l2, X = int }

Таким образом, мы получили подстановку

σ[ l1 --> int, Y --> l2, X --> int ]

которая унифицирует нашу систему уравнений (*)

Заметим, что тип l2 мы пока не вывели и пока не задействовали еще одно условие - тело лямбды. Итак, если какие-то типовые переменные остались не выведены, то необходимо задействовать тело лямбды. Как?

Напомним, что λ-выражение

x->x*x

имеет тип

l1 → l2

причем уже получено, что l1=int

Принимая это предположение, выводим тип тела лямбды: x*x: int Отсюда получаем недостающее равенство:

{ l1 = int, l2 = int, Y = int, X = int }

и соответствующую подстановку