java - JavaのHindley-Milnerアルゴリズム

Question

私はJavaで書かれた単純なデータフローベースのシステム（LabViewエディタ/ランタイムのように想像してください）に取り組んでいます。ユーザーはエディターでブロックを相互に接続でき、データフローグラフが正しいことを確認するために型推論が必要ですが、ほとんどの型推論の例は数学表記、ML、Scala、Perlなどで書かれています。 "。

Hindley-Milnerアルゴリズムについて読んだところ、実装できる良い例が記載されたこのドキュメントが見つかりました。これは、制約のようにT1=T2のセットで機能します。ただし、私のデータフローグラフは、制約のようにT1> = T2に変換されます（または、T2はT1、共分散、またはT1 <：T2を拡張します（さまざまな記事で見たように））。型変数（のようなジェネリック関数で使用される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 の記事を読み、使用できる記事を 1 つ見つけました (Francois Pottier: Type inference in present 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 のように、最初の型が 2 番目の型を拡張または等しい場合に、2 つの具象型について通知できます。

Union は、可能であれば、2 つの具象型の共通サブタイプを計算します。たとえば、(Object, Serializable) == Object&Serializable, (Integer, String) == null などです。

Intersection は、(List, Set) == Collection、(Integer, String) == Object など、2 つの具象型の最も近いスーパータイプを計算します。

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 は (文字列、T) です。ケース 3 がアクティブになります。Reflexives は空であるため、T の LowerBounds は String に設定されます。T の UpperBounds は存在しないため、TypeRelations は変更されません。

2.) rel は (整数、T) です。ケース 3 が再びアクティブになります。Reflexives はまだ空です。T の下限は String と Integer の交点に設定され、Object が生成されます。T の上限はまだなく、TypeRelations の変更もありません。

3.) rel は T >= U です。ケース 1 がアクティブになります。Reflexives は空であるため、T の Upper Bounds は U の Upper Bounds と結合され、空のままになります。次に、下限 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,...>)

いくつかのアイデア:

• ConcreteType と ParametricType が一致する場合、それはエラーです。
• TypeVariable と ParametricType が一致する場合、たとえば T = C(U1,...,Un) の場合、新しい Type 変数と関係を T1 >= U1, ... , Tn >= Un として作成し、それらを操作します。
• 2 つの ParametricType が一致する場合 (D<> と C<>)、D >= C であり、型引数の数が同じかどうかを確認し、各ペアをリレーションとして抽出します。

Answer 2

Hindley-Milnerアルゴリズムは、基本的に統合アルゴリズムです。つまり、変数を使用したグラフ方程式のグラフ同型を解くためのアルゴリズムです。

Hindley-Milnerはあなたの問題に直接当てはまりませんが、Google検索でいくつかのリードが見つかりました。例：「多形言語での語用論的サブタイピング」 、「名前の非等価性に基づくHindley/Milner型システムへのサブタイピング拡張を提示します...」。（私はそれを読んでいません。）

---

...ただし、ほとんどの型推論の例は、数学表記、ML、Scala、Perlなどで書かれていますが、私は「話しません」。

そのハードルを自分で乗り越えなければならないと思います。型理論と型チェックは基本的に数学的なものです...そして難しいです。あなたは言語を習得するためにハードヤードを置く必要があります。