Prologで様々な多相型推論

この記事は時空を色々遡って、2017年の言語実装技術の12日目の記事として投稿するために色々と書き換えをしたものです。
11日目、16日目、20日目、21日目と型推論のオンパレードのようになっているので、Prologの記事も合わせて載せたいと思い書き換えて投稿させてもらいます。

概要

型理論、操作的意味論などの理論では一般的に一階述語論理が広く用いられていますが、多くのプログラマにとって馴染みがなく難しい数式に思えます。
Prologを使うことでその図を簡単に理解可能になります。例えば Prolog で多相型推論を記述した TIPER ¹ で示されている環境を保存し copy_term 述語によって具体化する手法を用いるとわずか十数行で多相型推論を記述可能です。(付録 A)
しかしながら、一般的な言語での実装をするには飛躍があります。そこでここでは、自由型変数を求め型スキームを求めるHindley-MilnerのアルゴリズムWを Prolog により実装し解説します。
また、Prologの有用性について述べ、レベルベースの高速化についても触れます。

1. はじめに

多相的な型推論は型再構築とも呼ばれ、Hindley-Milner ² のアルゴリズムWは有名で、SML,OCaml,Haskell等の言語の型推論の最も基本的な技術として用いられています。アルゴリズムWは、let id = fun x -> x in id id のような式に型の記述はありませんが、型を推論することで 'a -> 'a のような型を再構築することができます。アルゴリズムWは基本的なアルゴリズムですが、その理解は意外と難しく言語実装者を悩ませる技術の１つと言えるでしょう。

この文章を書き始めたきっかけは、Rust での OCaml 実装で理論的な論文に乗っている形に近い形で理解してもらえたならば、将来より高度な型理論の論文がかけるようになるのではないかという思いから書きはじめたものです。「わかんねぇよ、これじゃ、人間に理解できないよ」などと思われているかも知れませんがｗ

型推論を理解するのに重要な技術、概念は型スキーム、自由変数、一般化、具体化、単一化です。
この中でも単一化は煩雑な処理を書く必要があります。型変数を作って他の方との連立方程式を作り、単一化処理を作り、出現検査を行い、型変数を剥ぎ取る処理を行う必要があります。
Prolog は単一化を持った言語なので単一化の煩雑な処理を記述すること無く、型推論を記述可能なので本質をよりはっきりと意識して見ることが出来ます。(このPrologさえ理解していればというのがハードル高そうなのですけどｗ)

2. 形式手法と自然演繹とProlog

プログラミング言語の形式的な図 (評価規則や型付け規則) は一般的に一階述語論理である自然演繹スタイルの推論規則が用いられます。
なぜ、一階述語論理は型システムの記述に用いられるのかは、筆者の推測ですが、単一化やバックトラックを使うと短く記述できるからでしょう。

Prologもまた一階述語論理型言語なので自然演繹スタイルの図に似せて記述し実行できます。
しかし、Prologさえあれば何でも推論できるわけではありません。Prologは深さ優先探索で推論するため左再帰を含む規則の推論は無限ループに陥ります。
自然演繹は探索アルゴリズムは深さ有線探索以外の探索方法での推論も行えるので、Prologで無限ループに陥るような規則を使わないと解けない問題でも、例えば優秀な人が計算すれば解くことが出来ます。人間が計算しなくてもより高度な自動推論システムならば推論できるでしょう。

それでは、Prologは不完全で価値のない言語なのでしょうか？そんなことはありません。Prologで実装可能な推論規則は、構文主導の推論規則、あるいはアルゴリズミックな推論規則などと呼ばれます。構文主導な推論規則であれば、素直にPrologでも実装可能です。Prologで実装可能ならば関数型言語や命令的な言語でも素直に実装できます。Prologは宣言的な言語ですが、アルゴリズミックである規則かどうかを判断するのに役立ちます。Prologで書かれたシステムは素直に関数型言語やオブジェクト指向言語、命令的な言語に移植して実装できますが、Prologで実装できない規則は素直に命令的な言語で記述できないでしょう。

