Hindley-Milner型推論アルゴリズムをGroovyで書いてみた

こないだ「Haskellのforallについて理解したことを書いておく(ランクN多相限定)」の記事を書いたときにHindley-Milner型推論アルゴリズム*1を調査するにあたって、こちらにある「Scala by Example」の16章にあるScalaでの実装例をGroovyに書きなおしたので晒しておきます。

以下のような型検査・推論ができます。実行はできません。

def listLenTest = LetRec('len',
                         Lam('xs',
                             App(App(App(Var('if'),
                                         App(Var('isEmpty'), Var('xs'))),
                                     Var('zero')),
                                 App(Var('succ'),
                                     App(Var('len'),
                                         App(Var('tail'),
                                             Var('xs'))))
                                )),
                         App(Var('len'),
                             App(
                                 App(Var('cons'),
                                     Var('zero')),
                                 Var('nil'))
                            )
                        );
assert listLenTest.toString() == 'letrec len = λ xs . (((if (isEmpty xs)) zero) (succ (len (tail xs)))) in (len ((cons zero) nil))'
assert typeInfer.showType(listLenTest) == "Int[]"

型理論としてのHMを理論的に(型付ラムダ計算の定理の集合として)理解して実装しているわけではないのですが、先の「Scala By Example」の著者はScala開発者にしてJava Genericsの開発者、著名なる型理論学者Martin Odersky先生様その人ですので、プログラムの動作としてはまあ間違いはないと思っています。

コードから読み取ったことについて、多数のコメントを追記してあります。また、テストコードも追加したフルバージョンはこちらのgistにのせました。

Hindley-Milner型推論の特徴は、

• 双方向性。左辺・右辺の型、仮引数と実引数、宣言の型と使用側が期待する型、リターンしている型と返り値宣言の型、など、どっちかが決まれば、どっちかが決まるのだが、HMでは前後関係も関係なく、双方向で決まる。ここはScalaとかJava7/8とかGroovyの「型推論」と大きく異なる*2。
• 上の結果でもあるが、明示的な型宣言が(多くの場合?)不要*3。リテラルの型さえ決まっていれば、波及して型が決まる。矛盾があれば、エラーになる。字面上、明示された型指定が全く無いのに、例外無くすべて宣言されているのと同じように扱われる。もし決まらなければ(「\a->a」など)、自動的に多相型になる。
• 多相型に対応。つまり以下のコードはGenericsに対応している。こんな簡潔なコードなのに!!
• 多相型の解決と型推論の統合。つまり「型推論の開始時に未知の型」は、「多相型の型変数」と同じ枠組みで扱われて解決しようとする。
• 多相型の解決は識別子の使用を契機とするが、let変数とlambda変数では多相型解決についての意味上の違いがある。詳細はコメント参照。

でしょうかね。
Hindleyによって論文が書かれたのが1969年とのこと。なんかもう。

で、Groovy 2.1のカスタムタイプチェッカとしてHMを実装してみる野望(ゴゴゴゴ)*4

import groovy.transform.*
import static TypeInfer.typeInfer

@InheritConstructors
class TypeError extends Exception {}

/**
 * 構文木や式木をnewキーワード無しでオブジェクトを生成するために、
 * @Newify AST変換を適用するアノテーション@ApplyNewifyを定義する。
 *  @AnnotationCollectorは、Groovyの合成アノテーション作成機能。
 *  [annotations]* @AnnocationCollector @interface 新規アノテーション {}
 * で、[annotations]*を指定したのと等価な新規アノテーションを作成する。
 */
@Newify([Var,Lam,App,Let,LetRec,Tyvar,Arrow,Tycon])
@AnnotationCollector @interface ApplyNewify {}

/**
 * Termおよびそのサブクラスによって構文木を構成する項を定義する。
 * 項とは以下のいずれか。
 *   - 変数(Var)
 *   - λ抽象(Lambda)
 *   - 関数適用(App)
 *   - let式(Let)
 *   - letrec式(LetRec)
 * @Immutable AST変換を適用するとTupleConstructorと同様に、
 * メンバーを引数で初期化するコンストラクタが生成される。
 */
interface Term {}
@Immutable class Var implements Term { String x
    @Override String toString(){ x } }
@Immutable class Lam implements Term { String x; Term e
    @Override String toString(){ "λ $x . $e" } }
@Immutable class App implements Term { Term f; Term e
    @Override String toString(){ "($f $e)" } }
