はじめてのかたちぇっか

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 とほとんど同じだと思います．構文とかもかなり似ているような．ただ，値への簡約ではなく，論理変数経由で計算結果を伝えていく点は違いますけど．