3. 構文

ここで説明に用いる言語の構文を以下に示します:

式
E ::= X                 変数
    | fun(X->E)         関数
    | E $ E             関数適用
    | let(X = E; E)     let式
単相型
T ::= A                 型変数
    | T->T              関数
型スキーム
Sc::= T                 単相型
    | ∀([A1,...,An],T) 多相型

式 E は変数 X, 関数 fun(X->E),関数適用 E $ E, let式 let(X = E; E) からなります。
単相型 T は型変数 A または関数の型 T->T からなります。
型スキームは単相型tあるいは多相型 ∀([A1,...,An],T) からなります。

---

^{※ここで用いた構文はBNF(バッカス・ナウア記法)に似ていますが、正確にはBNFではありません。BNFと言い切ると突っ込まれることがあるので構文(syntax)とだけ書くことで無用な議論を回避できるので構文とかくとよいようです。CoPLではBNFっていい切ってるんだけどなぁ。}

4. 型再構築

ここでは型再構築のアルゴリズムWをPrologで実装します。実装全体は 付録 C を参照してください。

4.1 ユーティリティ

member_eq(X,[Y|_]) :- X == Y.
member_eq(X,[_|Xs]) :- member_eq(X,Xs).

member_eq/2 述語はリスト内にある値が存在するかどうかを単一化をすること無く実体で調べます。

(X : Sc) ∈ Γ :- member(X : Sc, Γ).

∈/2 述語は単一化ありでリスト内の型スキームを求めるために使います。

union_eq([],Ys,Ys).
union_eq([X|Xs],Ys,Zs) :- member_eq(X,Ys), union_eq(Xs,Ys,Zs).
union_eq([X|Xs],Ys,[X|Zs]) :- union_eq(Xs,Ys,Zs).

union_eq/3 述語はリスト同士を集合として扱い同じ要素は1つだけ残します。変数の単一化は行いません。

subtract_eq([],_,[]).
subtract_eq([X|Xs],Ys,Zs) :- member_eq(X,Ys),subtract_eq(Xs,Ys,Zs).
subtract_eq([X|Xs],Ys,[X|Zs]) :- subtract_eq(Xs,Ys,Zs).

subtract_eq/3 述語はリストからリストを差し引きます。変数の単一化は行いません。

4.2 自由型変数 FTV Free Type Variable

自由型変数とは、型の中に含まれる型変数です。
ただし、型スキームのパラメータに含まれている型変数は省きます。
ftv/2 述語は型、型スキームまたは型環境の自由型変数を求めます:

ftv(A,[A]) :- var(A).
ftv((T1->T2),FTV) :- ftv(T1,FTV1), ftv(T2,FTV2), union_eq(FTV1,FTV2,FTV).
ftv(∀(FTV1,T2),FTV) :- ftv(T2,FTV2), subtract_eq(FTV2,FTV1,FTV).
ftv([],[]).
ftv([_:T|Γ],FTV) :- ftv(T,FTV1), ftv(Γ,FTV2), union_eq(FTV1,FTV2,FTV).

4.3 一般化

述語 ^/2 は : と組み合わせて３パラメータの述語として用い、型環境 Γ と型 T から型 T を一般化し型スキームを求めます。

Γ˄(T) : ∀(FTV,T) :- ftv(T,FTVʹ),ftv(Γ,FTVʹʹ), subtract_eq(FTVʹ,FTVʹʹ,FTV), FTV \= [].
Γ˄(T) : T.

型スキームを求めるには型 T の自由型変数 FTVʹ から型環境 Γ の自由型変数 FTVʹʹ を差し引いた FTV が空でなければ FTV をパラメータとして多相型とします。 FTV が空であるならば単相の型とします。

4.4 インスタンス化

インスタンス化は一般化された型スキームから型を新たに生成します。

