Prolog で型チェック [Prolog]
Prolog の力といえば単一化ですが、[1] の記事でやったような型チェックの場合も、同じ型であるかどうかの判断というのは単一化でうまく書けそうです。
型チェックのところだけ書きたいので構文木は適当に与えられているものとします。 整数と真偽値と条件分岐と変数束縛とラムダから成る簡単な言語を想定して Prolog で型チェックを行ってみます。
type_of(Num, _, number) :- number(Num).
type_of(true, _, bool).
type_of(false, _, bool).
type_of(if(Cond, True, False), Env, T) :-
type_of(Cond, Env, bool),
type_of(True, Env, T),
type_of(False, Env, T).
type_of(let(Sym, Val, Body), Env, T) :-
type_of(Val, Env, T2),
extend_env(Env, Sym, T2, Env2),
type_of(Body, Env2, T).
type_of(Var, Env, T) :- atom(Var), apply_env(Env, Var, T).
type_of(lambda(Arg, Body), Env, (T1 -> T2)) :-
extend_env(Env, Arg, T1, Env2),
type_of(Body, Env2, T2).
extend_env(Env, Sym, Val, [Sym:Val | Env]).
apply_env([Sym:Val | _], Sym, Val) :- !.
apply_env([_:_ | Rest], Sym, Val) :- apply_env(Rest, Sym, Val).
ここで a -> b とか a:b は単なる中置演算子で書いた構造で特別なものではありません(それぞれ ->(a,b), :(a,b) と同じ)。
単一化のおかげで Scheme のときのより簡潔に書けているというだけでも大分ありがたいのですが、さらにボーナスがついています。
ちょっとプログラムをテストしてみましょう。
?- type_of(123, [], X). X = number Yes ?- type_of(true, [], X). X = bool Yes ?- type_of(if(1,2,3), [], X). No ?- type_of(if(true,2,3), [], X). X = number Yes ?- type_of(let(x,1,x), [], X). X = number Yes ?- type_of(let(x,false,x), [], X). X = bool Yes ?- type_of(lambda(x,if(x,1,2)), [], X). X = bool->number Yes ?- type_of(lambda(x,if(true,x,2)), [], X). X = number->number Yes ?- type_of(lambda(x,x), [], X). X = _G215->_G215 Yes
特筆すべきは最後のラムダのところです。
まず [1] の記事の実装では関数の引数の型は明示的に書かなければならなかったのですが、ここでは特別な追加実装なしに引数の型推論もしてくれています。type_of(lambda... のところで Arg の型 T1 はインスタンス化されないまま型環境に追加されて後で単一化により型が決まっているわけです。
また最後の例のように何でもいい型は最後まで型がインスタンス化されないということによって表現されます。
Prolog の機能におんぶにだっこになることによってこうしたことが「ただで」手に入ったということですね。
追記:関数適用の文法を含めるのを忘れてた。まあいいか。
[1] http://rainyday.blog.so-net.ne.jp/2008-03-30
コメント 0