2016 Fiscal Year Research-status Report
多機能型システムを持ったプログラミング言語のための型付き中間言語の設計
| Project/Area Number |
16K00095
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
J Garrigue 名古屋大学, 多元数理科学研究科, 准教授 (80273530)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | 型システム / 中間言語 / 型健全性 |
|---|
| Outline of Annual Research Achievements |
研究計画に書いてあるOCamlの型付き中間言語の導入を目指しながら、今年は主に現在の型システムの把握と型付き中間言語導入のための調整を行った。
OCamlの型システムが複雑で、実装に使われる道具が必ずしも通常の理論の紹介に沿っていないため、それを正確に把握する必要がある。例えば、型変数のスコープや一般化に単一化などで変わる導入レベルという数値が使われていて、それについての研究論文はない。しかも、この値は型変数以外にも、型定義のスコープの判定にも使われており、型システムの健全性で重要な役割を果している。しかしながら、モジュールシステムとの干渉が詳しく調べられておらず、実際にファンクター(モジュール間の関数)を使うと正しく動かない場合を見付けた。今後、そういうことが起きないように、モジュールにおける型変数レベルの明確な定義を導入し、システムを修正し、既存プログラムへの影響を最低限に抑えた。新しい定義は中間言語との相性がよくて、スムーズな導入を可能にするはずだ。
それ以外にも、GADTの網羅性に関わる問題を修正した。網羅性は通常型システムの一部と認識されないが、バグがあると正しくないプログラムが実行され、予期できない動作が起きる可能性がある。これをどう中間言語で扱うかについて検討した。
また、フランスでPierrick Coudercに会い、彼が進めている型付け語の構文木の型の再確認を行うプロジェクトについて議論した。このプロジェクトはこちらのプロジェクトと補完的な関係にあり、バックエンドでの変換には対応していないが、フロントエンドのバグの発見に貢献できるものだ。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
中間言語の理論的な設計がまだ完成しておらず、実装を始めていない。
しかし、下調べが進んでおり、実装方針も確認できた。
|
| Strategy for Future Research Activity |
当初の予定どおり、中間言語の設計と実装を完成させる予定である。
また、可能な範囲内でCoqでの検証も検討する。場合によってPierrick Coudercとの協力も考える。
バックエンドでの変換について、OCaml Labsが開発するflambdaという枠組みに型の概念をもっと入れるとも検討している。
|
| Causes of Carryover |
年度末の学会出席のために残した金額が大き過ぎた。
|
| Expenditure Plan for Carryover Budget |
次年度の旅費に当てる予定である。
|