@Immutable class Let implements Term { String x; Term e; Term f
    @Override String toString(){ "let $x = $e in $f" } }
@Immutable class LetRec implements Term { String x; Term e; Term f
    @Override String toString(){ "letrec $x = $e in $f" } }

/**
 * Typeおよびそのサブクラスによって式木の構成要素を定義する。
 * 型とは以下のいずれか。
 *  - 型変数(Tyvar)
 *  - 関数型(Arrow)
 *  - 型コンストラクタ呼び出し(Tycon)(具体型)
 * 型変数を含む型を多相型と呼ぶ。
 */
interface Type {}
@Immutable class Tyvar implements Type { String a
    @Override String toString(){ a } }
@Immutable class Arrow implements Type { Type t1; Type t2
    @Override String toString(){ "($t1 -> $t2)" } }
@Immutable class Tycon implements Type { String k; List<Type> ts = []
    @Override String toString(){ k + "[${ts.join(',')}]" } }

/**
 * Substは「型に含まれる型変数の置換処理」を表わす。
 * Subst represent a step of substitution of type variables of polymorphic type.
 *
 * Substはcallメソッドが定義されているので、Subst(のサブクラス)のイ
 * ンスタンスに対して関数のように呼び出すことができる(Groovyの機能)。
 * 例えばx = new Subst(); x(..)と呼べるということ。
 * 2種類の引数の型に対してcallが定義されている。
 * 
 *  - call(Type)
 *    型中に含まれる型変数を置換する。
 *  - call(Env)
 *    Envに含まれるすべての型スキーマに含まれる型変数を置換したEnvを返す。
 * 
 * 実装機構としては、Substのサブクラスのインスタンス1つは、「Innerクラ
 * ス→内部クラスを含むOuterクラスのインスタンス」、それをまた含む
 * Outerクラス…というチェインを構成する。そのチェインは複数の置換処理
 * を連鎖である。callはOuterクラスのcallを呼び、という再帰処理が行なわ
 * れるので、複数の置換が適用できる。Innerクラスのインスタンスを作成す
 * るには、extendを呼ぶ。
 */
@ApplyNewify
abstract class Subst {
    /**
     * 指定した型変数の置換結果を返す。
     * SubstのOuter/Innerクラス関係から構成されるチェインを辿って探す。
     */
    protected abstract Type lookup(Tyvar x)
    abstract String toString()

    /**
     * 型Type t中に含まれる型変数を置換した結果の型を返す。
     * 型に含まれる型変数(つまり多相型の型変数)の変数を、変化しなく
     * なるまでひたすら置換する。置換の結果がさらに置換可能であれば、
     * 置換がなされなくなるまで置換を繰り返す。(循環参照の対処はさ
     * れてないので現実装は置換がループしてないことが前提)。
     */
    Type call(Type t) {
        switch (t) {
        case Tyvar: def u = lookup(t); return (t == u) ? t : call(u)
            // TODO: this code could throw stack overflow in the case of cyclick substitution.
        case Arrow: return Arrow(call(t.t1), call(t.t2))
        case Tycon: return Tycon(t.k, t.ts.collect{owner.call(it)})
        }
    }

    /**
     * 環境Env eに含まれるすべての型スキーマに含まれる型変数を置換した
     * Envを返す。
     */
    Env call(Env env) {
        env.collectEntries { String x, TypeScheme ts ->
            // assumes tyvars don't occur in this substitution
            def tmp = new TypeScheme(ts.tyvars, owner.call(ts.tpe))
            [x, tmp]
        }
    }

    /**
     * Innerクラスのインスタンスを生成する操作がextend()であり、「1つの
     * 型変数を一つの型へ置換」に対応するインスタンス1つを返す。ただし
     * extendで生成されたインスタンスは、extendを呼び出した元のオブジェ
     * クト(extendにとってのthisオブジェクト) =Outerクラスのインスタン
     * スとチェインしており、さらにcallにおいて、Outerクラスを呼び出し
     * て実行した置換の結果に対して追加的に置換を行うので、元の置換に対
     * して「拡張された置換」になる。
     */
    Subst extend(Tyvar x, Type t) {
        new Subst() {
            Type lookup(Tyvar y) {
                if (x == y) t else Subst.this.lookup(y)
            }
            String toString() {
                Subst.this.toString() + "\n$x = $t"
            }
        }
    }

