我读了至少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可以告诉两个具体类型，如果第一个扩展或等于第二个，例如，（字符串，对象）==true，（对象，字符串）==false。
如果可能的话，联合计算两个具体类型的通用子类型，例如，（Object，Serializable）==Object&Serializable，（Integer，String）==null。
交集计算两种具体类型的最接近的超类型，例如，（列表，集合）==集合，（整数，字符串）==对象。
SubC 是结构分解函数，在这个简单的情况下，它将只返回一个包含其参数的新 TypeRelation 的单例列表。
跟踪结构：
UpperBounds = Map<TypeVariable, Set<Type>>
LowerBounds = Map<TypeVariable, Set<Type>>
Reflexives = List<TypeRelation>
UpperBounds 跟踪类型，这些类型可能是类型变量的超类型，LowerBounds 跟踪可能是类型变量的子类型的类型。自反函数跟踪对类型变量之间的关系，以帮助算法的边界重写。
算法如下：
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 为空，因此 T 的下限设置为 String。不存在 T 的上限，因此，类型关系保持不变。
2.） rel is （Integer， T）;案例 3 再次激活。自反义仍然是空的，T的下限设置为字符串和整数的交集，产生对象，T仍然没有上限，类型关系也没有变化
3.） rel 是 T >= U.案例 1 被激活。因为自反是空的，所以 T 的上限与 U 的上限相结合，U 的上限保持为空。然后将下限 U 设置为下限 ot T，得到对象 >= U。TypeRelation（T， U） 是 Reflexives 的附加项。
4.） 算法终止。从边界开始，对象 >= T 和对象 >= 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）与整数合并，该整数失败且算法失败。
类型系统的扩展
将泛型类型添加到类型系统在主情况和 SubC 函数中需要扩展。
Type = { TypeVariable, ConcreteType, ParametricType<Type,...>)
一些想法：
- 如果具体类型和参数类型相遇，则这是一个错误。
- 如果 TypeVariable 和 ParametricType 相遇，例如 T = C（U1,...,Un），则创建新的 Type 变量和关系，如 T1 >= U1， ... ， Tn >= Un 并使用它们。
- 如果两个参数类型满足 （D<> 和 C<>），请检查 D >= C 以及类型参数的数量是否相同，然后将每对提取为关系。
