2019 Fiscal Year Research-status Report
Implementing a Reliable and Expressive Programming Language
| Project/Area Number |
19K24339
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
叢 悠悠 東京工業大学, 情報理工学院, 助教 (30847629)
|
|---|
| Project Period (FY) |
2019-08-30 – 2021-03-31
|
| Keywords | 代数的効果 / 限定継続命令 / プログラム変換 |
|---|
| Outline of Annual Research Achievements |
2019年度は、さまざまな限定継続命令と代数的効果・ハンドラの対応関係について研究した。限定継続命令は、継続の捕捉を引き起こす制御演算子と、継続の範囲を定める限定子からなるが、命令の種類によって、捕捉された継続が使用される場所が異なる。たとえば、Danvy and Filinski の shift/reset 命令では制御演算子、Sitaram の fcontrol/run 命令では限定子が継続を用いた計算を行う。
本研究では、限定継続命令を用いて代数的効果・ハンドラを模倣する。その際、shift/reset を用いると、異なる種類のエフェクトを容易に扱うことができるが、構文上のギャップを埋めるために、プログラムの大幅な書き換えが必要となる。一方、fcontrol/run を用いると、プログラムの構造は保持できるものの、異なるエフェクトを区別するために、タグを導入しなければならない。この２点から、代数的効果・ハンドラは、構文的には fcontrol/run と類似しているが、機能的には shift/reset に近い、という結論が得られた。
この対応関係をふまえて、限定継続命令と代数的効果・ハンドラ間のプログラム変換を定義した。既存研究として、Binernacki らは shift/reset スタイルの限定継続命令をもつ言語と、１種類のみの演算を扱う代数的効果の言語を行き来する変換を定義している。本研究では、代数的効果の言語を複数の演算で拡張したうえで、２つの言語の間に fcontrol/run のバリアントをもつ中間言語を導入した。これによって、構文的な書き換えとブランチの導入・除去を別々に行うことが可能になり、変換の定義がよりシンプルになった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究の最終目標は、依存型と代数的効果・ハンドラを併せ持つ言語を実装することである。2019年度の研究では、限定継続命令と代数的効果・ハンドラの関係を明らかにしたが、これは言語の実装方針を決定するための重要な要素である。なぜなら、適切な限定継続命令を使用することで、実行時のオーバーヘッドを回避したり、プログラム変換の型保存定理の証明を簡易にしたりすることができるからである。
計画通りに実施できなかったこととしては、３月に予定していたポーランド・ブロツワフ大学訪問が挙げられる。これは、訪問時期が新型コロナウィルスの感染拡大と重なってしまい、受け入れ先から延期を要請されたことによるものだが、今後、オンラインで議論をしながら共同研究を進めることを考えている。
一方で、計画外の成果として、Microsoft Research Lab - Redmond の Daan Leijen 氏と共同研究を始め、代数的効果によるヒープの表現について検討した。これは、エフェクトインスタンスの新たな応用例であり、タグ付き限定継続命令の理論とも深く関連している。したがって、この研究を発展させれば、実用面・理論面の両方において、よりインパクトのある成果を出すことができる。
|
| Strategy for Future Research Activity |
2020年度は、実装にフォーカスする。大まかな方針としては、Racket の Turnstile 言語を使って代数的効果とハンドラの依存型システムを実装し、プログラムを実行する際に、fcontrol/run への変換を適用する。
限定継続命令として fcontrol/run を採用するのは、代数的効果・ハンドラとの構文的な類似性により、プログラム変換の定義や、型保存定理の証明が単純になるからである。特に、後者に関しては、shift/reset を用いる場合と異なり、複雑な多相性を導入する必要がなくなる。
実装の具体的な流れは以下の通りである。まず、Chang ら [POPL 2017] の Turnstile 言語を用いて、例外機構をもつ単純型付き言語（1）を実装する。次に、1 に基づいて、代数的効果・ハンドラをもつ単純型付き言語（2）を実装する。これは、1 の例外ハンドラの中で、例外が発生したときの継続を使用できるように拡張することで達成される。単純型付き言語の実装が済んだら、Chang ら [POPL 2020] の Turnstile+ 言語を用いた依存型付き言語の実装に移る。まず、例外機構をサポートする言語（3）から始め、これを代数的効果・ハンドラ（4）に拡張する。このうち、3 を実装する際には、型規則の中で「型の中に例外を起こす項が現れてはならない」というインバリアントを保持する必要がある。
実装が完了したら、依存型と代数的効果・ハンドラを用いたプログラムを作成する。１つ目のステップとして、代表的なエフェクトである例外、状態、非決定性を伴うものを一通りカバーする。２つ目のステップでは、Idris の Effect ライブラリの応用例を再実装し、プログラムの記述量や実行時間を比較する。
|
| Causes of Carryover |
新型コロナウィルスの感染拡大のため、出張が２件取り消しとなった。具体的には、3月2日から4日にかけて佐賀で開催予定であった PPL 2020 と、3月8日から23日に予定していたヴロツワフ大学訪問である。後者については、可能であれば2020年度後半に実施する予定である。
|
Research Products
(1 results)
