2020 Fiscal Year Research-status Report
動的型付けと静的型付けを融合した漸進的型付けのメタ理論
| Project/Area Number |
19K20247
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 助教 (80828476)
|
|---|
| Project Period (FY) |
2019-04-01 – 2022-03-31
|
| Keywords | プログラミング言語 / 漸進的型システム / 多相性 / 計算効果 |
|---|
| Outline of Annual Research Achievements |
昨年に引き続き、漸進的型システムで多相性を扱う方法について研究を進めた。具体的には以下のような成果を挙げている。
(1) これまでに考案した列多相性を導入した漸進的型システムは、データ構造を定義するための重要な構築子であるレコードとヴァリアントの両方を含んでいたこともあり、その意味論が複雑なものとなってしまっていた。昨年度はこれを簡素化し、より簡潔な意味論を与えることに成功した。この結果を利用して、今後はパラメトリシティなど、よりプログラムの意味的性質を捉えた定理の証明に取り組む予定である。
(2) 多相性を含む漸進的型システムのためのコアーション計算体系に関して研究を進め、当初想定していたものとは異なるものの、興味深い結果を得た。こちらは今後論文の執筆を予定している。
(3) これまでに考案した多相型を導入したエフェクトハンドラの型システムに関する研究について論文を執筆、関数型言語のトップ国際会議であるICFP2020に採録され、発表も行った。
(4) エフェクトハンドラをはじめとする制御演算子の意味的な基礎となるのが継続渡し形式（CPS）への変換であるが、当該年度に実施した研究により、値呼び出しの多相型計算体系 System F に対し型情報が暗黙的であった場合でも CPS 変換が可能であることを示した。これは制御演算と型推論を含むプログラミング言語に対して漸進的型システムを与える際に有用な知見となると期待される。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
列多相をサポートする漸進的型システムの簡素化や多相的漸進的型システムのコアーション計算体系を与えるなど、多相的漸進的型システムのメタ理論に関する理解が深まった。
また多相的な計算体系に対するCPS変換を与えることで、今後多相漸進的型システムに制御演算子を導入することにも期待がもてる。
成果のうちいくつは学会で既に発表済み、あるいは発表を予定している。特にエフェクトハンドラの多相型システムの研究はトップ国際会議であるICFPに採択され、発表を行った。
以上の成果により、進捗状況についてはおおむね順調に進展していると考えられる。
|
| Strategy for Future Research Activity |
今後は引き続き列多相性を導入した漸進的型システムに関する研究を進め、パラメトリシティなどの証明を行う。またコアーション計算体系については論文の執筆を進める。
さらに、昨年度までの研究から制御演算子、特にエフェクトハンドラに関する理解が大きく深まったため、漸進的型システムへエフェクトハンドラを導入する方法についても研究を進めていきたい。
|
| Causes of Carryover |
新型コロナウイルスの流行の継続により国内・国際会議がオンラインでの開催となり、また国内出張も控えざるを得ない状況が続いたため。
使用計画としては、研究環境の整備および情勢が許せば旅費として使用することを予定している。
|
