多機能型システムを持ったプログラミング言語のための型付き中間言語の設計

2017 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は数人の研究者が蜜に連絡を取り、開発を行っていたが、2016年の暮れから、GitHubにコードを移し、多くの人が貢献できるようにした。結果的には、外部から提供されるコードが多くなり、特に型検証器は今までと違い、その変遷を知らない人が手を加えるようになった。
それを考えると本プロジェクトがより重要になるが、中間言語の新規導入だけでなく、型検証器自体をより安全で拡張しやすい形に変更する必要性が明確になった。その問題についてOCamlの他の開発者と相談し、制約解消をベースにした型検証器とその出力としての中間言語を作ることになった。
そのために言語全体の明確な定義が必要なので、今年度はそれを手掛けた。Leo Whiteのアイデアを元に、モジュールシステムの形式化を始めた。また、再帰型とオブジェクトおよび多相ヴァリアントがOCamlのコア言語の重要な特徴なので、既に作ってあった構造的多相性と再帰型を含めたコア言語をベースにして、それをよりOCamlに近づけるための準備を始めた。
ただ、OCamlのコア言語がラベル付き引数やGADTなど、それ以外の多くの機能を持っているので、それら全部を含めた定義を形式化しなければならず、まだ完成していない。その傍らで、現行の型検証器の修正や拡張を続けているので、その変更も反映して行かなければならない。特にGADTに関する様々な改良が型検証の定義に関わるので、慎重に進めている。

Current Status of Research Progress

4: Progress in research has been delayed.

Reason

目標に型検証器の刷新が加えられたことで、デザインを考えなおす必要があった。

Strategy for Future Research Activity

概要に書いたように、今後は言語仕様を完成させ、制約解消に基いた型検証器と型付き中間言語を作る予定である。
そのために、フランスのINRIAのFrancois PottierやDidier RemyとイギリスのOCamlLabsの方たちの協力が得られる。

Causes of Carryover

今年度は予定より海外出張が少かったので、余剰金ができたが、元々最終年度の予算が少く見積ってあったので、来年度は旅費などとして使用する予定である。