Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System
Gradual typing combines static and dynamic typing in the same language, offering programmers the error detection and strong guarantees of static types and the rapid prototyping and flexible programming idioms of dynamic types. Many gradually typed languages are implemented by translation into an untyped target language (e.g., Typed Clojure, TypeScript, Gradualtalk, and Reticulated Python). For such languages, it is desirable to support arbitrary interaction between translated code and legacy code in the untyped language while maintaining the type soundness of the translated code. In this paper we formalize this goal in the form of the open-world soundness criterion. We discuss why it is challenging to achieve open-world soundness using the traditional proxy-based approach for higher-order casts. However, the transient design satisfies open-world soundness. Indeed, we present a formal semantics for the transient design and prove that our semantics satisfies open-world soundness. In this paper we also solve a challenging problem for the transient design: how to provide blame tracking without proxies. We define a semantics for blame and prove the Blame Theorem. We also prove that the Gradual Guarantee holds for this system, ensuring that programs can be evolved freely between static and dynamic typing. Finally, we demonstrate that the runtime overhead of the transient approach is low in the context of Reticulated Python, an implementation of gradual typing for Python.
Fri 20 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
| 14:20 - 16:00 | Gradual Typing and ContractsPOPL at Auditorium Chair(s): Ronald Garcia University of British Columbia | ||
| 14:2025m Talk | Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System POPL | ||
| 14:4525m Talk | Gradual Refinement Types POPLLink to publication DOI Pre-print | ||
| 15:1025m Talk | Automatically Generating the Dynamic Semantics of Gradually Typed Languages POPL | ||
| 15:3525m Talk | Sums of Uncertainty: Refinements go gradual POPL | ||
