2017 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)の，動的な言語機構のための漸進的型付けについては，コード片をデータとして扱えるような言語のモデルを設定し，そのモデルに実行時にコード片の型検査を行う機構をキャストの一種として導入し拡張を行い，操作的意味論や型付け規則の形式化を行った．そして，このモデルが漸進的型付け体系としての基本的な性質を満たすことを一部証明した．課題(2)の，計算効果をもつ言語のための統一的な漸進的型付けについては，数年前に村井らが研究した，公開契約計算のトレース意味論について研究を進め，操作的意味論に対して完全抽象的(fully abstract)なトレース意味論の構築に成功した．また，非決定計算に顕在的契約を導入したような言語のモデルについての研究を行い，素朴に導入すると型に現れる契約情報が無意味なものになってしまうこと，そして，非決定計算の意味論を工夫することによって，その問題が克服できることがわかった．課題(3)の，漸進的型付けの効率的な実装技術の理論については，二階の型理論である System F の漸進的型付け拡張の研究の一環として研究を行った．一般に漸進的型付き言語は実行時型検査を行いながらプログラム実行が進むために，型情報をプログラム中や実行時に保持する必要がある．これを素朴に二階の計算体系で考えると，型変数を介した型情報の受渡しのオーバーヘッドが発生することになる．この問題に対して，実行時に型情報を保持する必要があるかどうかを静的に解析し，必要のない部分については型情報を消去する最適化が行えることを示し，インタプリタ実装を行った．
その他，課題(2)に関連して，通信プロトコルを型として記述するセッション型の体系の漸進化や，トレース意味論を元にした高階関数の仕様記述ができる動的論理の拡張の研究などを行った．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
３つ挙げた課題それぞれについて着実に研究成果がでてきており初年度の成果としてほ，おおむね順調に進展しているといってよい．課題１のコードをデータとして扱える言語のための漸進的型付け，そして，課題２の非決定計算のための顕在的契約計算に関する研究成果については，まだ論文として発表ができておらず，今後，論文執筆を通じて研究内容を洗練させる必要がある．トレース意味論の完全抽象性については，国内ワークショップで発表を行ったが今後成果を洗練させて国際学術雑誌などでの発表を目指す必要があるだろう．課題３について研究実績の概要で述べた，二階の漸進的型付け体系はトップカンファレンスで発表済である．また，関連する成果である漸進的セッション型，動的論理の拡張研究はいずれもトップカンファレンスで発表済もしくは発表予定であり，今後，本課題の研究との本格的な融合が期待される．
|
| Strategy for Future Research Activity |
課題1の，コードをデータとして扱える言語のための漸進的型付けについては，基盤となる(漸進的型付け導入前の)体系の表現力が弱いことがわかっている．具体的には，コード型にそのコードの型環境情報も含まれているため制約が過度になっている，という問題である．既存の研究で，型環境を抽象化できる型理論が研究されているので，それを利用することを考えている．課題2については，非決定計算の契約計算拡張について研究を進める．また，計算効果一般に対しての漸進的型付けを考えるために，まず，計算効果を統一的に扱えるプログラミング言語のモデルとして限定継続とノミナル・ゲーム意味論を採用し，そのモデル上の漸進的型付けを研究する．限定継続については，これまでの研究で，動的型付と単純型を素朴に組み合わせると，プログラムのかなりの部分が「継続を使うかもしれない」として型付けされてしまい，結果として，制限が強い型システムになることがわかった．今年度はこの問題の解決を図る.一方のノミナル・ゲーム意味論を元にするアプローチについては，動的論理の拡張の研究を出発点として，ここでのトレース意味論をノミナル・ゲーム意味論で置き換えることによって，計算効果を持つ言語一般に対するプログラム検証の理論的枠組みを構築する．課題3については，昨年度の研究で構築した，多相的な顕在的契約計算についての無駄な動的検査の除去を行うためのプログラム変換の理論を発展させ，静的プログラム解析・コンパイル手法へ応用するための研究を行う．
|
-
-
-
-
-
-
-
-
[Journal Article] Gradual Session Types2017
Author(s)
Atsushi Igarashi, Peter Thiemann, Vasco T. Vasconcelos, Philip Wadler
-
Journal Title
Proceedings of the ACM on Programming Languages
Volume: 1 Issue ICFP
Pages: 38:1-38:28
DOI
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
-
-
-
-
-
-
[Presentation] Gradual Session Types2017
Author(s)
Atsushi Igarashi, Peter Thiemann, Vasco T. Vasconcelos, Philip Wadler
Organizer
ACM SIGPLAN International Conference on Functional Programming
Int'l Joint Research
