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

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

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

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

Алгоритм Хиндли-Милнера описан в Пирсе, с.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.