Вывод типов при вызове обобщенных методов с лямбдами и перегрузкой функций: различия между версиями
Материал из Вики проекта PascalABC.NET
Перейти к навигацииПерейти к поиску
Mikst (обсуждение | вклад) |
Mikst (обсуждение | вклад) |
||
| Строка 9: | Строка 9: | ||
Имеется множество ограничений на типы C, записываемое в виде равенств вида: | Имеется множество ограничений на типы C, записываемое в виде равенств вида: | ||
C { S<sub>i</sub> = T<sub>i</sub> } | |||
Требуется найти для этого множества ограничений наиболее общий '''унификатор'''. | Требуется найти для этого множества ограничений наиболее общий '''унификатор'''. | ||
'''Унификатором''' множества ограничений | '''Унификатором''' множества ограничений | ||
C | C { S<sub>i</sub> = T<sub>i</sub> } | ||
называется типовая подстановка σ, такая что для каждого уравнения | называется типовая подстановка σ, такая что для каждого уравнения | ||
| Строка 26: | Строка 22: | ||
σ(S) = σ(T) | σ(S) = σ(T) | ||
'''Пример 1.''' | |||
C { X = int, Y = X→X } | |||
Нетрудно видеть, что типовая подстановка σ имеет вид: | |||
[ X --> int, Y --> int → int ] | |||
'''Пример 2.''' | |||
C { X = Y→X } | |||
Поскольку X находится и в левой и в правой части, то решения (подстановки) нет. | |||
Версия от 19:13, 25 июня 2014
Алгоритм Хиндли-Милнера
Алгоритм Хиндли-Милнера предназначен для вывода типов при наличии ограничений
Для компиляции он важен когда мы выводим типы параметров в вызове обобщенной функции, при этом в качестве параметров фигурируют ляибда-выражения.
Алгоритм Хиндли-Милнера описан в Пирсе, с.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 находится и в левой и в правой части, то решения (подстановки) нет.
