[OOPSLA24] Gradually Typed Languages Should Be Vigilant!

Описание: Gradually Typed Languages Should Be Vigilant! (Video, OOPSLA 2024)
Olek Gierczak, Lucy Menon, Christos Dimoulas, and Amal Ahmed
(Northeastern University, USA; Northeastern University, USA; Northwestern University, USA; Northeastern University, USA)

Abstract: In gradual typing, different languages perform different dynamic type checks for the same program even
though the languages have the same static type system. This raises the question of whether, given a gradually
typed language, the combination of the translation that injects checks in well-typed terms and the dynamic
semantics that determines their behavior sufficiently enforce the static type system of the language. Neither
type soundness, nor complete monitoring, nor any other meta-theoretic property of gradually typed languages
to date provides a satisfying answer.


In response, we present vigilance, a semantic analytical instrument that defines when the check-injecting
translation and dynamic semantics of a gradually typed language are adequate for its static type system.
Technically, vigilance asks if a given translation-and-semantics combination enforces the complete run-time
typing history of a value, which consists of all of the types associated with the value. We show that the standard
combination for so-called Natural gradual typing is vigilant for the standard simple type system, but the
standard combination for Transient gradual typing is not. At the same time, the standard combination for
Transient is vigilant for a tag type system but the standard combination for Natural is not. Hence, we clarify
the comparative type-level reasoning power between the two most studied approaches to sound gradual typing.
Furthermore, as an exercise that demonstrates how vigilance can guide design, we introduce and examine
a new theoretical static gradual type system, dubbed truer, that is stronger than tag typing and more faithfully
reflects the type-level reasoning power that the dynamic semantics of Transient gradual typing can guarantee.

Article: https://doi.org/10.1145/3649842

Supplementary web page: http://olekg.pl/papers/vigilance-tech...

ORCID: https://orcid.org/0009-0002-8850-0984, https://orcid.org/0009-0002-9583-4448, https://orcid.org/0000-0002-9338-7034, https://orcid.org/0000-0001-7424-572X

Video Tags: gradual typing, semantics, logical relations, natural, transient, oopslaa24main-p120-p, doi:10.1145/3649842, orcid:0009-0002-8850-0984, orcid:0009-0002-9583-4448, orcid:0000-0002-9338-7034, orcid:0000-0001-7424-572X

Presentation at the OOPSLA 2024 conference, October 20–25, 2024, https://2024.splashcon.org/track/spla...
Sponsored by ACM SIGPLAN,