| 研究課題/領域番号 |
19K11892
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
松田 一孝 東北大学, 情報科学研究科, 准教授 (10583627)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2023-03-31
|
| キーワード | プログラミング言語 / 関数プログラミング / 双方向変換 / 可逆プログラミング / 線形型システム / 型推論 |
|---|
| 研究実績の概要 |
本研究の目的は一方向プログラミング技術と双方向プログラミング技術の融合により，現実的な労力での双方向プログラミングを行うことができるプログラミング言語の設計である．
双方向プログラミングにおいても，リソースを考慮した型システムである線形型システムは重要となる．これは，大雑把には，ソースからビューへの変換を記述する際において，ソース（の一部）と対応しているデータ（すなわち更新が可能なデータ）をリソースとみなすことができるためである．実際，双方向プログラミングと関連の深い可逆プログラミングにおいても線形型システムはよく用いられている．しかしながら，実用的なプログラミングのための，特に高階関数を許すような線形型システムの研究はいまだオープンなトピックである．特にそうした型システムについては効率的な型推論手法を持つことが期待される．我々は双方向プログラミング言語への応用を目指して，Linear Haskellのコア言語に対するqualified typingに基づく型推論手法を提案した．対象となる型システムでは線形な関数を非線形な文脈で注釈なしに使うことが可能であり，このことは線形とは限らない通常の一方向プログラミングと，線形性が重要となる双方向プログラミングの融合を行うという我々の目的と相性がよいことが期待される．Qualified typingを用いることにより主要型付けを行うことができ，また線形性の制約が局所的になるため効率的な型推論が可能である．また，対象型システムでは線形性の制約と型の制約が独立しているため，線形性に関する量化子除去の技術を応用することにより，qualified typingにおける問題の一つである曖昧な型変数の問題を解決することが可能となっている．
本研究の成果は，国際会議ESOP2020に採録が決定している．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
前述の通り，線形型システムは双方向プログラミング言語において重要である．また，ESOPはプログラミング言語理論分野におけるコンペティティブな国際会議の一つであり，その成果はジャーナルなみの厳しい査読を経たものである．以上の理由から「おおむね順調に進展している」と判断した．
|
| 今後の研究の推進方策 |
今年度の成果の発展としていくつかの方向性が考えられる．
一つの方向性は，作成した線形型システムを利用した双方向プログラミング言語の作成である．可逆プログラミング言語は双方向プログラミングの一種である．可逆プログラムを構成する手法の一つにプログラム逆化（program inversion）がある．その文脈において，部分評価のアイデアを応用した部分プログラム逆化が効果的であると知られている．我々は現在，この部分プログラム逆化のアイデアを応用した線形型付き可逆プログラミング言語を作成中である．この「部分プログラム逆化」の表現には，一方向プログラムと双方向プログラム間のコミュニケーションが必要となり，それを扱うのに線形型システムは有用であると期待される．我々はまず可逆プログラミング言語においてこのアイデアの有効性を確認し，その後そのアイデアを双方向プログラミングに応用することを目指す．
もう一つの方向性は，提案型推論手法の拡張である．たとえば高ランク多相性や型クラス等に拡張できれば，Haskellのような現実に使われる関数プログラミング言語に手法を応用するための第一歩となる．こうした技法は双方向プログラミング言語の設計においても有用であると期待されるものである．
|
| 次年度使用額が生じた理由 |
今年度の成果の発表は2020年度におこなわれる予定であるため，研究発表に関する経費は2019年度ではなく2020年度に執行する予定である．また，執行予定であった物品費の一部は，適切なスペックの製品が見つからなかったため翌年度以降にまわすことにした．
|
