Java中的Hindley-Milner算法

Question

我正在开发一个用Java语言编写的基于数据流的简单系统(想象一下，它就像一个LabView编辑器/运行时)。用户可以在编辑器中将块连接在一起，我需要类型推断来确保数据流图是正确的，但是，大多数类型推断示例都是用数学符号、ML、Scala、Perl等编写的，我不会“说”这些符号。

我读到了Hindley-Milner算法，找到了一个我可以实现的很好的例子的this文档。它适用于一组T1 = T2 like约束。但是，我的数据流图转换为类似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式的例子或解释将不胜感激。

Answer 1

我读了至少20篇文章，找到了一篇我可以使用的文章(Francois Pottier: Type inference in presence of subtyping: from theory to practice)：

输入：

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) ==集合，(Integer，String) ==对象。

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)；Case 3被激活。因为反射为空，所以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的上限与U的上限结合在一起，U的上限保持为空。然后，将下界U设置为T的下界，产生对象反射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的上限(此时是对象)与Integer合并，这将失败，算法也会失败。

类型系统的扩展

将泛型类型添加到类型系统中需要在主实例和SubC函数中进行扩展。

Type = { TypeVariable, ConcreteType, ParametricType<Type,...>)

一些想法：

• 如果ConcreteType和ParametricType相遇，这是错误的。
• 如果TypeVariable和ParametricType相遇，例如T= C(U1，...，Un)，则创建新的类型变量和关系作为T1 >= U1，...，Tn >= Un并使用它们。
• 如果两个ParametricType相遇(D<>和C<>)检查D >= C和类型参数的数量是否相同，则提取每一对作为关系。

Answer 2

Hindley-Milner算法本质上是一种统一算法，即求解带有变量的图方程的图同构的算法。

Hindley-Milner并不直接适用于你的问题，但是谷歌搜索发现了一些线索；例如"Pragmatic Subtyping in Polymorphic Languages"，它说“我们给Hindley/Milner类型系统提供了一个基于名称不等价的子类型扩展……”。(我还没读过。)

...然而，大多数类型推断示例都是用数学符号、ML、Scala、Perl等编写的，我不会“讲”这些符号。

我认为你必须自己克服这个障碍。类型理论和类型检查基本上是数学上的.也很难。你需要付出艰苦的努力来学习这门语言。