inst(A, A) :- var(A).
inst((T1->T2), (T1->T2)).
inst(∀(FTV,T), T_) :- maplist(inst1,FTV,S),sub(S,T,T_).
inst1(T,(T1,T2)) :- newvar(T2).
sub(S,X,T_)                   :- var(X), (X,T)∈S,!, sub(S, T, T_).
sub(S,(T1->T2),   (T1_->T2_)) :- !,sub(S,T1,T1_), sub(S,T2,T2_).
sub(_,T       , T)            :- !.

単相の型、型変数 A または関数の場合もそのままの値を返します。
多相の型の場合、 FTV の中身を新しい型変数を作成して置き換えます。

4.5 単一化

単一化は2つの型を同じものとして方程式を解きます。

unify(T,T).

単一化の実装は Prolog の機能をそのまま使用します。

4.6 アルゴリズムW

newvar(T), [X : T|Γ] ⱶW E : Tʹ
--%--------------------------------     [Abs]
Γ ⱶW fun(X->E) : (T -> Tʹ).

Γ ⱶW E0 : T, Γ˄(T) : Sc, [X : Sc|Γ] ⱶW E1 : Tʹ
--%------------------------------------------- [Let]
Γ ⱶW let(X = E0 ; E1) : Tʹ.

atom(X), (X : Sc) ∈ Γ, inst(Sc,T)
--%--------------------------------     [Var]
Γ ⱶW X : T.

Γ ⱶW E0 : T0, Γ ⱶW E1 : T,
newvar(Tʹ), unify(T0, (T -> Tʹ))
--%--------------------------------     [App]
Γ ⱶW (E0 $ E1) : Tʹ.

型再構築アルゴリズムWは4つの推論規則 Abs、Let、Var、 App を含みます。
Absは関数の規則です。新たな型変数 T を生成し、変数名 X の型を T として型環境 Γ を拡張して式 E の型 Tʹ を求めます。このとき、 fun(X->E) の型は (T->Tʹ) になります。
LetはLet式の規則です。 E0 の型 T を求め、型環境 Γ と型 T から一般化した型スキーム Sc を求めます。 E1 の型 Tʹ は変数名 X、型スキーム Sc で環境 Γ を拡張し求めます。
Varは変数の規則です。環境 Γ を X で検索し型スキーム Sc を求め、インスタンス化した型 T を返します。
Appは関数適用の規則です。 E0 の型 T0、 E1 の型 T1 を求め、新たな型変数 Tʹ を生成し、 T0 と T->Tʹ を単一化し、型 Tʹ を返します。

5 レベルを使った高速化

多相の型推論は便利ですが、そのままのアルゴリズムを使うと大きなプログラムでは型推論に時間がかかってしまいます。特に古いコンピュータでは遅かったそうです。そこで、自由型変数の計算を高速化する手法が編み出されました ³。Oleg による雄弁な解説は ⁴ 型推論はガーベジコレクションに似ているという視点で解説されています。Implementations of various type systems in OCaml⁵ には、更に拡張した様々な型システムがあります。Udon言語 ⁶ はSMLによるレベル付き多相関数の良い例です。 型推論器と現実 ⁷ ではレベル付き型推論が勉強会で紹介されています。Go での日本語による詳しい解説記事は、アドベントカレンダーの20日目 ⁸ の記事が参考になるでしょう。

基本的なアイディアは多相関数の型パラメータを求めるには関数、あるいはブロックのスコープ内で作られた型変数の中で型が確定していないものを取り出せれば良いので、let 以下の式は１つネストレベルを上げて、型変数のレベルを保存しておき、一般化する際には、レベルより深いものだけを取り出すようにするのです。

実装例は 付録 E にあります。型変数は Prolog の変数を用いました。Prolog は一度値を束縛したら変数の変更が出来ないので、実装例では型変数からレベルへの写像 C を持ち回ることにしました(C という名前は型変数のカウンタ変数の代わりという意味です)。

単一化は、 occurs チェック内で型変数 V1,V2 のレベル Lv1,Lv2 が Lv1 < Lv2 のときに V2 のレベルを Lv1 にします。

