我阅读了至少 20 篇文章并找到了一篇我可以使用的文章(Francois Pottier:存在子类型的类型推断:从理论到实践):
输入:
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。
如果可能,联合计算两个具体类型的公共子类型,例如,(Object, Serializable) == Object&Serializable, (Integer, String) == null。
Intersection 计算两个具体类型的最接近的超类型,例如,(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 是 (String, T); 案例 3 被激活。因为 Reflexives 是空的,所以 T 的 LowerBounds 设置为 String。不存在 T 的 UpperBounds,因此,TypeRelations 保持不变。
2.) rel 是 (Integer, T); 案例 3 再次被激活。Reflexives 仍然为空,T 的下限设置为 String 和 Integer 的交集,产生 Object,T 仍然没有上限,TypeRelations 没有变化
3.) rel 是 T >= U。案例 1 被激活。因为 Reflexives 是空的,所以 T 的 Upper Bounds 与 U 的 Upper bounds 结合在一起,U 仍然是空的。然后将下界 U 设置为下界 ot 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 是 T >= U。情况 2 被激活。该案例试图将 T 的上限(此时为 Object)与 Integer 联合,但失败且算法失败。
类型系统的扩展
向类型系统添加泛型类型需要在主要情况和 SubC 函数中进行扩展。
Type = { TypeVariable, ConcreteType, ParametricType<Type,...>)
一些想法:
- 如果 ConcreteType 和 ParametricType 相遇,那就是错误。
- 如果 TypeVariable 和 ParametricType 满足,例如 T = C(U1,...,Un) 则创建新的 Type 变量和关系为 T1 >= U1, ... , Tn >= Un 并使用它们。
- 如果两个 ParametricType 满足(D<> 和 C<>)检查是否 D >= C 并且类型参数的数量相同,然后将每一对提取为关系。