java - Java 中的 Hindley-Milner 算法

Question

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

我阅读了 Hindley-Milner 算法并找到了 this文档中有一个我可以实现的很好的例子。它适用于一组类似 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 示例或解释。

Answer 1

我至少阅读了 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 计算两个具体类型的公共(public)子类型，例如，(Object, Serializable) == Object&Serializable, (Integer, String) == null。

交集计算两个具体类型的最近父类(super class)型，例如，(List, Set) == Collection, (Integer, String) == Object。

SubC 是结构分解函数，在这个简单的例子中，它只会返回一个包含其参数的新 TypeRelation 的单例列表。

跟踪结构:

UpperBounds = Map<TypeVariable, Set<Type>>
LowerBounds = Map<TypeVariable, Set<Type>>
Reflexives = List<TypeRelation>

UpperBounds 跟踪可能是类型变量的父类(super class)型的类型，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 的上界与 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 的上界(此时为对象)与 Integer 结合，但失败了，算法也失败了。

类型系统的扩展

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

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

一些想法:

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