occurs(C|V1,V2:C_)      :- var(V2),member_eq(V1=Lv1,C),member_eq(V2=Lv2,C),Lv1 < Lv2,update(C|V2=Lv1:C_).
occurs(C|_,V2:C)        :- var(V2),!.

一般化は、型変数 V のレベル Lv1 が現在のレベル Lv より大きい場合のみ一般化変数 gen(V) に書き換えます。

gen(C,Lv|V:gen(V))        :- var(V),member_eq(V:Lv1,C),Lv1 > Lv,!.
gen(_,_ |V:V)             :- var(V),!.

具体化は、 gen(I) の変数だけをコピーします。このとき、コピーした変数はキャッシュ M (Mapの略) に保存して、再度 inst 内で現れた場合に利用します。

inst(_ ,C/M|gen(I):T/(C/M))         :- member(I=T,M).
inst(Lv,C/M|gen(I):T/(C_/[I=T|M]))  :- newvar(C,Lv:T/C_).

型推論のメインプログラムでは、 let の E1 を計算するときのみレベル Lv を +1 します:

w(A,Lv,C|(E1$E2):T3/C_)        :- w(A,Lv,C|E1:T1/C1),w(A,Lv,C1|E2:T2/C2),
                                  newvar(C2,Lv:T3/C3),unify(C3|T1,T2->T3:C_).
w(A,Lv,C|(let(X=E1);E2):T2/C_) :- Lv1 is Lv+1, w(A,Lv1,C|E1:T1/C1),
                                  gen(C1,Lv|T1:T1_),w([X:T1_|A],Lv,C1|E2:T2/C_).
w(A,Lv,C|X:T_/C_)              :- atom(X),member(X:T,A),inst(Lv,C/[]|T:T_/(C_/_)).

update はリスト内を書き換え、 member_eq はリスト内の変数を実体で比較して値を取得、 newvar はレベル環境 C とレベルLvから型変数 V を作り、型変数 V とレベルを保存した環境を返します。

update([V=_|C]|V1=Lv:[V=Lv|C]) :- V == V1.
update([X|C]|V=Lv:[X|C_]) :- update(C|V=Lv:C_).
member_eq(X:V,C) :- member(X1:V,C),X1==X.
newvar(C,Lv:V/[V=Lv|C]).

このような変更で、多相関数の型パラメータを高速に求めることができます。

6. まとめ

単一化がファーストクラスの機能としてある Prolog を使うと型推論は短く書くことが出来ました。Prolog を理解すれば一階述語論理を理解したことになるので、論文の図も簡単に読み解くことができるようになります。アルゴリズムWは基本的なアルゴリズムです。Prolog では論理型言語から関数型言語のレベルまで落とし込む操作ができます。最後に、型推論の高速化にはレベルを用いたアルゴリズムをPrologで簡潔に記述しました。
Prologはあまり馴染みのない言語かも知れませんが、型理論とは案外相性が良い言語です。 Prologを使えば型理論はずっと身近になるはず。みなさんも Prolog を使って型推論を書いてみてはどうでしょうか？

付録

付録 A. 最も短い多相型推論

:- op(740,xfx,[$]).
:- op(900,xfx,ⱶs).

inst(∀(Γ,T), Tʹ) :- copy_term(∀(Γ,T),∀(Γ,Tʹ)).
gen(Γ,T,∀(Γ,T)).
tp(Γ, X, T)                 :- atom(X), member(X : Sc, Γ), inst(Sc, T).            % [Var]
tp(Γ, E0 $ E1, Tʹ)          :- tp(Γ, E0, (T -> Tʹ)), tp(Γ, E1, T).                 % [App]
tp(Γ, fun(X->E), (T -> Tʹ)) :- tp([X : ∀([],T)|Γ], E,Tʹ).                         % [Abs]
tp(Γ, let(X = E0; E1), Tʹ)  :- tp(Γ, E0, T), gen(Γ,T, Sc), tp([X : Sc|Γ], E1, Tʹ). % [Let]

