| 研究課題/領域番号 |
19K24339
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
叢 悠悠 東京工業大学, 情報理工学院, 助教 (30847629)
|
|---|
| 研究期間 (年度) |
2019-08-30 – 2024-03-31
|
| キーワード | 代数的効果 / 制御演算子 / 依存型 |
|---|
| 研究実績の概要 |
2022年度は、制御演算子や代数的効果のコンパイルに関する研究を行った。
制御演算子のコンパイルにはしばしば CPS 変換が用いられる。ここで、すべての部分式に対する継続を明示化してしまうと、変換後のプログラムが大きくなってしまうため、実世界のコンパイラでは選択的な CPS 変換を採用し、複雑な制御を伴う部分式のみを CPS に書き換えることが多い。これを依存型付き言語で実現する場合、条件文の変換が非自明になることが分かった。純粋な依存型付き言語では、条件文の then 節と else 節の型が条件式の評価結果に依存することが許される。すると、制御演算子を持つ依存型付き言語では、2つの節のエフェクトが条件式に依存することを許すのが自然である。しかし、これを許してしまうと、コンパイル時にエフェクトが定まらないケースが生じる。具体的には、条件式が閉じた式でない場合、それを true あるいは false に評価することができず、エフェクトが不定となってしまう。この発見について TyDe 2022 で口頭発表を行った。
一方、CPS 変換によるコンパイルの正当性を証明するための方法として、CPS 変換とその逆変換がリフレクションとよばれる関係を満たすことを示すという方法がある。本研究では、制御演算子のリフレクションを導出する手順に従って、代数的効果のリフレクションを導出することを試みた。その結果、代数的効果に対するもっとも単純な CPS 変換をコンパイル関数として用いた場合、リフレクションを得ることが困難であることが分かった。原因としては、深いハンドラの意味論がオペレーションの CPS 変換に組み込まれていること、および純粋な継続とハンドラの return 節が変換によって統合されてしまうことが挙げられる。この発見について PEPM 2023 で口頭発表を行った。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
上記の研究成果は、いずれも本研究で開発するプログラミング言語の効率・信頼性の向上につながるものである。
制御演算子や代数的効果を用いるプログラムでは、条件文の then 節と else 節の片方が純粋で、もう片方が純粋でないことがしばしばある。このような条件文に型を付ける際には、純粋な節を純粋でないものとして見做すことで、2つの節のエフェクトを揃えるのが一般的である。しかし、コンパイルを行う際には、純粋な式は形を変える必要がないのに対し、純粋でない式は CPS に書き換える必要がある。そのため、純粋でないものとして扱う式が多いほど、コンパイル後のプログラムのサイズが大きくなり、その分実行時間も多くかかる。TyDe 2022 で発表した困難を解決し、選択的な CPS 変換を定義することができれば、純粋な式をそのまま純粋な式として扱うことが可能になり、コンパイル時のプログラムの肥大化を防ぐことができる。
また、依存型付き言語は、安全性が重要視される場面で使用されることが多い。なぜなら、依存型を用いるとプログラムの詳細な仕様を表現でき、型付きのプログラムを書くことで仕様を満たすことの保証を得ることができるからである。ただし、この保証はコンパイラが正しいことを前提としている。具体的には、コンパイラが型と意味を保持したままプログラムを機械語に変換した場合にのみ、仕様通りの動作が期待できる。PEPM 2023 で発表した困難を解決し、代数的効果のリフレクションを得ることができれば、代数的効果をもつ言語のコンパイラが正しいことを形式的に証明できるようになり、その結果として実行時の安全性を保証することが可能になる。
|
| 今後の研究の推進方策 |
2023年度の主な目標は、2022年度に発見した困難を解決することである。
制御演算子のコンパイルに関しては、部分評価のテクニックを応用することを考えている。具体的には、型の中に出現する項に対して、静的に与えられている情報をもとにできるだけ評価を行う。これによって条件部分の値を求めることができれば、条件文全体のエフェクトを定めることが可能になる。
代数的効果のリフレクションについては、Hillerstrom ら 2020 の CPS 変換をコンパイル関数として用いることを考えている。この変換は単純な CPS 変換と異なり、ハンドラの意味論をハンドラの変換規則に持たせているほか、継続と return 節を別々に扱っている。そのため、単純な CPS 変換を用いたときに生じた問題を回避できると予想される。一方で、変換自体が複雑であるため、リフレクションの証明において新たな困難が生じる可能性がある。
上記に加えて、名前付きハンドラとプロンプトタグ付きの制御演算子の関係性に関する研究も行う。これらは複数のファイルや状態などを扱うために有用な機構であり、C++ や Haskell といった言語に実装されている。両者の間に型と意味を保存する変換することができれば、安全性や正当性を保持したまま、一方の機構を他方の機構によって容易に実現することができる。
|
| 次年度使用額が生じた理由 |
当初は ICFP 2022 に現地参加する予定であったが、その前に海外出張が続いたため、オンライン参加に切り替えた。これによって生じた次年度使用額は、ICFP 2023 への参加に伴う旅費として使用する予定である。
|
