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

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

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

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

Алгоритм Хиндли-Милнера описан в Пирсе, с.343.

Его суть состоит в следующем. 
Имеется множество ограничений на типы C, записываемое в виде равенств вида:

 C { S<sub>i</sub> = T<sub>i</sub> }

Требуется найти для этого множества ограничений наиболее общий '''унификатор'''. 

'''Унификатором''' множества ограничений 
 C { S<sub>i</sub> = T<sub>i</sub> } 
называется типовая подстановка σ, такая что для каждого уравнения 

 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 (для удобства и без нарушения общности)

Попытаемся понять, какая здесь возникает система ограничений на типы, как их выводить в процессе унификации, 

====Система уравнений для типовых переменных и ее решение====
=====Этап 1. Без компиляции тела лямбды =====
Итак, сопоставляем фактические параметры формальным:

 array of string ↪ IEn<X>
 l1 → l2 ↪ X → IEn<Y>

Для отношения сопоставления фактических параметров формальным используем вместо равенства значок ↪ по направлению от фактического параметра к формальному. 
Это необходимо, поскольку равенство типов здесь получается лишь во втором случае, а в 
первом необходимо дополнительно проверять отношение наследования или реализации интерфейса.

Второе соотношение дает уравнение
 X → IEn<Y> = l1 → l2

Рассмотрим первое соотношение. 

 array of string ↪ IEn<X>

Определим все интерфейсы, поддерживаемые array of string и выясним, есть ли среди них интерфейс IEn<Z> для некоторого типа Z
Такой запрос в .NET сделать можно. В данном случае ответ - да: array of string поддерживает в частности интерфейс IEn<string>.
Генерируем отсюда уравнение:

IEn<X> = IEn<string>


Таким образом, получаем:

 IEn<X> = IEn<string>
 X → IEn<Y> = l1 → l2

Упрощаем:

 X = string 
 X = l1 
 IEn<Y> = l2

Дальнейшее упрощение приводит к уравнениям: 

 X = string
 l1 = string 
 IEn<Y> = l2

Подстановка, которая приводит к такому упрощению, это разумеется

 σ [ X ↦ string, l1 ↦ string, l2 ↦ IEn<Y> ]

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

Заметим, что технологически на данном этапе нам удобно считать l1 и l2 известными и выразить X,Y через l1 и l2.
Это связано с тем, что вначале в компиляторе PascalABC.NET выполняется вывод типов X,Y обобщения SelectMany и только затем - вывод параметров лямбды.
Поэтому мы поступаем следующим образом: вводим вспомогательный типовый параметр l3 и получаем:

 X = string
 Y = l3 
 l1 = string 
 IEn<l3> = l2

Таким образом, X и Y выражены через конкретные типы или типы параметров лямбды или вспомогательные, и у нас остается система уравнений только относительно параметров лямбды и вспомогательных:

 l1 = string 
 IEn<l3> = l2

Данный этап закончен. Не привлекая тип тела лямбды, ничего получить нельзя.

=====Этап 2. Компиляция тела лямбды =====

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

Для нее и вычислим тип тела лямбды. Если он не может быть вычислен с этими типами параметров лямбды, то - ошибка.
В данном случае лямбда имеет вид:

 x->x.Split()

и на данный момент известно, что

 x: string

Поэтому тип возвращаемого значения лямбды вычисляется однозначно:

 array of string

Заметим, что мы не можем написать для составного типа равенство и должны использовать тот же значок ↪ сопоставления фактического параметра формальному:

 array of string ↪ IEn<l3>

Этот значок означает, что array of string в качестве типа возвращаемого значения лямбды можно подставить вместо формального параметра IEn<l3>.
Получим отсюда дополнительное уравнение. Поскольку array of string реализует интерфейс IEn<string>, то
 IEn<l3> = IEn<string>

Упрощаем:
 l3 = string

Добавляем в систему: 
 l1 = string 
 l2 = IEn<l3>
 l3 = string

В итоге получаем: 

 l1 = string 
 l2 = IEn<string>
 l3 = string

Теперь вернемся к X и Y и вспомним, что  Y = l3. В итоге получим:

 l1 = string 
 l2 = IEn<string>
 l3 = string
 X = string
 Y = string 

Все типы выведены - ура. Данные равенства по-существу задают подстановку, которая унифицирует нашу систему уравнений:

 σ [ X ↦ string, Y ↦ string, l1 ↦ string, l2 ↦ IEn<string> ]

'''Замечание.''' Тип возвращаемого значения l2 лямбды можно сузить и положить равным array of string

'''Замечание.''' Для общности array of string можно записывать как Array<string>

===Модифицированный алгоритм Хиндли-Милнера===
Алгоритм Хиндли-Милнера вывода типов и получения наиболее общего унификатора в своей основе имеет '''алгоритм унификации''',
рекурсивно вычисляющий подстановку. Базовый алгоритм описан в Пирсе на с.350.

Приведем его в нашем случае. 

Пусть X - типовая переменная, S,T - типовые выражения, V - вектор типовых переменных. 

==== Алгоритм унификации====
Пусть C - исходная система уравнений на типовые переменные, X - типовая переменная, S,T - типовые выражения, V - вектор типовых выражений (например, для List<IEn<T>,List<int>> V = (IEn<T>,List<int>)), функция unify(C) возвращает подстановку. Обозначим также через FV(T) множество типовых переменных в типе T.

 unify(C) 
 {
   если C = &empty; , то 
     return []
   иначе 
   {
     Выделим из C первое уравнение: S = T. 
     Пусть { '''S = T''' } &cup; C' = C
     Eсли S = T
      то return unify(C')
     если S = X и (X &notin; FV(T) или X на внешнем уровне является классом или интерфейсом)
      то return unify([X ↦ T]C')•[X ↦ T])
     если T = X и (X &notin; FV(S) или X на внешнем уровне является классом или интерфейсом) // симметрично предыдущему
      то return unify([X ↦ S]C')•[X ↦ S])
     если S = S1 → S2 и T = T1 → T2
       то return unify(C' &cup; {S1 = T1, S2 = T2})
     Если S = C<V> и T = C1<V1> и С = С1 и |V| = |V1| 
       то return unify(C' &cup; {V = V1})
     Если S = I<V> и T = I1<V1> и I = I1 и |V| = |V1| 
       то return unify(C' &cup; {V = V1})
     Если ни по одной ветке до этого не вышли
       то return неудача
   }

После вывода всех типов их надо подставить во внешний контекст (в секцию where) и проверить, удовлетворяются ли эти условия