:- tp([],fun(x->x),(T->T)).
:- tp([],let(id=fun(x->x); id $ id),(T->T)).

:- halt.

付録 B. 宣言的な多相型推論

:- op(740,xfx,[∈, ⊑ , ˄, $]).
:- op(900,xfx,ⱶs).
:- op(1200, xfx, --).
term_expansion((A--B), (B:-A)).

(X : Sc) ∈ Γ :- member(X : Sc, Γ).

% Instantiation
    ∀(Γ,T) ⊑ Tʹ :- copy_term(∀(Γ,T),∀(Γ,Tʹ)).
    m(T) ⊑ T.

% Generalization
    Γ˄(T) : ∀(Γ,T).

% Syntactical Rule System

    atom(X), (X : Sc) ∈ Γ, Sc ⊑ T
    --%-------------------------------- [Var]
    Γ ⱶs X : T.

    Γ ⱶs E0 : (T -> Tʹ), Γ ⱶs E1 : T
    --%-------------------------------- [App]
    Γ ⱶs (E0 $ E1) : Tʹ.

    [X : m(T)|Γ] ⱶs E : Tʹ
    --%-------------------------------- [Abs]
    Γ ⱶs fun(X->E) : (T -> Tʹ).

    Γ ⱶs E0 : T, Γ˄(T) : Sc, [X : Sc|Γ] ⱶs E1 : Tʹ
    --%------------------------------------------- [Let]
    Γ ⱶs let(X = E0; E1) : Tʹ.

:- [] ⱶs fun(x->x) : (T->T).
:- [] ⱶs let(id=fun(x->x); id $ id) : (T->T).

:- halt.

付録 C. 型スキームを求めるバージョン

:- op(740,xfx,[∈, ˄, $]).
:- op(900,xfx,ⱶW).
:- op(1200, xfx, --).
term_expansion((A--B), (B:-A)).

member_eq(X,[Y|_]) :- X == Y.
member_eq(X,[_|Xs]) :- member_eq(X,Xs).

union_eq([],Ys,Ys).
union_eq([X|Xs],Ys,Zs) :- member_eq(X,Ys), union_eq(Xs,Ys,Zs).
union_eq([X|Xs],Ys,[X|Zs]) :- union_eq(Xs,Ys,Zs).

subtract_eq([],_,[]).
subtract_eq([X|Xs],Ys,Zs) :- member_eq(X,Ys),subtract_eq(Xs,Ys,Zs).
subtract_eq([X|Xs],Ys,[X|Zs]) :- subtract_eq(Xs,Ys,Zs).

ftv(A,[A]) :- var(A).
ftv((T1->T2),FTV) :- ftv(T1,FTV1), ftv(T2,FTV2), union_eq(FTV1,FTV2,FTV).
ftv(∀(FTV1,T2),FTV) :- ftv(T2,FTV2), subtract_eq(FTV2,FTV1,FTV).
ftv([],[]).
ftv([_:T|Γ],FTV) :- ftv(T,FTV1), ftv(Γ,FTV2), union_eq(FTV1,FTV2,FTV).

(X) ∈ Γ :- member(X, Γ).

% Generalization
    Γ˄(T) : ∀(FTV,T) :- ftv(T,FTVʹ),ftv(Γ,FTVʹʹ), subtract_eq(FTVʹ,FTVʹʹ,FTV), FTV \= [].
    Γ˄(T) : T.

% Instantiation
    inst(A, A) :- var(A).
    inst((T1->T2), (T1->T2)).
    inst(∀(FTV,T), T_) :- maplist(inst1,FTV,S),sub(S,T,T_).
    inst1(T,(T1,T2)) :- newvar(T2).
    sub(S,X,T_)                   :- var(X), (X,T)∈S,!, sub(S, T, T_).
    sub(S,(T1->T2),   (T1_->T2_)) :- !,sub(S,T1,T1_), sub(S,T2,T2_).
    sub(_,T       , T)            :- !.

