2021 Fiscal Year Research-status Report
動的型付けと静的型付けを融合した漸進的型付けのメタ理論
| Project/Area Number |
19K20247
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 助教 (80828476)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | プログラミング言語 / 漸進的型付け / 多相性 / 継続渡し形式 |
|---|
| Outline of Annual Research Achievements |
当該年度は次の二つの課題について研究を進めた．
(1)多相コアーション計算体系：昨年に引き続き，多相性を含む漸進的型付き言語の実装モデルである多相コアーション計算体系について研究を行った．その結果，漸進的型付けでパラメリック多相を保証するための仕組みである動的名前生成を使用する場合，漸進的型付けの空間効率性（プログラムの実行にかかる空間消費量が元のプログラムから推測することができるという性質）が成り立たないことがわかった．この成果は国際ワークショップ Scheme and Functional Programming 2021 で発表済みである．また逆に，動的名前生成が多相コアーション計算体系のプログラムが空間効率的でなくなることの唯一の原因であることも示した．以上の成果をまとめた論文を国際会議に投稿中である．
(2)多相性の下での継続渡し形式への変換：多相的エフェクトハンドラの漸進的型システムを与えることを念頭に，その基礎付けとなり得る継続渡し形式(Continuation-Passing Style; CPS)への変換について研究を行った．その結果値呼び出しで型情報が暗黙的である多相型計算体系 Implicit System F に対し継続渡し形式への変換を与え，さらにそれがプログラムの型付けと意味を保存することを示した．以上の成果をまとめた論文が国際会議 ICFP 2021 に受理され，発表済みである．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
多相コアーション計算体系（より一般的には動的名前生成をサポートする漸進的型付き言語）について当初は空間効率性が成り立つと予想していたが，その予想に反し空間効率性が成り立たないこと，動的名前生成がその唯一の原因であることなど，当初の想定していた以上の成果が得られた．また Implicit System F に対し型付けと意味を保存するような継続渡し形式への変換を与えることができるかは長年の未解決問題であったが，それを解決したことで一定の成果を得たと考えている．一方当初予定した列多相をサポートする漸進的型システムの研究については十分簡素なモデルが得られず新たに論文としてまとめる段階には至っていない．以上を総合的に評価し，進捗状況についてはおおむね順調に進展していると考える．
|
| Strategy for Future Research Activity |
列多相性を導入した漸進的型付き言語の研究を進める．プログラミング言語モデルへの要請として，多くのプログラムを表現することができる一方，簡素であることが求められる．今後の研究でもこの要求を満たす簡素なモデルを得ることを目指すが，難しい場合は応用として想定していた多相エフェクトハンドラをサポートする漸進的型付き言語を直接与えることを目指す．
|
| Causes of Carryover |
新型コロナウイルスの流行の継続により国内外の学会がオンラインでの開催となり，また研究出張や滞在も控えざるを得ない状況が続いたため．
翌年度の使用計画として，研究環境の整備や研究に必要な物品の購入および情勢が許せば旅費や滞在費として使用することを予定している．
|
