Java中的Milner算法
我正在研究一个简单的基于数据流的系统（想象它像一个LabView编辑器/运行库），用Java编写。 用户可以在编辑器中将块连接在一起，我需要类型推断来确保数据流图是正确的，但是，大多数类型推断示例都是用数学符号ML，Scala，Perl等编写的，我不会“说” ”。
我阅读了Hindley-Milner算法，并找到了一个我可以实现的很好的例子。 它适用于一组类似T1 = T2的约束。 但是，我的数据流图像翻译为T1> = T2（如我在各篇文章中看到的那样）约束条件（或T2延伸T1或协方差或T1 <：T2）。 没有lambda只是类型变量（用于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的例子或解释将不胜感激。
我阅读了至少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。
如果可能，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是（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被激活。 由于反身是空的，T的上界与U的上界相结合，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是T> = U。情况2被激活。 该案例试图将T的上界（这是此时的对象）与整数联合，失败并且算法失败。
类型系统的扩展
向类型系统添加泛型类型需要在主要情况和SubC函数中使用扩展。
Type = { TypeVariable, ConcreteType, ParametricType<Type,...>)
一些想法：
Hindley-Milner算法基本上是一种统一算法，即用于求解带有变量的图方程的图同构的算法。
Hindley-Milner并不直接适用于您的问题，但谷歌搜索遇到了一些线索; 例如“多态语言中的语用分型”，其中说：“我们提出了基于名称不等式的Hindley / Milner类型系统的子类型扩展......”。 （我没看过。）
...但是，大多数类型推理示例都是用数学符号ML，Scala，Perl等编写的，我不会“说”。
我想你将不得不克服这个障碍。 类型理论和类型检查从根本上说是数学上的...而且很困难。 你需要在艰难的场地中选择语言。
链接地址: http://www.djcxy.com/p/80881.html