Graduality and Parametricity: Together Again for the First Time
Parametric polymorphism and gradual typing have proven to be a difficult combination, with no language yet produced that satisfies the fundamental theorems of each: parametricity and graduality. Notably, Toro, Labrada, and Tanter (POPL 2019) conjecture that for any gradual extension of System F that uses dynamic type generation, graduality and parametricity are “simply incompatible”. However, we argue that it is not graduality and parametricity that are incompatible per se, but instead that combining the syntax of System F with dynamic type generation as in previous work necessitates type-directed computation, which we show has been a common source of graduality and parametricity violations in previous work.
We then show that by modifying the syntax of universal and existential types to make the type name generation explicit, we remove the need for type-directed computation, and get a language that satisfies both graduality and parametricity theorems. The language has a simple runtime semantics, which can be explained by translation to a statically typed language where the dynamic type is interpreted as a dynamically extensible sum type. Far from being in conflict, we show that the parametricity theorem follows as a direct corollary of a relational interpretation of the graduality property.
Wed 22 JanDisplayed time zone: Saskatchewan, Central America change
14:00 - 15:05
|What is Decidable about Gradual Types?|
Zeina Migeed University of California, Los Angeles, Jens Palsberg University of California, Los AngelesLink to publication DOI Media Attached File Attached
|Graduality and Parametricity: Together Again for the First Time|
Max New Northeastern University, Dustin Jamner Northeastern University, USA, Amal Ahmed Northeastern University, USALink to publication DOI Media Attached
|Does Blame Shifting Work?|
Lukas Lazarek Northwestern University, Alexis King Northwestern University, Samanvitha Sundar Northwestern University, Robby Findler Northwestern University, USA, Christos Dimoulas PLT @ Northwestern UniversityLink to publication DOI Media Attached