Abstracting Gradual Typing Moving Forward: Precise and Space-Efficient (Technical Report)

TL;DR

This paper improves Abstracting Gradual Typing (AGT) by refining its dynamic checks to ensure space efficiency and enforce type invariants, addressing key shortcomings in existing AGT semantics.

Contribution

It introduces a new theoretical framework that recasts AGT's dynamic checks as an abstract interpretation of subtyping, enabling space-efficient and reliable runtime enforcement.

Findings

Refined AGT semantics support proper tail calls.

Ensured enforcement of static type invariants at runtime.

Achieved space-efficient execution in gradually-typed languages.

Abstract

Abstracting Gradual Typing (AGT) is a systematic approach to designing gradually-typed languages. Languages developed using AGT automatically satisfy the formal semantic criteria for gradual languages identified by Siek et al. [2015]. Nonetheless, vanilla AGT semantics can still have important shortcomings. First, a gradual language's runtime checks should preserve the space-efficiency guarantees inherent to the underlying static and dynamic languages. To the contrary, the default operational semantics of AGT break proper tail calls. Second, a gradual language's runtime checks should enforce basic modular type-based invariants expected from the static type discipline. To the contrary, the default operational semantics of AGT may fail to enforce some invariants in surprising ways. We demonstrate this in the $\text{GTFL}_\lesssim$ language of Garcia et al. [2016]. This paper addresses both problems at once by refining the theory underlying AGT's dynamic checks. Garcia et al. [2016] observe that AGT involves two abstractions of static types: one for the static semantics and one for the dynamic semantics. We recast the latter as an abstract interpretation of subtyping itself, while gradual types still abstract static types. Then we show how forward-completeness [Giacobazzi and Quintarelli 2001] is key to supporting both space-efficient execution and reliable runtime type enforcement.