2019 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 による多相文脈の研究を取りいれた体系のインタプリタ実装を行うとともに，体系の正しさ(表面言語から中間言語への変換が型付けを保存すること，中間言語が型安全であること)などを示すことに成功した．現在論文を準備中である．また，交差型を取り入れた顕在的契約計算の研究を行いAPLAS2019で発表した．これにより，「ＡかつＢかつ…」というような仕様を列挙するような形で記述される契約についての動的検査の方法が明らかになった．
課題(2)の計算効果をもつ言語のための統一的な漸進的型付けについては，計算効果を一般的に扱う枠組みであるエフェクトハンドラーと多相性とを安全に組み合わせる研究を進めた．多相エフェクトのシグネチャ(型)を一定の形に制限し，エフェクトハンドラーがその型の制約を満たすよう実装されていれば，ユーザープログラム側に値制限などの制限を課さず素朴な多相型システムで型付けできれば全体として型安全であることを示すことに成功した．(投稿中)．
課題(3)の漸進的型付けの効率的な実装技術の理論については，昨年から続けているコアーション渡しによるコンパイル手法の研究を発展させ，インディアナ大学の研究グループがオープンソースで開発している Grift という漸進的型付け言語のコンパイラに組込むこと成功した．このコンパイラで各種ベンチマークプログラムで性能比較実験を行い，数倍のオーバーヘッドがかかるものの，末尾呼出しに関わるコアーションの合成ができ，末尾再帰関数でもスタックオーバーフローを起こしてしまうことがあるという問題を解決できることが確認できた．この成果はECOOP2020にて発表予定である．
|
| Research Progress Status |
令和元年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
令和元年度が最終年度であるため、記入しない。
|
Research Products
(20 results)
