制約に基づく汎用型推論モジュールの研究

点击翻译按钮获取中文摘要

型推論は、プログラム中に潜むエラーを実行前の段階で捕捉するための重要な技術である。しかし、従来の型推論のアルゴリズムは、対象とする個々の型体系に対して与えられ、しかもそれは型体系がより豊かになればなるほど複雑になる傾向にあった。とくに、多相型を含む型体系において、多相型の型推論を一般的に記述する方法が求められていた。このような問題を解決するため、Odersky, Sulzmann, Wherらは、制約系をベースとしたより一般的な型体系の枠組みであるHM(X)を提案した。しかしながら、HM(X)では、多相型の型付けは制約系によっては特徴づけられていなかった。本研究では、Odersky, Sulzmann, Wherらの研究をふまえ、多相型の型付けをも制約系によって特徴づけするような、型体系を記述する一般的な枠組みを提案した。この枠組みの中では、適切な制約系とその制約解消器を与えれば自動的に型推論アルゴリズムが得られる。この枠組みのなかでは、多相型の型付けを表す汎用的な制約が導入され、この制約を解くことにより型推論を行うことができる。この汎用的型推論の枠組みにおいては、型推論はより柔軟な多相型の使用を可能にする。例えば、分散アプリケーションやトップダウンのプログラム開発など、必ずしも型の定義が先に得られないような場合でも、多相型を扱うことができるようになる。これらの結果を著した論文は、日本ソフトウェア学会学会誌に採録された。