Metatheory for gradual typing integrating dynamic and static typing

2023 Fiscal Year Final Research Report

• Project/Area Number: 19K20247
• Research Category: Grant-in-Aid for Early-Career Scientists
• Allocation Type: Multi-year Fund
• Review Section: Basic Section 60050:Software-related
• Research Institution: National Institute of Informatics
• Principal Investigator: Sekiyama Taro 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (80828476)
• Project Period (FY): 2019-04-01 – 2024-03-31
• Keywords: 漸進的型付け / プログラミング言語 / 型システム / 多相性 / 計算効果

Outline of Final Research Achievements

This research aims to "advance the theory of gradual typing" and "explore the limitation of gradual typing." To this end, we focused on parametric polymorphism, a type-based mechanism to enhance the reuse of program components. In particular, we studied (1) a relationship between parametric polymorphism and space-efficiency, (2) a relationship between parametric polymorphism and data structures, and (3) a relationship between parametric polymorphism and computational effects. The results we obtained can be summarized as follows: (1) We proved that there is a trade-off between parametric polymorphism and space-efficiency in gradual typing. (2) We successfully introduced extensible data structures and row polymorphism into gradual typing. (3) We successfully provided novel polymorphic type systems for algebraic effect handlers, a programming mechanism to implement various computational effects in a programmable manner.

Free Research Field

ソフトウェア

Academic Significance and Societal Importance of the Research Achievements

漸進的型付けは動的・静的型付けの長所を臨機応変に使い分けることのできる新たな型付け方式で、TypeScriptをはじめ、様々なプログラミング言語で実用化されている。一方漸進的型付けによって保証される性質を理論的に解析することは、漸進的型付けの有用性を明らかにする上で重要である。本研究の目的は「漸進的型付けの更なる発展」と「漸進的型付けの限界を探る」ための理論研究を推進することである。またこれらの研究を通じ、将来的に「漸進的型付けの核はどこにあるのか」という根源的かつメタ的な問いを明らかにし、漸進的型付けの研究を正しい方向に加速させ、その抜本的な改革につながることを目指す。