    /**
     * 初期値としての空の置換を返す。
     * 任意のSubstインスタンスについて、OuterクラスのOuterクラスの…
     * という連鎖の最終端となる。
     */
    static final Subst emptySubst =  new Subst() {
        Type lookup(Tyvar t) { t }
        String toString() { "(empty)" }
    }
}

/**
 * TypeSchemeは、型抽象(∀X.T)を表わす。
 * 型抽象とは、「型引数」を引数に取り、型変数を含むテンプレートのよう
 * なものを本体とするような、λ式のようなもの。
 *
 * TypeSchemeはTypeを継承していない。その結果、Typeの構造の途中に
 * TypeSchemeが表われることもない。
 *
 * Haskellの「forall.」は型スキーマ(型抽象)に対応しているが、このHMアル
 * ゴリズムでは型スキーマ(抽象)はトップレベルの環境における識別子に直接
 * 結びつく形でしか存在しない。つまりランクN多相を許していない。
 *
 * もしTypeSchemeが型の一種であり、型構造の任意の部分に表われ得るなら
 * (つまりmgu()やtp()の型推定の解決対象の型コンストラクタなら)、ランク
 * N多相が実現されることになる。
 */
@Canonical
class TypeScheme {
    /**
     * tyvarsは型抽象において全称量化された型変数の集合を表す。
     * tyvars are set of universally quantified types in the type scheme.
     *
     * tyvarsは「その外側に対して名前が衝突しないことの保証」を持った型
     * 変数である。なぜなら型スキーマの使用に際してnewInstance()するこ
     * とでtpe中でのtyvars変数の使用がリネームされるからである。
     *
     * 具体的には、プログラム中にVar(x)の形で識別子xが使用されるとき、
     * 識別子xの型を得るために、環境に登録された「xに対応する型スキーマ」
     * を取得した上で、Type型に変換する処理(TypeScheme.newInstance())が
     * 行なわれる。newInstance()は、type中のtyvarsと同じ名前を持った変数
     * を、すべて重ならない新規の名前にリネーム置換したバージョンのtpe
     * を返す。
     */
    List<Tyvar> tyvars
    
    /**
     * 型のテンプレートを表わす。全称量化されている型変数と同じ型変数を
     * 含んでいれば、その型変数は、型スキーマがインスタンス化されるとき
     * に重ならない別名に置換される。
     */
    Type tpe

    /**
     * 型スキーマ(型抽象)を型に具体化する操作。
     *
     *    newInstance: TypeSchema → Type
     *
     * ちなみにgen()は反対に型から型スキーマを生み出す操作である。
     *
     *    gen: Type → TypeSchema
     * 
     * newInstance()は、全称限量指定された変数およびそれに束縛された変
     * 数(つまりフリー型変数を除いた全ての型変数)の使用を、新規の変数名
     * にリネームする。この操作の結果は、環境には左右されず、
     * TypeSchemeインスタンスのみの情報によって確定される。(変数名のシー
     * ドとなるtypeInfer.nの値には依存するが)
     * 
     * newInstance()の結果として得られる型には全称限量で指定されていた
     * 型変数は含まれない。たとえば、型スキーマ
     * 
     *    TypeSchema s = ∀ a,b . (a,b型を含む型)
     * 
     * に対して、newInstanceした結果は、
     * 
     *      s.newInstance() = (a',b'型を含む型)
     * 
     * であり、a,bは、a'b'に置換されるので、結果の型には決して現われな
     * い。
    */
    Type newInstance() {        
        tyvars.inject(Subst.emptySubst){ s, tv -> s.extend(tv, TypeInfer.instance.newTyvar())} (tpe)
    }
    String toString() { "∀ (${tyvars.join(',')}) . ($tpe)" }
}

/**
 * 環境Envは、プログラムのある位置における、識別子と型情報(型スキー
 * マ)の対応表である。
 * Env is map of identifier to type schema.
 * 環境Envは、意味的には型変数を含む制約の集合と見做すことができる。
 * Env can be regarded as set of constraints of relationships concerning
 * types include type variables. So HM type checker is constraints solver for it.
 * 環境は、tp()が解くべき、型方程式の制約条件を表現している。
 *     Env: 「プログラム中の識別子→型スキーマ」の対応の集合
 * 
 * ちなみに、Substもある種の対応表であるが、型変数の書き換えルールの
 * 集合。
 * 
 *     Subst: 「型変数→型(型変数|Arrow|Tycon)」という書き換え規則の集合
 * 
 * なお、明かにこの実装は空間効率が悪い。Scalaではタプルのリスト(連想リ
 * スト)で実現されていたところをGroovy化する際に、安易にMapにしてコピー
 * して受け渡すようにしたが、実用的には連想リストにすべき。
 */
