型推論とエラーメッセージの可読性

先週の土日を使って、型推論アルゴリズムを実装してみた。id:kkanda:20041004でLLパーサーのエラーメッセージは分かり易くて良いという話をしたが、型推論アルゴリズムを導入した瞬間すべてがぶち壊しになったorz
型推論アルゴリズムとは、制約条件を満たす最も一般的(most general)な型を見つけ出すアルゴリズムである。例えば、組み込み型としてint型とbool型のみを持つ言語があったときに、「x + x」の変数xは二項演算子「+」が両辺にint型の項を取るという制約条件からint型であることが推論される。
型推論アルゴリズムによって、プログラマーは型宣言をいちいちしなくてもプログラム中に存在する矛盾点を見つけ出すことが可能になる。例えば次のif文を見て欲しい。

if x then x + x else x

このif文中の変数xは、guad conditionとしてbool型を期待されつつ、then以降で「+」演算子の引数として渡されているためint型を期待されている。このような制約条件を充足する変数xは存在しないためこのif文は型エラーとなる。実際に今実装中のシステムで実行をした結果は次の通りである。

> lm x. if x then x + x else x;;
type reconstruction...
[?X0=bool int=?X0 ?X0=int ]: constraints
Unsolvable constraints at line 1, col 28

現在のシステムでは、定義域の定まらない変数を許していないためlambda項の内側の式としてif文を記述しているが前述のif文と本質的には変わらない。3行目の括弧内が式から導き出された制約で、「?X0=bool」は、「?X0という型はboolでなければならない」と読む。そのように読み下すと?X0はbool型でありint型でなければならないため確かに矛盾していることがわかる。
ここまではなんら問題はない。問題となるのは4行目の出力である。ここで、Type Checkerは制約を充足できなかったことを伝えることはできるのだが、結局のところxが何型であるのかがわからない。しかも、具体的にどの位置の変数とどの位置とが矛盾しているのかを通知できていない。
素直に型推論アルゴリズムを実装した場合、これが限界でもう少し詳細なエラーメッセージを出力するにはちょっとした工夫が必要となってくる。（つづく）