Theory of Gradual Typing for Modern Programming Languages

2020 Fiscal Year Final Research Report

• Project/Area Number: 17H01723
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Kyoto University
• Principal Investigator: Atsushi Igarashi 京都大学, 情報学研究科, 教授 (40323456)
• Co-Investigator(Kenkyū-buntansha): 馬谷 誠二 神奈川大学, 理学部, 准教授 (40378831) ; 中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581) ; 海野 広志 筑波大学, システム情報系, 准教授 (80569575)
• Project Period (FY): 2017-04-01 – 2021-03-31
• Keywords: 漸進的型付け / プログラミング言語 / 型システム

Outline of Final Research Achievements

Gradual typing is a programming-language technique that allows statically typed and dynamically typed parts to coexist in a single program. We have studied the theoretical foundations for applying this technique to advanced programming languages. The main result is computational calculi that introduce gradual typing to advanced programming language mechanisms such as polymorphism, session types, refinement types, nondeterminism, ML type inference, and intersection types; we have proved its properties (such as type safety). In addition, we improved space-efficient coercions that have been proposed as an implementation technique for gradual typing by coercion passing style compilation, which we implemented and evaluated.

Free Research Field

プログラミング言語

Academic Significance and Societal Importance of the Research Achievements

漸進的型付けの概念は、JavaScript に静的型を導入した TypeScript の登場などにより、現実のプログラミング言語にも適用され始めているが、先進的な型機構とどう共存できるか明らかではなく、また実行時オーバーヘッドが大きいことが本格的な導入の障壁になっていた．本研究成果は、漸進的型付けを先進的なプログラミング言語に導入するための理論的な基盤を整備するものであると同時に、効率的な実行を可能とするコンパイル手法の理論の改良を提案するとともに、実装を通じてその効果を評価したものである．