Prolog なら簡単に型チェッカが書ける，とか言ったが，すまん．ありゃ嘘だった．
まぁ，Prolog だと，プログラムを項として扱うと分解 (マッチング) が面倒だし，リストとして扱うとカンマで区切らないといけないから，どっちにしろ TAPL とかで扱っている形とかけ離れてしまうという．
そんなこんなで，いわば S 式で書く Prolog，ET 言語の出番ですな．一番使い慣れてるし．
例題プログラムは，TAPL の let-polymorphism のやつ．
let double = λ f:X -> X . λ a . f(f(a)) in
let a = double succ 1 in
let b = double not true in
...
というやつ．
しっかし，パーサを書くのは面倒なので，手抜きさせてください．問題を S 式で与えます．あと，ET では，*var みたいにアスタリスクを付けると変数になるので，識別子に制限はありません (個人的には，乗算やポインタのイメージが付きまとうので，?var とかの方が良かったのではないかと思う．ちなみに ? は，他の全ての変数にマッチしないことが保障される無名変数 (ワイルドカード) として扱われます)
(test) --> (= *F (*X -> *X)), // f:X -> X のつもり．下の式にインラインで書いても良いけど
(= *double (lambda (*F *A) (*F (*F *A)))),
(= *a (*double succ 1)),
(= *b (*double not true)),
(typeInf *a),
(typeInf *b).
あと，推論規則は，テキトーに必要最小限のを，パターンマッチ使いまくりで，IF-THEN ルールをひたすら書いて行きます．
(typeInf1 () ()) -->.
(typeInf1 (*F | *rest) (succ | *rest1))
-->
(= *F (Num -> Num)),
(typeInf1 *rest *rest1).
(typeInf1 (*F | *rest) (not | *rest1))
-->
(= *F (Bool -> Bool)),
(typeInf1 *rest *rest1).
(typeInf1 (*A | *rest) (true | *rest1))
-->
(= *A Bool),
(typeInf1 *rest *rest1).
(typeInf1 (*A | *rest) (*n | *rest1)),
{(number *n)}
-->
(= *A Num),
(typeInf1 *rest *rest1).
(typeInf2 ((Num -> Num) *X) *R)
-->
(typeInf2 *X Num),
(= *R Num).
(typeInf2 ((Bool -> Bool) *X) *R)
-->
(typeInf2 *X Bool),
(= *R Bool).
(typeInf2 Bool *R)
-->
(= *R Bool).
(typeInf2 Num *R)
-->
(= *R Num).
んでまぁ，あとは
// 間違い ！！
(typeInf ((lambda *parm *body) | *args))
-->
(typeInf1 *parm *args),
(print (lambda *parm *body)).
とか書きたくなるところですが，これだと *a と *b で型変数が共有されてしまうので，let-polymorphism にならない ！！
# *a で *F_a が (Num -> Num) になると，*b での *F_b の型は (Bool -> Bool) だから，*F_a と *F_b が同じ *F として共有されてしまうと全体としては不整合が起きる．
というわけで，変数をコピーして，フレッシュな変数を用意しましょうという話．
(typeInf ((lambda *parm *body) | *args))
-->
// コピーしてフレッシュな変数を使う
(copy (*parm *body) (*parm1 *body1)),
(typeInf1 *parm1 *args),
(print (lambda *parm1 *body1)),
(typeInf2 *body1 *result),
(print (*parm1 => *result)).
ちなみに，定義されてない述語，number/1 と print/1 と =/2 (unification) と copy/2 は組み込みルールです．
実行してみると，こんな感じ．
[D]>load "C:\\Documents and Settings\\aloha\\デスクトップ\\typeInf.eti"
[D]>(test)
-------------------------D execution ---------------------
(lambda ((Num -> Num) Num) ((Num -> Num) ((Num -> Num) Num)))
(((Num -> Num) Num) => Num)
(lambda ((Bool -> Bool) Bool) ((Bool -> Bool) ((Bool -> Bool) Bool)))
(((Bool -> Bool) Bool) => Bool)
----------------------------------------------------------
succeeded.
(test)
まぁ，S 式とパターンマッチによるルール記述とユニフィケーションと論理変数があると，定理証明器とか型チェッカはすごく簡単に (いや，もちろん，複雑な型体系になったら，それなりに大変だけど，他の言語とかに比べたら相対的に) 書けますよと．
パターンマッチは劇的にプログラムを宣言的にします．
あと，型推論の本質は記号によって組み立てられた構造のユニフィケーションなので．
今回使ったのは，ET の D (eterministic) ルールというサブセットのみで，他にもまぁいろいろ機能はあります．面倒だから説明しないけど(駄目)
たとえば論理変数だけだと表現力に乏しいので，情報 (制約) 付き変数とか．
D ルールのみだと，基本的に Erlang とほとんど同じだと思います．構文とかもかなり似ているような．ただ，値への簡約ではなく，論理変数経由で計算結果を伝えていく点は違いますけど．
| 