newvar(_).
unify(T,T).

% Algorithm W

    atom(X), (X : Sc) ∈ Γ, inst(Sc,T)
    --%--------------------------------     [Var]
    Γ ⱶW X : T.

    Γ ⱶW E0 : T0, Γ ⱶW E1 : T,
    newvar(Tʹ), unify(T0, (T -> Tʹ))
    --%--------------------------------     [App]
    Γ ⱶW (E0 $ E1) : Tʹ.

    newvar(T), [X : T|Γ] ⱶW E : Tʹ
    --%--------------------------------     [Abs]
    Γ ⱶW fun(X->E) : (T -> Tʹ).

    Γ ⱶW E0 : T, Γ˄(T) : Sc, [X : Sc|Γ] ⱶW E1 : Tʹ
    --%------------------------------------------- [Let]
    Γ ⱶW let(X = E0 ; E1) : Tʹ.

:- [] ⱶW fun(x->x) : (T->T).
:- [] ⱶW let(id=fun(x->x); id $ id) : (T->T).

:- halt.

付録 D. 単一化を実装

:- expects_dialect(sicstus).
:- op(740,xfx,[∈, ˄, $]).
:- op(900,xfx,ⱶW).
:- op(1200, xfx, --).
term_expansion((A--B), (B:-A)).

failwith(A,Xs) :- format(A,Xs),nl,!,halt. % エラー処理
foldr(_,[],S,S) :- !. % 畳み込み
foldr(F,[X|Xs],S,S_) :- foldr(F,Xs,S,S1),!,call(F,X,S1,S_),!.
zip([], [], []). % ２つのリストを１つにする
zip([X|Xs], [Y|Ys], [(X,Y)|Zs]) :- zip(Xs,Ys,Zs).

% 型変数検査と変数検査
tVar(X) :- \+var(X), atom(X), X \= int, X \= float.
val(X) :- atom(X).

% 型の置換
sub(S,X,T_)                   :- tVar(X), (X,T)∈S,!, sub(S, T, T_).
sub(S,(T1->T2),   (T1_->T2_)) :- !,sub(S,T1,T1_), sub(S,T2,T2_).
sub(S,∀(FTV, T),∀(FTV, T_)) :- !,findall((X,T),(member((X,T),S),member(X,FTV)),S_), sub(S_,T,T_).
sub(_,T       , T)            :- !.
gsub(S,Γ,Γ_) :- maplist(gsub1(S),Γ,Γ_),!. % 型環境の置換
gsub1(S,(X,T),(X,T_)) :- !,sub(S,T,T_),!.

ftv(A,[A]) :- tVar(A).
ftv((T1->T2),FTV) :- ftv(T1,FTV1), ftv(T2,FTV2), union(FTV1,FTV2,FTV).
ftv(∀(FTV1,T2),FTV) :- ftv(T2,FTV2), subtract(FTV2,FTV1,FTV).
ftv([],[]).
ftv([_:T|Γ],FTV) :- ftv(T,FTV1), ftv(Γ,FTV2), union(FTV1,FTV2,FTV).

X ∈ Γ :- member(X, Γ).

% Generalization
    Γ˄(T) : ∀(FTV,T) :- ftv(T,FTVʹ),ftv(Γ,FTVʹʹ), subtract(FTVʹ,FTVʹʹ,FTV), FTV \= [].
    _˄(T) : T.

% Instantiation
    inst(∀(FTV,T),T_) :- !,maplist(inst1,FTV,S),sub(S,T,T_).
    inst(T,T).
    inst1(T1,(T1,T2)) :- newvar(T2).

put(N,B) :- bb_put(N,B). get(N,B) :- bb_get(N,B). update(N,D,A) :- bb_update(N,D,A).
reset :- put(i,0). % カウンタiと置換sのグローバル変数のリセット
newvar(X) :- get(i,C), C2 is C + 1, put(i,C2), format(atom(X),'x~d', [C]). % 新しい変数を作成

