2018 Fiscal Year Annual Research Report
Theory of Gradual Typing for Modern Programming Languages
| Project/Area Number |
17H01723
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
馬谷 誠二 京都大学, 情報学研究科, 助教 (40378831)
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | プログラミング言語 / 漸進的型付け / 計算効果 |
|---|
| Outline of Annual Research Achievements |
交付申請書で挙げた3つの課題について以下のような成果が得られた.
課題(1)の,動的な言語機構のための漸進的型付けについては,昨年度構築した理論の制限を，Murase と Nishiwaki による多相文脈の研究を元にして緩めることを考え，体系の変更を行った．また，漸進的型付けとML型推論を組み合わせる際の問題点を発見し，実行時型推論と呼ばれる機構で解決できることを示した(POPL2019で発表)．
課題(2)の,計算効果をもつ言語のための統一的な漸進的型付けについて，ノミナルゲーム意味論の上での漸進的型付けを研究する計画だったが，その元となる公開契約計算のトレース意味論について証明の細部の修正を行っており進展していない．限定継続については，継続操作を行うことを動的に検査する機構を考案し，その意味論の定義と実装を行った．また，ノミナルゲーム意味論の研究が滞ったため，代替アプローチとして計算効果を一般的に扱う枠組みであるエフェクトハンドラーと多相性とを組み合わせる研究を行い，新しいエフェクトハンドラーのための多相型システムの構築に成功した(ESOP2019で発表)．また,昨年度の非決定計算への顕在的契約を導入する理論について成果をまとめ論文発表を行った(PPDP2018で発表)．
課題(3)の,漸進的型付けの効率的な実装技術の理論については,漸進的型付けの元で末尾再帰の最適化が行えないという問題を解決する，コアーション渡しによるコンパイル手法の研究を行った(PPL2019で発表)．
その他,課題(2)に関連して,通信プロトコルを型として記述するセッション型の体系の漸進化の研究についてはより標準的な通信プリミティブのもとでの漸進化の研究を進めた(BEAT2019で発表)．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
3つ挙げた課題それぞれについて，計画通りではない面もあるが，順調に進展している．特に実行的型推論については，計画からは外れた予想外の結果だが，漸進的型付けを実際のプログラミング言語に適用する際に重要な問題を解決するものである．ノミナルゲーム意味論については進展がなかったが，エフェクトハンドラーという計算効果一般に対する別のアプローチに着手でき，予備的な結果も得ることができた．これを漸進的型付けに反映していく．非決定計算への顕在的契約を導入する理論も含め，これらの結果は，いずれも国際会議(特に POPL, ESOP はトップカンファレンス)で発表済である．(3)の結果はまだ国内発表に留まっているが，ポテンシャルの高い研究だと考えている．さらに，これまでの結果についても洗練した上で学術雑誌への投稿が済んでいるものもあり，さらなる成果が期待できる．
|
| Strategy for Future Research Activity |
順調に進んでいるため，大きな研究計画の変更は必要ない．ノミナルゲーム意味論については保留しているが，エフェクトハンドラーの研究について，研究協力者が現れており，さらに研究が推進できそうな手応えを得ているのでその方向で推進する．
以下，個別の課題について．課題1の，動的な言語機構(特にコード生成)のための漸進的型付けについては，このままの方針で進めればよい．課題2の限定継続の研究については，成果の取り纏めと論文発表を行う予定である．課題3については，コアーション渡しによる漸進的型付けのコンパイル手法研究を推進する．
|
