Gradual typing: a new perspective

By Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, Jeremy G. Siek. 2019

52 citations recorded by the source corpus.

We define a new, more semantic interpretation of gradual types and use it to ``gradualize'' two forms of polymorphism: subtyping polymorphism and implicit parametric polymorphism. In particular, we use the new interpretation to define three gradual type systems ---Hindley-Milner, with subtyping, and with union and intersection types--- in terms of two preorders, subtyping and materialization. We define these systems both declaratively ---by adding two subsumption-like rules--- which yields clearer, more intelligible, and streamlined definitions, and algorithmically by reusing existing techniques such as unification and tallying.

Subfields: Artificial Intelligence, Computer Networks and Communications, Program Analysis & Verification, Software Engineering

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Networks and Communications

In Program Analysis & Verification

In Software Engineering

Citations in the corpus

Do Machine Learning Models Produce TypeScript Types that Type Check? (2023, methodology): “The earliest approach was a variation of unification-based type inference [47], and more recent work uses a wide range of techniques [9, 12, 21, 34, 35, 40].”
Migrating gradual types (2017, unknown): “, 2017), and union and intersection types (Siek & Tobin-Hochstadt, 2016; Castagna & Lanvin, 2017; Toro & Tanter, 2017; Castagna et al., 2019).”
Gradual Soundness: Lessons from Static Python (2022, methodology): “The name materialization and the rule Matr* are inspired by prior work [6].”
Solver-based gradual type migration (2021, methodology): “As part of this effort, we have produced new, open-source implementations of the algorithms presented in Rastogi et al. [2012] and Campora et al.”
What is decidable about gradual types? (2019, background): “2015b], and polymorphism and set theoretic types [Castagna et al. 2019].”