我读了关于Hindley-Milner算法,并发现了一个很好的例子可以实现的this文档.它工作在一组T1 = T2的约束.然而,我的数据流图转换为T1> = T2像约束(或T2扩展T1或协方差,或T1 <= T2,我在各种文章中看到).没有lambdas只是输入变量(在泛型函数中使用,如T merge(T in1,T in2))和具体类型. 总结HM算法：
Type = {TypeVariable,ConcreteType}
TypeRelation = {LeftType,RightType}
Substitution = {OldType,NewType}
TypeRelations = set of TypeRelation
Substitutions = set of Substitution
1) Initialize TypeRelations to the constraints,Initialize Substitutions to empty
2) Take a TypeRelation
3) If LeftType and RightType are both TypeVariables or are concrete
types with LeftType <: RightType Then do nothing
4) If only LeftType is a TypeVariable Then
replace all occurrences of RightType in TypeRelations and Substitutions
put LeftType,RightType into Substitutions
5) If only RightType is a TypeVariable then
replace all occurrences of LeftType in TypeRelations and Substitutions
put RightType,LeftType into Substitutions
6) Else fail
如何改变原来的HM算法来处理这些关系而不是简单的平等关系？
Java-ish的例子或解释将不胜感激.
解决方法
输入：
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.
交点计算两个具体类型的最接近的超类型,例如(List,Set)== Collection,String)== Object.
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是(String,T);情况3被激活.因为反身是空的,所以T的LowerBounds设置为String.不存在T的UpperBounds,因此TypeRelations保持不变.
2.)rel是(整数,T);情况3再次被激活.反身仍然为空,T的下限设置为String和Integer的交集,产生Object,仍然没有T的上限,TypeRelations中没有更改
3.)rel是T> = U.情况1被激活.因为反身是空的,所以T的上限与U的上限相结合,这个上限保持为空.然后下限U被设置为下限t T,产生Object> = U.TypeRelation(T,U)被加到反射器.
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并联,失败并且算法失败.
类型系统的扩展
Type = { TypeVariable,ConcreteType,ParametricType<Type,...>)
一些想法：
>如果ConcreteType和ParametricType符合,那就是一个错误.>如果TypeVariable和ParametricType满足,例如T = C(U1,…,Un),则创建新的类型变量和关系,如T1> = U1,Tn> = Un并与它们一起工作.>如果两个ParametricType满足(D和C),则检查D> = C和类型参数的数量是否相同,然后提取每一对作为关系.
