2021 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 – 2023-03-31
|
| Keywords | 代数的効果 / 限定継続命令 / 依存型 |
|---|
| Outline of Annual Research Achievements |
2021年度は、(1) 名前付きハンドラの理論と応用、(2) control/prompt 演算子の型システム、および (3) shift0/dollar 演算子と代数的効果・ハンドラの関係性について研究を行った。
名前付きハンドラは、同じエフェクトの異なるインスタンスを区別するための概念である。名前付きハンドラの形式化はいくつか存在するが、いずれも特殊な型判断や依存型を要求するため、既存の言語に導入することが困難である。本研究では、高階の多相型を用いて名前付きハンドラの型付けを行うことで、より単純な型システムを与えた。また、Microsoft Research の共同研究者および所属研究室の学生とともに、名前付きハンドラを用いたニューラルネットワークや型推論アルゴリズムの実装を行った。現在、これらの研究成果をまとめた論文を国際会議 OOPSLA 2022 に投稿中である。
control/prompt は浅いハンドラと類似した意味論を持つ制御演算子である。control/prompt の型システムは過去に与えられているが、捕捉した継続の呼び出し文脈に関する制約が課されている。本研究では、関数によって呼び出し文脈が表現された CPS 変換から型制約を導出することで、より一般的な型システムを与えた。この研究成果は国際会議 FSCD 2021 で発表しており、国際論文誌 LMCS の特集号への推薦論文として選ばれた。
shift0/dollar は深いハンドラと同等の表現力を持つ制御演算子である。本研究では、既存研究によって与えられた両者の間の相互変換を利用して、深いハンドラのプログラム変換と型システムを導出した。この研究成果は国際シンポジウム TFP 2022 で発表している。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
2021年度の研究成果は、本研究課題の目標であるプログラミング言語の安全性保証および実用性向上に直接つながるものである。まず、高階の多相型に基づく名前付きハンドラの形式化を確立したことにより、ハンドラの名前がエスケープして計算が失敗することをコンパイル時に検知できるようになった。次に、control/prompt 演算子の一般的な型システムを与えたことにより、浅いハンドラに対する型主導の最適化手法を開発する土台が整った。さらに、shift0/dollar 演算子の理論を利用した深いハンドラの意味論を与えたことにより、制御演算子の最適化手法を代数的効果・ハンドラのコンパイルに活用する可能性を拓いた。
上記の結果はいずれも依存型を持たない体系で得られたものであるが、いずれも依存型付きの体系に拡張できる見通しが立っている。たとえば、高階の多相性は Coq や Agda といった依存型付き言語でサポートされている概念である。また、制御演算子の依存型システムは研究代表者の博士論文ですでに与えられている。
より間接的な成果としては、前年度から所属研究室の学生および海外の研究者と行っている共同研究の進展が挙げられる。一つ目に、テュービンゲン大学との研究で、Effekt 言語に双方向エフェクトを導入した。この成果について、研究室の卒業生が TyDe 2021 で発表を行っている。二つ目に、Microsoft Research との研究で、Koka 言語の型推論アルゴリズムと最適化手法を開発した。これらについても、研究室の学生が TFP 2022 で発表している。
|
| Strategy for Future Research Activity |
2022年度は、前年度の研究成果に基づき、代数的効果・ハンドラのコンパイルに有用なプログラム変換を開発する。代数的効果・ハンドラをサポートする言語の多くは、ユーザのプログラムを CPS 形式に変換することで、継続の捕捉およびハンドラへのジャンプという大域的な制御を除去している。関数型言語では CPS 形式での最適化が盛んに研究されてきたが、一方で、直接形式に向いている最適化手法も多く知られている。そこで、本研究では CPS 形式から直接形式へのプログラム変換を定義する。変換のアルゴリズムは、Biernacki ら [PPDP 2021] によって与えられた、shift0/dollar 演算子に対する直接形式への変換を参考にして設計する。型保存性については、Barthe ら [HOSC 1999] によって与えられた、ラムダキューブに対する直接形式への変換をヒントにして保証する。
これに加えて、依存型と代数的効果・ハンドラのより大規模な応用例を考案する。一例として、名前付きハンドラを用いたニューラルネットワークの実装に依存型を導入することで、各ニューラル層の間の重み行列に正確な型を付けることが可能になり、それによって参照の安全性を保証することができるようになる。別の例として、名前付きハンドラによる型推論アルゴリズムの実装と依存型を組み合わせることで、単一化の正しさを型レベルで表現することが可能になり、それによって型推論の健全性を保証することができるようになる。
|
| Causes of Carryover |
新型コロナウィルスの感染拡大により、対面での参加を考えていた国際学会がオンライン開催になったため。また、同じ理由により、海外研究機関の訪問が延期となったため。
|
