Gradual Typing in an Open World

TL;DR

This paper introduces transient casts for gradually typed Python, providing a proxy-free, sound approach that works reliably even when only part of a program is translated, enhancing trust in type annotations.

Contribution

It formalizes and proves the soundness of transient casts in an open-world setting, addressing limitations of traditional proxy-based approaches in gradually typed languages.

Findings

Transient casts are sound and proxy-free.

Open-world soundness is formalized and proven in Coq.

Reticulated Python effectively integrates gradual typing with open-world guarantees.

Abstract

Gradual typing combines static and dynamic typing in the same language, offering the benefits of both to programmers. Static typing provides error detection and strong guarantees while dynamic typing enables rapid prototyping and flexible programming idioms. For programmers to fully take advantage of a gradual type system, however, they must be able to trust their type annotations, and so runtime checks must be performed at the boundaries of static and dynamic code to ensure that static types are respected. Higher order and mutable values cannot be completely checked at these boundaries, and so additional checks must be performed at their use sites. Traditionally, this has been achieved by installing wrappers or proxies on such values that moderate the flow of data between static and dynamic, but these can cause problems if the language supports comparison of object identity or has a foreign function interface. Reticulated Python is a gradually typed variant of Python implemented via a source-to-source translator for Python 3. It implements a proxy-free alternative design named transient casts. This paper presents a formal semantics for transient casts and shows that not only are they sound, but they work in an open-world setting in which the Reticulated translator has only been applied to some of the program; the rest is untranslated Python. We formalize this open world soundness property and use Coq to prove that it holds for Anthill Python, a calculus that models Reticulated Python.