|
研究計画に書いてあるOCamlの型付き中間言語の導入を目指しながら、今年は主に現在の型システムの把握と型付き中間言語導入のための調整を行った。
OCamlの型システムが複雑で、実装に使われる道具が必ずしも通常の理論の紹介に沿っていないため、それを正確に把握する必要がある。例えば、型変数のスコープや一般化に単一化などで変わる導入レベルという数値が使われていて、それについての研究論文はない。しかも、この値は型変数以外にも、型定義のスコープの判定にも使われており、型システムの健全性で重要な役割を果している。しかしながら、モジュールシステムとの干渉が詳しく調べられておらず、実際にファンクター(モジュール間の関数)を使うと正しく動かない場合を見付けた。今後、そういうことが起きないように、モジュールにおける型変数レベルの明確な定義を導入し、システムを修正し、既存プログラムへの影響を最低限に抑えた。新しい定義は中間言語との相性がよくて、スムーズな導入を可能にするはずだ。
それ以外にも、GADTの網羅性に関わる問題を修正した。網羅性は通常型システムの一部と認識されないが、バグがあると正しくないプログラムが実行され、予期できない動作が起きる可能性がある。これをどう中間言語で扱うかについて検討した。
また、フランスでPierrick Coudercに会い、彼が進めている型付け語の構文木の型の再確認を行うプロジェクトについて議論した。このプロジェクトはこちらのプロジェクトと補完的な関係にあり、バックエンドでの変換には対応していないが、フロントエンドのバグの発見に貢献できるものだ。
|
