信頼性と表現力を兼ね備えたプログラミング言語の実装
【研究キーワード】
代数的効果 / 限定継続命令 / 依存型 / プログラム変換 / 型理論 / 副作用 / 継続
【研究成果の概要】
2021年度は、(1) 名前付きハンドラの理論と応用、(2) control/prompt 演算子の型システム、および (3) shift0/dollar 演算子と代数的効果・ハンドラの関係性について研究を行った。
名前付きハンドラは、同じエフェクトの異なるインスタンスを区別するための概念である。名前付きハンドラの形式化はいくつか存在するが、いずれも特殊な型判断や依存型を要求するため、既存の言語に導入することが困難である。本研究では、高階の多相型を用いて名前付きハンドラの型付けを行うことで、より単純な型システムを与えた。また、Microsoft Research の共同研究者および所属研究室の学生とともに、名前付きハンドラを用いたニューラルネットワークや型推論アルゴリズムの実装を行った。現在、これらの研究成果をまとめた論文を国際会議 OOPSLA 2022 に投稿中である。
control/prompt は浅いハンドラと類似した意味論を持つ制御演算子である。control/prompt の型システムは過去に与えられているが、捕捉した継続の呼び出し文脈に関する制約が課されている。本研究では、関数によって呼び出し文脈が表現された CPS 変換から型制約を導出することで、より一般的な型システムを与えた。この研究成果は国際会議 FSCD 2021 で発表しており、国際論文誌 LMCS の特集号への推薦論文として選ばれた。
shift0/dollar は深いハンドラと同等の表現力を持つ制御演算子である。本研究では、既存研究によって与えられた両者の間の相互変換を利用して、深いハンドラのプログラム変換と型システムを導出した。この研究成果は国際シンポジウム TFP 2022 で発表している。
【研究代表者】
【研究種目】研究活動スタート支援
【研究期間】2019-08-30 - 2023-03-31
【配分額】1,950千円 (直接経費: 1,500千円、間接経費: 450千円)