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:20 25mTalk | Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System POPL | ||
14:45 25mTalk | Gradual Refinement Types POPL Link to publication DOI Pre-print | ||
15:10 25mTalk | Automatically Generating the Dynamic Semantics of Gradually Typed Languages POPL | ||
15:35 25mTalk | Sums of Uncertainty: Refinements go gradual POPL |