Вывод типов при вызове обобщенных методов с лямбдами и перегрузкой функций: различия между версиями
Mikst (обсуждение | вклад) |
Mikst (обсуждение | вклад) |
||
(не показано 38 промежуточных версий этого же участника) | |||
Строка 143: | Строка 143: | ||
array of string ↪ IEn<X> | array of string ↪ IEn<X> | ||
X → IEn<Y> | l1 → l2 ↪ X → IEn<Y> | ||
Для отношения сопоставления фактических параметров формальным используем вместо равенства значок ↪ по направлению от фактического параметра к формальному. | |||
Это необходимо, поскольку равенство типов здесь получается лишь во втором случае, а в | |||
первом необходимо дополнительно проверять отношение наследования или реализации интерфейса. | |||
Второе соотношение дает уравнение | |||
X → IEn<Y> = l1 → l2 | |||
Рассмотрим первое соотношение. | |||
array of string ↪ IEn<X> | array of string ↪ IEn<X> | ||
Определим все интерфейсы, поддерживаемые array of string и выясним, есть ли среди них интерфейс IEn<Z> для некоторого типа Z | Определим все интерфейсы, поддерживаемые array of string и выясним, есть ли среди них интерфейс IEn<Z> для некоторого типа Z | ||
Такой запрос в .NET сделать можно. В данном случае ответ - да: array of string поддерживает в частности интерфейс IEn<string>. | Такой запрос в .NET сделать можно. В данном случае ответ - да: array of string поддерживает в частности интерфейс IEn<string>. | ||
Таким образом, | Генерируем отсюда уравнение: | ||
IEn<X> = IEn<string> | |||
Таким образом, получаем: | |||
IEn<X> = IEn<string> | |||
X → IEn<Y> = l1 → l2 | |||
Упрощаем: | |||
string | X = string | ||
X = l1 | X = l1 | ||
IEn<Y> = l2 | IEn<Y> = l2 | ||
Строка 183: | Строка 196: | ||
IEn<l3> = l2 | IEn<l3> = l2 | ||
Таким образом, X и Y выражены через конкретные типы или типы параметров лямбды или вспомогательные, и у нас остается система | Таким образом, X и Y выражены через конкретные типы или типы параметров лямбды или вспомогательные, и у нас остается система уравнений только относительно параметров лямбды и вспомогательных: | ||
l1 = string | l1 = string | ||
Строка 207: | Строка 220: | ||
array of string | array of string | ||
Заметим, что мы не можем написать для составного типа равенство и должны использовать значок ↪: | Заметим, что мы не можем написать для составного типа равенство и должны использовать тот же значок ↪ сопоставления фактического параметра формальному: | ||
array of string ↪ IEn<l3> | array of string ↪ IEn<l3> | ||
Этот значок означает, что array of string в качестве типа возвращаемого значения лямбды можно подставить вместо IEn<l3>. | Этот значок означает, что array of string в качестве типа возвращаемого значения лямбды можно подставить вместо формального параметра IEn<l3>. | ||
Получим отсюда дополнительное уравнение. Поскольку array of string реализует интерфейс IEn<string>, то | |||
IEn<l3> = IEn<string> | |||
Упрощаем: | |||
l3 = string | |||
Добавляем в систему: | Добавляем в систему: | ||
l1 = string | l1 = string | ||
l2 = IEn<l3> | l2 = IEn<l3> | ||
l3 = string | l3 = string | ||
В итоге получаем: | |||
l1 = string | l1 = string | ||
Строка 239: | Строка 250: | ||
Y = string | Y = string | ||
Все типы выведены - ура. | Все типы выведены - ура. Данные равенства по-существу задают подстановку, которая унифицирует нашу систему уравнений: | ||
σ [ X ↦ string, Y ↦ string, l1 ↦ string, l2 ↦ IEn<string> ] | |||
'''Замечание.''' Тип возвращаемого значения l2 лямбды можно сузить и положить равным array of string | '''Замечание.''' Тип возвращаемого значения l2 лямбды можно сузить и положить равным array of string | ||
'''Замечание.''' Для общности array of string можно записывать как Array<string> | |||
===Модифицированный алгоритм Хиндли-Милнера=== | |||
Алгоритм Хиндли-Милнера вывода типов и получения наиболее общего унификатора в своей основе имеет '''алгоритм унификации''', | Алгоритм Хиндли-Милнера вывода типов и получения наиболее общего унификатора в своей основе имеет '''алгоритм унификации''', | ||
рекурсивно вычисляющий подстановку. Базовый алгоритм описан в Пирсе на с.350. | рекурсивно вычисляющий подстановку. Базовый алгоритм описан в Пирсе на с.350. | ||
Строка 251: | Строка 264: | ||
Приведем его в нашем случае. | Приведем его в нашем случае. | ||
Пусть C - исходная система уравнений на типовые переменные, | Пусть X - типовая переменная, S,T - типовые выражения, V - вектор типовых переменных. | ||
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) | unify(C) | ||
Строка 260: | Строка 275: | ||
иначе | иначе | ||
{ | { | ||
Пусть { S = T } ∪ C' = C | Выделим из C первое уравнение: S = T. | ||
Пусть { '''S = T''' } ∪ C' = C | |||
Eсли S = T | |||
то return unify(C') | то return unify(C') | ||
если S = X и (X ∉ FV(T) или X на внешнем уровне является классом или интерфейсом) | если S = X и (X ∉ FV(T) или X на внешнем уровне является классом или интерфейсом) | ||
Строка 269: | Строка 285: | ||
если S = S1 → S2 и T = T1 → T2 | если S = S1 → S2 и T = T1 → T2 | ||
то return unify(C' ∪ {S1 = T1, S2 = T2}) | то return unify(C' ∪ {S1 = T1, S2 = T2}) | ||
Если S = C<V> и T = C1<V1> и С = С1 и |V| = |V1| | |||
то return unify(C' ∪ {V = V1}) | |||
return неудача | Если S = I<V> и T = I1<V1> и I = I1 и |V| = |V1| | ||
то return unify(C' ∪ {V = V1}) | |||
Если ни по одной ветке до этого не вышли | |||
то return неудача | |||
} | } | ||
После вывода всех типов их надо подставить во внешний контекст (в секцию where) и проверить, удовлетворяются ли эти условия |
Текущая версия от 14:22, 7 июля 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 (для удобства и без нарушения общности)
Попытаемся понять, какая здесь возникает система ограничений на типы, как их выводить в процессе унификации,
Система уравнений для типовых переменных и ее решение
Этап 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 = ∅ , то return [] иначе { Выделим из C первое уравнение: S = T. Пусть { S = T } ∪ C' = C Eсли S = T то return unify(C') если S = X и (X ∉ FV(T) или X на внешнем уровне является классом или интерфейсом) то return unify([X ↦ T]C')•[X ↦ T]) если T = X и (X ∉ FV(S) или X на внешнем уровне является классом или интерфейсом) // симметрично предыдущему то return unify([X ↦ S]C')•[X ↦ S]) если S = S1 → S2 и T = T1 → T2 то return unify(C' ∪ {S1 = T1, S2 = T2}) Если S = C<V> и T = C1<V1> и С = С1 и |V| = |V1| то return unify(C' ∪ {V = V1}) Если S = I<V> и T = I1<V1> и I = I1 и |V| = |V1| то return unify(C' ∪ {V = V1}) Если ни по одной ветке до этого не вышли то return неудача }
После вывода всех типов их надо подставить во внешний контекст (в секцию where) и проверить, удовлетворяются ли эти условия