SSブログ

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


nice!(0)  コメント(0)  トラックバック(0) 
共通テーマ:パソコン・インターネット

nice! 0

コメント 0

コメントを書く

お名前:
URL:
コメント:
画像認証:
下の画像に表示されている文字を入力してください。

トラックバック 0

この広告は前回の更新から一定期間経過したブログに表示されています。更新すると自動で解除されます。