Я прочитал не менее 20 статей и нашел одну (Франсуа Поттье: Вывод типа при наличии подтипов: от теории к практике), которую я мог бы использовать:
Ввод:
Type = { TypeVariable, ConcreteType }
TypeRelation = { Left: Type, Right: Type }
TypeRelations = Deque<TypeRelation>
Вспомогательные функции:
ExtendsOrEquals = #(ConcreteType, ConcreteType) => Boolean
Union = #(ConcreteType, ConcreteType) => ConcreteType | fail
Intersection = #(ConcreteType, ConcreteType) => ConcreteType
SubC = #(Type, Type) => List<TypeRelation>
ExtendsOrEquals может рассказать о двух конкретных типах, если первый расширяет или равен второму, например, (String, Object) == true, (Object, String) == false.
Union вычисляет общий подтип двух конкретных типов, если это возможно, например, (Object, Serializable) == Object & Serializable, (Integer, String) == null.
Пересечение вычисляет ближайший супертип двух конкретных типов, например, (List, Set) == Collection, (Integer, String) == Object.
SubC - это функция структурной декомпозиции, котораяв этом простом случае просто вернет одноэлементный список, содержащий новое отношение TypeRelation его параметров.
Структуры отслеживания:
UpperBounds = Map<TypeVariable, Set<Type>>
LowerBounds = Map<TypeVariable, Set<Type>>
Reflexives = List<TypeRelation>
UpperBounds отслеживает типы, которые могут быть супертипами переменной типа,LowerBounds отслеживает типы, которые могут быть подтипами переменной типа.Reflexives отслеживает отношения между переменными типа пар, чтобы помочь в переопределении границ алгоритма.
Алгоритм выглядит следующим образом:
While TypeRelations is not empty, take a relation rel
[Case 1] If rel is (left: TypeVariable, right: TypeVariable) and
Reflexives does not have an entry with (left, right) {
found1 = false;
found2 = false
for each ab in Reflexives
// apply a >= b, b >= c then a >= c rule
if (ab.right == rel.left)
found1 = true
add (ab.left, rel.right) to Reflexives
union and set upper bounds of ab.left
with upper bounds of rel.right
if (ab.left == rel.right)
found2 = true
add (rel.left, ab.right) to Reflexives
intersect and set lower bounds of ab.right
with lower bounds of rel.left
if !found1
union and set upper bounds of rel.left
with upper bounds of rel.right
if !found2
intersect and set lower bounds of rel.right
with lower bounds of rel.left
add TypeRelation(rel.left, rel.right) to Reflexives
for each lb in LowerBounds of rel.left
for each ub in UpperBounds of rel.right
add all SubC(lb, ub) to TypeRelations
}
[Case 2] If rel is (left: TypeVariable, right: ConcreteType) and
UpperBound of rel.left does not contain rel.right {
found = false
for each ab in Reflexives
if (ab.right == rel.left)
found = true
union and set upper bounds of ab.left with rel.right
if !found
union the upper bounds of rel.left with rel.right
for each lb in LowerBounds of rel.left
add all SubC(lb, rel.right) to TypeRelations
}
[Case 3] If rel is (left: ConcreteType, right: TypeVariable) and
LowerBound of rel.right does not contain rel.left {
found = false;
for each ab in Reflexives
if (ab.left == rel.right)
found = true;
intersect and set lower bounds of ab.right with rel.left
if !found
intersect and set lower bounds of rel.right with rel.left
for each ub in UpperBounds of rel.right
add each SubC(rel.left, ub) to TypeRelations
}
[Case 4] if rel is (left: ConcreteType, Right: ConcreteType) and
!ExtendsOrEquals(rel.left, rel.right)
fail
}
Базовый пример:
Merge = (T, T) => T
Sink = U => Void
Sink(Merge("String", 1))
Отношения этого выражения:
String >= T
Integer >= T
T >= U
1.) Rel is (String, T);Случай 3 активирован.Поскольку Reflexives пусто, для LowerBounds of T задано значение String.Верхних границ для T нет, поэтому TypeRelations остаются без изменений.
2.) Rel is (Integer, T);Случай 3 снова активирован.Reflexives по-прежнему пустые, нижняя граница T установлена на пересечении String и Integer, что дает Object, все еще нет верхних границ для T и никаких изменений в TypeRelations
3.) Rel is T> = U.Случай 1 активирован.Поскольку Reflexives пусто, верхние границы T объединяются с верхними границами U, который остается пустым.Затем нижние границы U устанавливаются в нижние границы T, что дает Object> = U. TypeRelation (T, U) добавляется к Reflexives.
4.) Алгоритм завершается.Из границ Object> = T и Object> = U
В другом примере демонстрируется конфликт типов:
Merge = (T, T) => T
Sink = Integer => Void
Sink(Merge("String", 1))
Отношения:
String >= T
Integer >= T
T >= Integer
Шаги 1.) и 2.) такие же, как указано выше.
3.) Rel is T> = U. Случай 2 активирован.В этом случае делается попытка объединить верхнюю границу T (в данном случае это Object) с Integer, что приводит к сбою и сбою алгоритма.
Расширения к системе типов
Добавление общих типов в систему типов требует расширения в основных случаях и в функции SubC.
Type = { TypeVariable, ConcreteType, ParametricType<Type,...>)
Некоторые идеи:
- Если встречаются ConcreteType и ParametricType,это ошибка.
- Если встречаются TypeVariable и ParametricType, например, T = C (U1, ..., Un), то создайте новые переменные типа и отношения как T1> = U1, ...,Tn> = Un и работать с ними.
- Если два ParametricType встречаются (D <> и C <>), проверьте, совпадают ли D> = C и количество аргументов типа, затем извлеките каждую пару как отношения.