2020 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 – 2022-03-31
|
| Keywords | 代数的効果 / 限定継続命令 / 依存型 |
|---|
| Outline of Annual Research Achievements |
2020年度は、依存型と代数的効果・ハンドラを併せ持つプログラミング言語の実装に取り組んだ。当初の研究計画の通り、実装には Racket 言語を用いた。この言語を採用した理由は、(1) control パッケージに多くの限定継続命令が用意されていること、また (2) turnstile パッケージに依存型付き言語を実装するための機構が用意されていることの２点である。
実装の手順としては、副作用を持たない依存型付きラムダ計算を出発点とし、それに２つの拡張を加えていった。まず、raise と try with による例外機構を追加した。これは、継続を使用できないような代数的効果に対応する。次に、限定継続命令 fcontrol/run を追加した。これは、継続を用いて１種類のエフェクトを処理できるようなハンドラに相当する。
実装を行う過程では、Racket を用いることの利点が実感できた。一つは、プリミティブの限定継続命令が提供されていることにより、開発言語の意味論を直接形式で定義できることである。もう一つは、高度なマクロシステムが整備されていることにより、開発言語の型規則を導出規則の形で直感的に定義できることである。実際、出来上がった実装はコード量が非常に少なく、そのほとんどが型規則を表現する本質的なコードとなっている。
一方で、turnstile パッケージの改善点も複数見つかった。まず、公式ドキュメントに掲載されている言語実装例が少なく、いくつかの API の使用方法が十分に説明されていなかった。また、エラーを解決する際に Racket マクロシステムの知識が必要となるため、パッケージ利用のハードルがやや高く感じられた。このことは turnstile 開発者に報告している。さらに、Scheme 2020 ワークショップで、所属研究室の学生とともに改善策および応用例の提案を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
2020年度の研究により、依存型と代数的効果・ハンドラを併せ持つ小さな言語の実装が達成された。実装した言語で記述可能なプログラムはまだ限定的であるが、2019年度の理論的な研究成果を直接活用できたほか、Racket 言語を用いることの有効性が検証された。
計画通りに実施できなかったことは、2019年度に予定していたポーランド・ブロツワフ大学への訪問、および2020年度に予定していた米国・ノースイースタン大学への訪問である。実施できなかった理由は、新型コロナウィルスの感染状況により、海外への渡航が制限されていたためである。訪問予定であった研究者とはオンラインで何度か議論を交わしたが、オンライン授業や学会の実施・運営などにより十分に時間を取れなかったため、研究期間の延長を申請した。
一方で、当初の計画には盛り込んでいなかった研究成果も得られている。一つは、Microsoft Research の Daan Leijen 氏、および香港大学の Ningning Xie 氏との共同プロジェクトである。彼らとは名前付きハンドラのための型システムを開発しており、現在、国際会議の論文を投稿中である。
二つ目は、スイス・EPFL の Jonathan Brachthauser 氏、ドイツ・テュービンゲン大学の Philip Schuster 氏、および所属研究室の修士課程学生との共同プロジェクトである。彼らとは双方向コミュニケーションを可能にする代数的効果の理論構築と、それに基づいた言語実装を行なっており、現在、国際ワークショップへの投稿論文を執筆中である。
三つ目は、お茶の水女子大学の浅井健一氏、および浅井研究室の修士・博士課程学生との共同プロジェクトである。彼らとは動的な限定継続命令の型システムを開発しており、2021年7月に国際会議 FSCD 2021 でこれまでの成果を発表する予定である。
|
| Strategy for Future Research Activity |
2021年度は理論および実装の拡張を行う。具体的には、Leijen 氏および Xie 氏と開発している名前付きハンドラの型システムを依存型で拡張し、それを Racket 言語で実装する。
研究の流れとしては、まず名前付きハンドラとプロンプトタグ付き限定継続命令の関係を明らかにする。すでに、ブロツワフ大学の研究者によって、名前なしハンドラとタグなし限定継続命令の対応関係が明らかになっている。本研究では、彼らの型システムに名前・タグの情報を保持する環境を追加するとともに、彼らのプログラム変換をハンドラ・名前渡し形式に変更する。
次に、得られた型システムに依存型を導入する。今まで、健全性を保証する目的で「型に現れる項は純粋なもののみ」という制約を設けていたが、拡張後はこれに加えて「名前・タグを含まないもののみ」という制約が必要になると考える。
依存型システムが設計できたら、これを Racket 言語で実装する。Racket の control パッケージには、プロンプトタグ付きの fcontrol/run 命令が用意されているため、プログラムの評価は直接形式で簡潔に記述できると考えられる。
最後に、実装された言語を用いてプログラム例を作成する。実用的な例の一つとして、pretty printer が挙げられる。アイディアとしては、依存型を使用することで正しさを保証しつつ、名前付きハンドラを使用することで動的変数を表現し、実行時の環境に合わせたインデントを実現する。
|
| Causes of Carryover |
新型コロナウィルスの感染拡大により、海外研究機関の訪問が延期になったほか、国際会議がオンライン開催となったため、次年度使用額が生じた。
残りの研究費は、状況が許せば訪問予定であった研究機関や国際会議への渡航費として使用する予定である。また、プログラミング言語理論関連の書籍を購入する予定である。
|
Research Products
(4 results)