unify((T1, T2), S, S_)            :- sub(S,T1,T1_), sub(S,T2,T2_),!,unify1((T1_,T2_), S, S_),!. % 置換してunify1呼び出し
unify1((T1, T1), S, S)            :- !. % 同じなら何もしない
unify1((X, T), S, [(X,T)|S])      :- tVar(X),!,occurs(X, T).
unify1((T, X), S, [(X,T)|S])      :- tVar(X),!,occurs(X, T).
unify1(((T1->T2),(T3->T4)), S,S_) :- !,foldr(unify, [(T1,T3),(T2,T4)], S,S_).       % 関数
unify1((T1, T2), S, _)            :- !,failwith('error ~w',[unify1((T1, T2), S)]).  % エラー
% 出現検査
occurs(X, X)            :- tVar(X),!,failwith('unify occurs error ~w ~w',[X,tVar(X)]).
occurs(X, ∀(FTV, T))     :- !,maplist(occurs(X),[T|FTV]).
occurs(X, (T1->T2))     :- !,maplist(occurs(X), [T1,T2]).
occurs(_, _)            :- !.

% Algorithm W

    atom(X), (X : Sc) ∈ Γ, sub(S,Sc,Sc_),
    inst(Sc_,T)
    --%--------------------------------     [Var]
    (Γ,S) ⱶW X : (T,S).

    (Γ,S) ⱶW E0 : (T0,S0), (Γ,S0) ⱶW E1 : (T,S1),
    newvar(Tʹ), unify((T0, (T -> Tʹ)),S1,S2)
    --%--------------------------------     [App]
    (Γ,S) ⱶW (E0 $ E1) : (Tʹ,S2).

    newvar(T), ([X : T|Γ],S) ⱶW E : (Tʹ,S1)
    --%--------------------------------     [Abs]
    (Γ,S) ⱶW fun(X->E) : ((T -> Tʹ),S1).

    (Γ,S) ⱶW E0 : (T,S0),
    sub(S0,T,T_), gsub(S0,Γ,Γ_), Γ_˄(T_) : Sc,
    ([X : Sc|Γ],S0) ⱶW E1 : (Tʹ,S1)
    --%------------------------------------------- [Let]
    (Γ,S) ⱶW let(X = E0 ; E1) : (Tʹ,S1).

tp(E:T) :- reset,([],[]) ⱶW E : (T1,S), sub(S,T1,T).

:- tp(fun(x->x):T), writeln(T).
:- tp(let(id=fun(x->x); id $ id):T), writeln(T).

:- halt.

付録 E. レベルを用いて高速化

% Algorithm W with Depth Level
:- op(600,xfy,[$,catch]).
:- op(10,fx,[try]).
try {A} catch {E->F} :- catch(A,E,F).
throw(F,P) :- format(atom(Err),F,P),throw(Err).
update([V=_|C]|V1=Lv:[V=Lv|C]) :- V == V1.
update([X|C]|V=Lv:[X|C_]) :- update(C|V=Lv:C_).
member_eq(X:V,C) :- member(X1:V,C),X1==X.
newvar(C,Lv:V/[V=Lv|C]).

occurs(_|V1,V2:_)       :- V1==V2,throw('unify occurs error ~w ~w',[V1,V2]).
occurs(C|V1,V2:C_)      :- var(V2),member_eq(V1=Lv1,C),member_eq(V2=Lv2,C),Lv1 < Lv2,update(C|V2=Lv1:C_).
occurs(C|_,V2:C)        :- var(V2),!.
occurs(_|V,gen(V2):_)   :- throw('unify occurs error ~w ~w',[V,V2]).
occurs(C|V,(T2->T3):C_) :- occurs(C|V,T2:C1),occurs(C1|V,T3:C_).
occurs(C|_,_:C).

