Implementing a Reliable and Expressive Programming Language
| Project/Area Number |
19K24339
|
|---|
| Research Category |
Grant-in-Aid for Research Activity Start-up
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
1001:Information science, computer engineering, and related fields
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
叢 悠悠 東京工業大学, 情報理工学院, 助教 (30847629)
|
|---|
| Project Period (FY) |
2019-08-30 – 2024-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| Budget Amount *help |
¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
Fiscal Year 2020: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2019: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
|
|---|
| Keywords | 代数的効果 / 制御演算子 / 依存型 / 限定継続命令 / プログラム変換 / 型理論 / 副作用 / 継続 |
|---|
| Outline of Research at the Start |
依存型と代数的効果は、それぞれプログラムの仕様の記述と、複雑な動作の実装に役立つツールである。これらを共存させると、信頼性と表現力を両立できると考えられるが、プログラムが仕様通りに振る舞うことの保証や、言語の実装に多大な労力がかかってしまう。
本研究では、代数的効果をもつ依存型付き言語をなるべく低いコストで実装する。アイディアとしては、制御演算子（実行の流れを操作するための演算子）に関する研究成果と、関数型言語 Racket のインフラを利用することで、証明や実装の手順を単純化する。これによって、意図通りに動作するソフトウェアの実装がより現実的になることが期待される。
|
| Outline of Annual Research Achievements |
2022年度は、制御演算子や代数的効果のコンパイルに関する研究を行った。
制御演算子のコンパイルにはしばしば CPS 変換が用いられる。ここで、すべての部分式に対する継続を明示化してしまうと、変換後のプログラムが大きくなってしまうため、実世界のコンパイラでは選択的な CPS 変換を採用し、複雑な制御を伴う部分式のみを CPS に書き換えることが多い。これを依存型付き言語で実現する場合、条件文の変換が非自明になることが分かった。純粋な依存型付き言語では、条件文の then 節と else 節の型が条件式の評価結果に依存することが許される。すると、制御演算子を持つ依存型付き言語では、2つの節のエフェクトが条件式に依存することを許すのが自然である。しかし、これを許してしまうと、コンパイル時にエフェクトが定まらないケースが生じる。具体的には、条件式が閉じた式でない場合、それを true あるいは false に評価することができず、エフェクトが不定となってしまう。この発見について TyDe 2022 で口頭発表を行った。
一方、CPS 変換によるコンパイルの正当性を証明するための方法として、CPS 変換とその逆変換がリフレクションとよばれる関係を満たすことを示すという方法がある。本研究では、制御演算子のリフレクションを導出する手順に従って、代数的効果のリフレクションを導出することを試みた。その結果、代数的効果に対するもっとも単純な CPS 変換をコンパイル関数として用いた場合、リフレクションを得ることが困難であることが分かった。原因としては、深いハンドラの意味論がオペレーションの CPS 変換に組み込まれていること、および純粋な継続とハンドラの return 節が変換によって統合されてしまうことが挙げられる。この発見について PEPM 2023 で口頭発表を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
上記の研究成果は、いずれも本研究で開発するプログラミング言語の効率・信頼性の向上につながるものである。
制御演算子や代数的効果を用いるプログラムでは、条件文の then 節と else 節の片方が純粋で、もう片方が純粋でないことがしばしばある。このような条件文に型を付ける際には、純粋な節を純粋でないものとして見做すことで、2つの節のエフェクトを揃えるのが一般的である。しかし、コンパイルを行う際には、純粋な式は形を変える必要がないのに対し、純粋でない式は CPS に書き換える必要がある。そのため、純粋でないものとして扱う式が多いほど、コンパイル後のプログラムのサイズが大きくなり、その分実行時間も多くかかる。TyDe 2022 で発表した困難を解決し、選択的な CPS 変換を定義することができれば、純粋な式をそのまま純粋な式として扱うことが可能になり、コンパイル時のプログラムの肥大化を防ぐことができる。
また、依存型付き言語は、安全性が重要視される場面で使用されることが多い。なぜなら、依存型を用いるとプログラムの詳細な仕様を表現でき、型付きのプログラムを書くことで仕様を満たすことの保証を得ることができるからである。ただし、この保証はコンパイラが正しいことを前提としている。具体的には、コンパイラが型と意味を保持したままプログラムを機械語に変換した場合にのみ、仕様通りの動作が期待できる。PEPM 2023 で発表した困難を解決し、代数的効果のリフレクションを得ることができれば、代数的効果をもつ言語のコンパイラが正しいことを形式的に証明できるようになり、その結果として実行時の安全性を保証することが可能になる。
|
| Strategy for Future Research Activity |
2023年度の主な目標は、2022年度に発見した困難を解決することである。
制御演算子のコンパイルに関しては、部分評価のテクニックを応用することを考えている。具体的には、型の中に出現する項に対して、静的に与えられている情報をもとにできるだけ評価を行う。これによって条件部分の値を求めることができれば、条件文全体のエフェクトを定めることが可能になる。
代数的効果のリフレクションについては、Hillerstrom ら 2020 の CPS 変換をコンパイル関数として用いることを考えている。この変換は単純な CPS 変換と異なり、ハンドラの意味論をハンドラの変換規則に持たせているほか、継続と return 節を別々に扱っている。そのため、単純な CPS 変換を用いたときに生じた問題を回避できると予想される。一方で、変換自体が複雑であるため、リフレクションの証明において新たな困難が生じる可能性がある。
上記に加えて、名前付きハンドラとプロンプトタグ付きの制御演算子の関係性に関する研究も行う。これらは複数のファイルや状態などを扱うために有用な機構であり、C++ や Haskell といった言語に実装されている。両者の間に型と意味を保存する変換することができれば、安全性や正当性を保持したまま、一方の機構を他方の機構によって容易に実現することができる。
|
Report
(4 results)
Research Products
(16 results)