@InheritConstructors
@ApplyNewify
class Env extends LinkedHashMap<String, TypeScheme> {
}

/**
 * TypeInferはHM型推論の全体を含む。Scalaではオブジェクトだったので、
 * @Singletonとして定義してある。サービスメソッドを呼び出すための静的
 * import可能な変数として、static typeInferを容易してある。
 * 型チェックの全体の流れは、
 *
 * showType ->  predefinedEnv
 *          ->  typeOf         ->    tp  ->  mgu
 *
 * である。
 */
@ApplyNewify
@Singleton
class TypeInfer {

    int n = 0
    def reset() {
        n = 0
    }
    
    /**
     * 名前が重ならない新規の型変数を作成する。
     */
    Type newTyvar() { Tyvar("a${n++}") }

    /**
     * 環境中にで定義された識別子xに対応する型スキーマを取得する。
     */
    TypeScheme lookup(Env e, String x) {
        return e.get(x)
    }

    /**
     * 型tに含まれているすべての型変数の集合(A)から、この環境に登録され
     * ているすべての型スキーマの「全称量化に関するフリー型変数の集合
     * (※1)」=(B)を除外したもの((A)-(B))を全称量化することで型スキーマ
     * を生成する。
     *
     * (※1)λx.yのとき変数xに束縛されていることを「λ束縛」と呼び、
     *     「λ束縛されていない変数」をフリー変数と呼ぶが、それと同様に、
     *     型変数に関する∀y...のとき型変数yに束縛されていることを「全
     *     称量化束縛」と呼び、「全称量化束縛」されていない型変数を「全
     *     称量化に関するフリー型変数」とする(ここで作った言葉)。
     *
     * 環境において「全称量化に関するフリー型変数」が発生するケースとい
     * うのは、具体的にはラムダ式
     *
     *    λ x . y
     *
     * において、識別子xに対応する型は、新規の型変数として環境に登録さ
     * れ、そのもとでyが型推論されるが、y解析中でのxの登場はスキーマ内
     * で全称量化されていない、という状態である。
     */
    TypeScheme gen(Env env, Type t) {
        new TypeScheme(tyvars(t) - tyvars(env), t)
    }

    /**
     * 型に対するtyvars()は、指定した型Type t中に含まれる型変数のリスト
     * を返す。
     */
    List<Tyvar> tyvars(Type t) {
        switch (t) {
        case Tyvar: return [t]
        case Arrow: return tyvars(t.t1) + tyvars(t.t2)
        // 型コンストラクタ T[a,b]のとき、Tは型変数ではない。
        case Tycon: return t.ts.inject([]) { List<Tyvar> tvs, Type elem -> tvs + tyvars(elem) }
        }
    }

    /**
     * 型スキーマに対するtyvars()は、指定した型スキーマTypeSchema tsの
     * 型テンプレート(ts.tpe)が使用している型変数から、全称量化された変
     * 数(ts.tyvars)を除外したものを返す。これは、何かというと、型スキー
     * マの型テンプレート(TypeSchema.tpe)が含む「全称量化に関するフリー
     * 型変数)の集合」である。
     */
    List<Tyvar> tyvars(TypeScheme ts) {
      tyvars(ts.tpe) - ts.tyvars
    }

    /**
     * 環境Envに対するtyvarsは、その環境に登録されているすべての型スキー
     * マに対するtvarsの値全体を返す。
     * つまり、環境全体が含む「全称量化に関するフリー変数の集合」を返す。
     */
    List<Tyvar> tyvars(Env env) {
        env.values().inject([]){ acc, it -> acc+tyvars(it)}
    }

    /**
     * 型tと型uのユニフィケーション。
     * 型tと型uに対してs'(t) s'(u)が一致するような、sを拡張した置換s'
     * を返す。
     */
    Subst mgu(Type t, Type u, Subst s) {
        def (st, su) = [s(t), s(u)]
        if (st instanceof Tyvar && su instanceof Tyvar && st.a == su.a) { return s } // 等しい型変数
        else if (st instanceof Tyvar) { return s.extend(st, su) } // 左辺が型変数
        else if (su instanceof Tyvar) { return mgu(u, t, s) } // 右辺が型変数
        else if (st instanceof Arrow && su instanceof Arrow) { // Arrow同士
            return mgu(su.t1, st.t1, mgu(su.t2, st.t2, s))
        }
        else if (st instanceof Tycon && su instanceof Tycon && st.k == su.k) {
            return zip(st.ts, su.ts).inject(s) { acc, it -> mgu(it[0], it[1], acc) }
        }
        throw new TypeError("cannot unify $st with $su")
    }

