2023 Fiscal Year Annual Research Report
動的型付けと静的型付けを融合した漸進的型付けのメタ理論
| Project/Area Number |
19K20247
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (80828476)
|
|---|
| Project Period (FY) |
2019-04-01 – 2024-03-31
|
| Keywords | プログラミング言語 / 型システム / 漸進的型付け / 多相性 / レコード |
|---|
| Outline of Annual Research Achievements |
当該年度は次の二つの課題について研究を進めた。
【多相性をもつ漸進的型付き言語】前年度までに引き続き、多相性を含む漸進的型付き言語の実装モデルである多相コアーション計算体系の空間効率性についての研究を行った。これまでの研究によりパラメトリシティと空間効率の良い多相コアーション計算は両立しないことがわかっていたが、本年度の研究により、一般的な多相計算体系における重要な性質であるパラメトリシティを一部あきらめる（具体的には動的型が型引数として使われた際にはパラメトリシティを保証しない）代わりに、多相コアーション計算体系を空間効率良く実装できることを証明した。本研究の成果により、多相性をサポートする漸進的型付け言語をより大規模なシステムに適用できる可能性を示すことができた。本成果はPLDI'24にて発表予定である。
【データ構造のための漸進的型付け】本年度は、前年度までに得られた知見を活用し、レコードなどのデータ構造操作を行うプログラミング言語のための漸進型付けの形式化および型システムにおける重要な性質である型健全性を証明した。本研究の成果により、漸進的型付けをデータ構造操作についても適用できることが示され、より多くのプログラムについて静的型付けと動的型付けを状況に応じて使い分けることが可能になると期待できる。今後は型健全性の他に、パラメトリシティといった重要な性質が成り立つことを確認後、国際会議への投稿を計画している。
|
