ML系言語の型エラー報告を改良する

さて、お約束していた OCaml の型エラーメッセージ改良のための改造、ある程度形になりましたので、公開します。

hg clone -b typeloc https://bitbucket.org/camlspotter/mutated_ocaml

ビルドは configure の後、 make core coreboot world です。インストールなさる場合は既存の OCaml システムを潰さないように注意してください。インストールなしにトップレベルを試したい場合は ./ocaml -I stdlib 。といってもまだコンセプトが理解できる程度にしか動作せずまだまだ不完全です。バグもあるかと思います。

さてここから簡単にアイデアを説明します。MLの型推論についてある程度の知識が必要です。

HM 型システムではプログラムの各所を見ながらそれぞれが要求する型の情報を制約として集め、解の存在を探します。このシステムは上手くできていて、全ての制約を集めてから解の存在を探す必要はありません。制約が見つかるごとに型の単一化を行い、単一化に失敗したら解の非存在がその時点で示せ、型エラーとして報告できるのです。（実際の OCaml の型推論ではバックトラックを行うこともあるので、厳密にこう一直線に進むわけではありませんが、大筋としてはやはり単一化に失敗→即型エラーの図式は変わりません）

さて、通常の型推論での型エラー報告では、この最後に行った（そして失敗した）単一化に関して、この単一化を引き起こした型の制約を導入したプログラムの副式の位置をエラー箇所として指摘します。プログラマはその箇所を中心に型エラーを引き起こしている問題点を探し、修正する訳ですが、場合によってはこの修正するべき場所が型推論器が指摘したエラー箇所と全く違った場所になる事があります。これが ML や Haskell の型エラーの修正が難しく感じる一因になっています。

何故こんな事が起こるのか。それは、実はそれ以前に導入した型の制約、そしてそれを導入したプログラムの副式にこそ問題があったのだが、その時点ではそれを発見するに足る制約がまだ足りなかったからです。最後の制約による単一化で初めて顕在化した、といえるでしょう。理想的にはこの「都合の悪い、問題を起こしている型の制約と副式の位置」をドンピシャで指摘できれば良いのですがそんなことはできません。型システムは全体の解の有無を示せるだけで、人間様にとってどこが都合が悪いかなんて事は書いている本人にしかわからない。

プログラムの型推論中に各副式の型は次第に自由型変数（制約なし）から、型の単一化を繰り返す事により、だんだんと具体的な型に変化していきます。例えば 'a が int になったり、 'b が 'c -> 'd になったり。このように、各副式の型制約を追加すると、型変数だった型に型コンストラクタ (int や ->)が導入されていきます。そしてどこかで、例えばこの int と 'c -> 'd を単一化しようとすると失敗し型エラーとなります。この int と -> の矛盾がなければ単一化に成功したはずです。どの副式がこの型コンストラクタ達を導入したのでしょうか。

これがアイデアです。型推論に失敗した場所を報告するよりも、型推論の失敗の原因となった型コンストラクタ、型制約の導入された場所を報告したほうがより修正するべき場所に近い型エラーレポートになるのではないか。

実際に使ってみるとこれが確かに中々よい。通常の型エラーレポートでは「ここの時点でエラーを見つけました。ここでこの型とこの型の単一化に失敗しました」と言われても、

そもそもなぜその二つの型になるのか良くわからない…

となる場合がままありますが、型制約が導入された場所は文面上からも明らかで、例えば int ならば必ずそこに数字が書いてあるし、-> ならば必ずλ抽象か関数適用が書いてある。なので当然で驚きはありません。どちらかというと、

これがこの型になるのはわかる。これもこの型になるのはわかる。え、なんでこの二つが単一化されてしまった？

と思うものです。もちろん、指摘された二箇所（型コンストラクタ二つの齟齬が見つかるわけだから二箇所です）の副式のいずれかが必ず修正するべき位置とは限らないのですけれども。

このアイデアはもともと私の同僚である Lennart ( http://en.wikipedia.org/wiki/Lennart_Augustsson ) が思いついて私達の仕事で使っている Haskell の型推論器に実装されてたものです。これを実装するためには全ての型コンストラクタ(というか副型式)に、この型コンストラクタはコードの何処で導入されたのかを記録せねばなりません。この改造がやりやすいかどうかは元の型システムの実装に依存するので、例えば GHC のチームにはこのアイデアを既に伝えてあるそうですが難しいのか実現されていないようです。幸い OCaml では第一歩はやりやすかったので実装してみました。といっても結構トリッキーなのですけれども。

Opa でも同じ事が!

Opa の世界でも全く同じ事をしている人が! もういいや、下書き途中だけど記事出しちゃいますね: http://blog.opalang.org/2012/07/programming-tools-ux-better-type-error.html