    /**
     * 二つのリストxs=[x1,x2,x3..], ys=[y1,y2,y3]のとき、
     * [[x1,y1],[x2,y2],[x3,y3]..]を返す。
     */
    static zip(xs, ys) {
        if (xs.size() != ys.size()) {
            throw new TypeError("cannot unify $xs with $ys, number of type arguments are different")
        }
        Iterator itor = ys.iterator()
        xs.collect { [it, itor.next()] }
    }

    /**
     * エラーメッセージに含めるための、処理中の項への参照。
     */
    Term current = null

    /**  
     * envのもとで、eの型がt型に一致するためのsを拡張した置換s'を返す。
     * 数式で書くと以下のとおり。
     *
     *    s'(env) ├ ∈ e:s'(t)
     *  
     * つまり、型の間の関係制約式(型変数を含む)の集合envのもとで、「s'(env)の
     * 型はs'(t)である」を満たすような、sを拡張した置換s'を値を返す。
     */
    Subst tp(Env env, Term e, Type t, Subst s) {
        current = e
        switch (e) {
        case Var:
            // 変数参照eの型は、eの識別子e.xとして登録された型スキーマを実体化(全称量
            // 化された変数のリネーム)をした型である。
            TypeScheme u = lookup(env, e.x)
            if (u == null) throw new TypeError("undefined: "+e.x)
            return mgu(u.newInstance(), t, s)
        case Lam:
        
            // λで束縛される変数とletで束縛される変数の扱いの違いにつ
            // いて。
            // 変数(識別子)は、HMの多相型の解決において、キーとなる存在
            // である。型スキーマは変数(識別子)にのみ結びつく。変数を介
            // 在して得た型スキーマを基軸に、インスタンス化=全称量化=型
            // 変数置換が実行される。
            //
            // 識別子x,yに束縛される式が多相型であるとき、型変数の解決
            // の扱いに関して両者には違いがある。
            //
            // λx.eの場合、xに対応して環境に登録されるのは、xの型を表
            // わす新規の型変数(a = newTyvar())を型テンプレートとする型
            // スキーマ(型抽象)であり、かつaについては全称限量されない。
            // つまり「全称量化に関するフリー型変数を含む型スキーマ」に
            // なっている。
            //
            // let y=e1 in e2の場合、yに対応して環境に登録されるのは、
            // e1の型を元にして、e1中の型変数群
            // 
            // 「e1.tyvars-tyvars(e1.e)」…(*)
            // 
            // を全称限量した型スキーマ(型抽象)。例えば「new
            // TypeScheme(tyvars(e1), e1)」が登録される。
            // なお、(*)における、tyvars(e1.e)は、e1中のフリー型変数だ
            // が、これが生じるのは、λ束縛の本体の型検査の場合である。
            // つまり
            //
            //   \ x -> let y=e1 in e2
            //
            // のように、λ本体の中にlet式が出現するときに、let束縛され
            // る識別子yのために登録される型スキーマでは、xに対応する型
            // スキーマで使用されている型変数がフリーなので全称限量対象
            // から除外される。
            // 
            // [ここでのλとletの違いがどのような動作の違いとして現われるか?]
            // 
            // Haskellで確認する。
            // 
            // ghci> let x=length in x [1,2,3]+x "abc"
            // 6
            // ghci> (\ x -> x [1,2,3]+x "abc") length
            //         <interactive>:5:12:
            //     No instance for (Num Char)
            //       arising from the literal `1'
            //     Possible fix: add an instance declaration for (Num Char)
            //     In the expression: 1
            //     In the first argument of `x', namely `[1, 2, 3]'
            //     In the first argument of `(+)', namely `x [1, 2, 3]'
            //
            // letでのxに束縛された多相関数lengthの型(a->a)における型変
            // 数aは全称限量される(Haskell流に書くとforall a.a->a)ので、
            // 「x [1,2,3]」と「x "abc"」それぞれにおけるxの出現それぞ
            // れでaがリネームされ(1回目はa',二回目はa''など)、別の型変
            // 数扱いになる。そのため、a'とa''がそれぞれのIntとCharに実
            // 体化されても、型エラーにならない。
            // 
            // λの場合、xの型は全称限量されない(a->a)なので、a=Intと
            // a=Charの型制約が解決できず型エラーとなる。この動作はテス
            // トケースtestTpLamP2()、testTpLetP1() で確認する。
            def (Tyvar a, Tyvar b) = [newTyvar(), newTyvar()]
            Subst s1 = mgu(t, Arrow(a, b), s)
            return tp(new Env(env)+[(e.x):new TypeScheme([], a)], e.e, b, s1)
        case App:
            Tyvar a = newTyvar()
            Subst s1 = tp(env, e.f, Arrow(a, t), s)
            return tp(env, e.e, a, s1)
        case Let:
            // λ x ...で束縛される変数とlet x= ..in..で束縛され
            // る変数の違いについては前述の通り。
            Tyvar a = newTyvar()
            Subst s1 = tp(env, e.e, a, s)
            return tp(new Env(env) + [(e.x):gen(s1(env), s1(a))], e.f, t, s1)
         case LetRec:
             def (Tyvar a, Tyvar b) = [newTyvar(), newTyvar()]
             def s1 = tp(new Env(env) + [(e.x):new TypeScheme([], a)], e.e, b, s)
             def s2 = mgu(a, b, s1)
             return tp(new Env(env) + [(e.x):gen(s2(env), s2(a))], e.f, t, s2)
         }
    }

