Вывод типов при вызове обобщенных методов с лямбдами и перегрузкой функций: различия между версиями
Mikst (обсуждение | вклад) |
Mikst (обсуждение | вклад) |
||
Строка 138: | Строка 138: | ||
Попытаемся понять, какая здесь возникает система ограничений на типы, как их выводить в процессе унификации, | Попытаемся понять, какая здесь возникает система ограничений на типы, как их выводить в процессе унификации, | ||
====Система уравнений для типовых переменных==== | |||
Итак, сопоставляем фактические параметры формальным: | Итак, сопоставляем фактические параметры формальным: | ||
Версия от 22:05, 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 называется подстановка σ такая что любой другой унификатор σ' имеет вид:
σ' = γ • σ
для некоторой подстановки γ.
В данном примере
γ = [ 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 }
и соответствующую подстановку.
Реальный пример
Пример 5. В коде .NET в качестве типов (будем обозначать их буквами X,Y) могут быть:
- типовые переменные
- конкретные именованные типы (int, double)
- типы вида C<X> или I<X> (C - имя класса, I - имя интерфейса)
- функциональные типы X → Y
Приведем реальный пример с типами третьего вида.
var a: array of string; SelectMany(a,x->x.Split());
Функция SelectMany имеет следующий прототип:
SelectMany<X,Y>(a: IEn<X>,f: X → IEn<Y>): IEn<Y>;
Здесь IEn - это IEnumerable и метод расширения SelectMany записан не в принятом в .NET виде
a.SelectMany(x->x.Split());
а с переносом объекта, вызвавшего SelectMany в качестве первого параметра SelectMany (для удобства и без нарушения общности)
Попытаемся понять, какая здесь возникает система ограничений на типы, как их выводить в процессе унификации,
Система уравнений для типовых переменных
Итак, сопоставляем фактические параметры формальным:
array of string = IEn<X> X → IEn<Y> = l1 → l2
Здесь особое внимание обратим на первое равенство. Конечно, в виде равенства это соотношение записывать нельзя = мы записали так по аналогии с предыдущим.
Используем вместо равенства значок ~:
array of string ~ IEn<X> X → IEn<Y> = l1 → l2
Определим все интерфейсы, поддерживаемые array of string и выясним, есть ли среди них интерфейс IEn<Z> для некоторого типа Z Такой запрос в .NET сделать можно. В данном случае ответ - да - array of string поддерживает в частности интерфейс IEn<string> Таким образом, первое уравнение упрощается:
string = X X = l1 IEn<Y> ~ l2