unify(C|T1,T2:C)          :- T1==T2.
unify(C|V,T:C_)           :- var(V),!,occurs(C|V,T:C_),T=V.
unify(C|T,V:C_)           :- var(V),!,occurs(C|V,T:C_),T=V.
unify(C|T1->T2,T3->T4:C_) :- unify(C|T1,T3:C1),unify(C1|T2,T4:C_).
unify(_|T1,T2:_)          :- throw('unify error (~w,~w)',[T1,T2]).

gen(C,Lv|V:gen(V))        :- var(V),member_eq(V:Lv1,C),Lv1 > Lv,!.
gen(_,_ |V:V)             :- var(V),!.
gen(C,Lv|T1->T2:T1_->T2_) :- !,gen(C,Lv|T1:T1_),gen(C,Lv|T2:T2_).
gen(_,_ |T:T).

inst(_ ,C/M|gen(I):T/(C/M))         :- member(I=T,M).
inst(Lv,C/M|gen(I):T/(C_/[I=T|M]))  :- newvar(C,Lv:T/C_).
inst(Lv,CM|(T1->T2):(T1_->T2_)/CM_) :- inst(Lv,CM|T1:T1_/CM1),inst(Lv,CM1|T2:T2_/CM_).
inst(_ ,CM|T:T/CM).

w(_,_ ,C|I:int/C)              :- integer(I).
w(_,_ ,C|true:bool/C).
w(_,_ ,C|false:bool/C).
w(A,Lv,C|λ(X,E):(T1->T2)/C_)   :- newvar(C,Lv:T1/C1),w([X:T1|A],Lv,C1|E:T2/C_).
w(A,Lv,C|(E1$E2):T3/C_)        :- w(A,Lv,C|E1:T1/C1),w(A,Lv,C1|E2:T2/C2),
                                  newvar(C2,Lv:T3/C3),unify(C3|T1,T2->T3:C_).
w(A,Lv,C|(let(X=E1);E2):T2/C_) :- Lv1 is Lv+1, w(A,Lv1,C|E1:T1/C1),
                                  gen(C1,Lv|T1:T1_),w([X:T1_|A],Lv,C1|E2:T2/C_).
w(A,Lv,C|X:T_/C_)              :- atom(X),member(X:T,A),inst(Lv,C/[]|T:T_/(C_/_)).
w(_,_ ,_|X:_/_)                :- atom(X),throw('lookup error ~w',[X]).

test(E:T) :- try { format('test ~w ',[E]), w([],0,[]|E:T2/_),!,
                   (T\=T2->throw('expected ~w but ~w',[T,T2]) ; writeln(ok))
                 } catch { Err->format('error ~w\n',[Err]) }.

:- test(1:int).
:- test(true:bool).
:- test(false:bool).
:- test((let(x=1);x):int).
:- test((let(id=λ(x,x));id):(1->1)).
:- test((let(id=λ(x,x));id$id):(2->2)).
:- test((let(id=λ(x,x));id$id$1):int).
:- test((let(id=λ(x,x));id$id$true):bool).
:- halt.

参考文献

1. TIPER Type Inference Prototyping Engines from Relational Specifications of type systems http://kyagrd.github.io/tiper/ ↩

2. http://en.wikipedia.org/wiki/Hindley–Milner_type_system ↩

3. Didier Rémy. Extending ML type system with a sorted equational theory. 1992 http://gallium.inria.fr/~remy/ftp/eq-theory-on-types.pdf ↩

4. How OCaml type checker works -- or what polymorphism and garbage collection have in common http://okmij.org/ftp/ML/generalization.html ↩

5. Implementations of various type systems in OCaml. https://github.com/tomprimozic/type-systems ↩

6. A Hobby implementation of ML https://github.com/fetburner/Udon ↩

7. 型推論器と現実 https://github.com/nomaddo/ml-study-typing/blob/master/main.md ↩

8. OCaml でも採用されているレベルベースの多相型推論とは http://rhysd.hatenablog.com/entry/2017/12/16/002048 ↩