    /**
     * 環境envにおいてTerm eの型として推定される型を返す。
     */
    Type typeOf(Env env, Term e) {
      def a = newTyvar()
      tp(env, e, a, Subst.emptySubst)(a)
    }

    /**
     * 既定義の識別子(処理系の組み込み関数もしくはライブラリ関数を想定)を
     * いくつか定義した型環境を返す。型のみの情報でありそれらに対する構
     * 文木の情報はない。
     */
    Env predefinedEnv() {
        Type booleanType = Tycon("Boolean", [])
        Type intType = Tycon("Int", [])
        Closure<Type> listType = { Type t -> Tycon("List", [t]) }
        Closure<TypeScheme> gen = { Type t -> gen(new Env(), t) }

        def a = newTyvar()
        return new Env(['true':gen(booleanType),
                       'false':gen(booleanType),
                       'if':gen(Arrow(booleanType, Arrow(a, Arrow(a, a)))),
                       'zero':gen(intType),
                       'succ':gen(Arrow(intType, intType)),
                       'nil':gen(listType(a)),
                       'cons':gen(Arrow(a, Arrow(listType(a), listType(a)))),
                       'isEmpty':gen(Arrow(listType(a), booleanType)),
                       'head':gen(Arrow(listType(a), a)),
                       'tail':gen(Arrow(listType(a), listType(a))),
                       'fix':gen(Arrow(Arrow(a, a), a))]) 
    }

    /**
     * 項の型を返す。
     */
    String showType(Term e) {
        try {
            typeOf(predefinedEnv(), e).toString()
        } catch (TypeError ex) {
            "\n cannot type: $current"+
                "\n reason: ${ex.message}"
        }
    }

    /**
     * @Singleton宣言したクラスのシングルトンはTypeInfer.instanceで保持
     * されており、クラス外からも取得できる。しかし、
     * 「TypeInfer.instance」が少し冗長なのと、Scala版に合せるため、シ
     * ングルトンを以下で定義する静的変数TypeInfer.typeInferで取得でき
     * るようにする。ただしSingletonの初期化タイミングの都合上か、遅延
     * 設定のAST変換@Lazyを指定しないとうまくいかないようである。
     */
    @Lazy static typeInfer = TypeInfer.instance
}

テストコードつきはこちら。

上記は元コード同様関数型っぽい作りになってる(Substによる実現とか)が、書き換えを許す前提でならもっと簡潔になりそう。型変数の一意性保証のために「型変数名」とかの置き換えにたよらず、型変数オブジェクトを単にシェアすればいいんじゃないかな…。

*1:もしくはDamas–Milner or Damas–Hindley–Milnerとしても知られているとのこと。

*2:HMと比べると果してそれらが「推論」と呼べるのかどうか…。

*3:実言語では、常にはそうならないケースもあると思われる。ランクN多相とかにとどまらず。あと、実用上は宣言しないと、人間がついていけない(デバッグできない。)という問題もあり、適宜宣言するのだろう。

*4:型に継承関係があると難しそうだ。