Вывод типов при вызове обобщенных методов с лямбдами и перегрузкой функций: различия между версиями
Mikst (обсуждение | вклад) |
Mikst (обсуждение | вклад) |
||
Строка 36: | Строка 36: | ||
'''Пример 2.''' | '''Пример 2.''' | ||
C { X = | C { X = Y → X } | ||
Поскольку X находится и в левой и в правой части, то решения (подстановки) нет. | Поскольку X находится и в левой и в правой части, то решения (подстановки) нет. | ||
'''Пример 3.''' | '''Пример 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 называется подстановка σ такая что любой другой унификатор σ' имеет вид: | |||
σ' = γ • σ | |||
для некоторой подстановки γ. | |||
В данном примере | |||
γ = |
Версия от 19:35, 25 июня 2014
Алгоритм Хиндли-Милнера
Алгоритм Хиндли-Милнера предназначен для вывода типов при наличии ограничений
Для компиляции он важен когда мы выводим типы параметров в вызове обобщенной функции, при этом в качестве параметров фигурируют ляибда-выражения.
Алгоритм Хиндли-Милнера описан в Пирсе, с.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 называется подстановка σ такая что любой другой унификатор σ' имеет вид:
σ' = γ • σ
для некоторой подстановки γ.
В данном примере
γ =