2018 Fiscal Year Annual Research Report
Staged Computing based on Advanced Type Systems
| Project/Area Number |
18H03218
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
浅井 健一 お茶の水女子大学, 基幹研究院, 准教授 (10262156)
Kiselyov Oleg 東北大学, 情報科学研究科, 助教 (50754602)
|
|---|
| Project Period (FY) |
2018-04-01 – 2022-03-31
|
| Keywords | 多段階計算 / プログラム生成 / 先進的型システム / 多相型 / 一般化代数データ型 / 型安全性 / スクープ安全性 / 計算エフェクト |
|---|
| Outline of Annual Research Achievements |
４年間の研究計画の初年度にあたり、先進的型システムをもつ言語をターゲット言語とするプログラム生成の安全性、特に、型安全性とスコープ安全性に関する基礎理論の考察を行った。
ML系プログラム言語が持つlet多相とコード生成と計算エフェクトの３つを併せ持つプログラム言語に対して、素朴な型システムを想定すると、型安全性が壊れることが知られている。そこで、本研究では、このような組み合わせのプログラム言語は、アプリケーション記述において必要、もしくは、有用であることを明らかにし、ついで、このようなアプリケーションを記述できる程度に表現力が強く、かつ、型安全性が成立する程度に制限が効いている言語と型システムを設計した、伝統的に「値制限」と呼ばれる多相型の導入法と、「緩い値制限」と呼ばれる導入法のそれぞれに対して、自然でプログラマにとってわかりやすい制限をもうけて、結果として型安全性をもつ型システムを実現した。このうち、値制限に基づく方法は見通しの良い証明がつくが、緩い値制限に基づく方法は非常に難解な証明が必要であるため、本研究では、サブサンプションとよばれる規則を追加することとした。このルール自体が意味論的に健全であることの証明は次年度以降に行う。
このほか、依存型を持つプログラム言語に対して部分計算などのメタプログラミングを行う場合の型安全性の確保や、近年研究が非常に盛んになっている「代数的効果とハンドラ」に基づいて、プログラム生成との関係や他の言語へのプログラム変換や型の保存性などについて検討を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究はプログラム生成に関する基礎理論から言語設計・実装、そして、アプリケーションの記述までを含んだものであり、本年度の研究では、多相型をもつプログラムの生成について成果を得た。また、プログラム生成で重要となる計算エフェクトの研究においては、「代数的効果とハンドラー」をML系言語に翻訳したり、故ルーティンを持つ言語に変換する研究を行い、そこでも先進的型システムの役割の重要性を解き明かした。これらの成果の論文発表は来年度以降となるが、本研究の中間をなす部分で成果を得ており、研究は順調に進展していると判定した。
|
| Strategy for Future Research Activity |
初年度で得られた基礎理論に基づき多相型を持つプログラムの生成については、型安全に行える言語を得ており、これをプログラム言語として実装し、アプリケーションを記述する必要がある。
２年目以降は、多相型以外の重要な型である一般化代数データ型や依存型を持つプログラムの生成について検討し、初年度と同様な成果を得ることを目標とする。
|
