Вывод типов при вызове обобщенных методов с лямбдами и перегрузкой функций
Материал из Вики проекта PascalABC.NET
Перейти к навигацииПерейти к поиску
Алгоритм Хиндли-Милнера
Алгоритм Хиндли-Милнера предназначен для вывода типов при наличии ограничений
Для компиляции он важен когда мы выводим типы параметров в вызове обобщенной функции, при этом в качестве параметров фигурируют ляибда-выражения.
Алгоритм Хиндли-Милнера описан в Пирсе, с.343 Его суть состоит в следующем. Имеется множество ограничений на типы C, записываемое в виде равенств вида:
C { Si = Ti }
Требуется найти для этого множества ограничений наиболее общий унификатор.
Унификатором множества ограничений
C { Si = Ti }
называется типовая подстановка σ, такая что для каждого уравнения
S = T
в множестве C выполняется
σ(S) = σ(T)
Пример 1.
C { X = int, Y = X→X }
Нетрудно видеть, что типовая подстановка σ имеет вид:
[ X --> int, Y --> int → int ]
Пример 2.
C { X = Y→X }
Поскольку X находится и в левой и в правой части, то решения (подстановки) нет.