Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Thu 17 Jan 2019 11:20 - 11:42 at Sala I - Gradual Types Chair(s): Nikhil Swamy

Bringing the benefits of gradual typing to a language with parametric polymorphism like System F, while preserving relational parametricity, has proven extremely challenging: first attempts were formulated a decade ago, and several recent developments have been published in the past year. Among other issues, these proposals can however signal parametricity errors in unexpected situations, and improperly handle type instantiations when imprecise types are involved. These observations further suggest that existing polymorphic cast calculi are not well suited for supporting a gradual counterpart of System F. Consequently, we revisit the challenge of designing a gradual language with explicit parametric polymorphism, exploring the extent to which the Abstracting Gradual Typing methodology helps us derive such a language, GSF. We present the design and metatheory of GSF. In addition to avoiding the uncovered semantic issues, GSF satisfies all the expected properties of a gradual parametric language, save for one property: the dynamic gradual guarantee, which was left as conjecture in all prior work, is here proven to be simply incompatible with parametricity. We nevertheless establish a weaker property that allows us to disprove several claims about gradual free theorems, clarifying the kind of reasoning supported by gradual parametricity.

slides (gsf-popl2019.pdf)8.17MiB

Conference Day
Thu 17 Jan

Displayed time zone: Belfast change

10:36 - 12:04
Gradual TypesResearch Papers at Sala I
Chair(s): Nikhil SwamyMicrosoft Research
10:36
22m
Talk
Type-Driven Gradual Security with ReferencesTOPLAS
Research Papers
Matías ToroUniversity of Chile, Ronald GarciaUniversity of British Columbia, Éric TanterUniversity of Chile & Inria Paris
DOI Media Attached File Attached
10:58
22m
Talk
Gradual Type Theory
Research Papers
Max NewNortheastern University, Dan LicataWesleyan University, Amal AhmedNortheastern University, USA
Link to publication DOI Media Attached File Attached
11:20
22m
Talk
Gradual Parametricity, RevisitedDistinguished Paper
Research Papers
Matías ToroUniversity of Chile, Elizabeth LabradaUniversity of Chile, Éric TanterUniversity of Chile & Inria Paris
Link to publication DOI Pre-print Media Attached File Attached
11:42
22m
Talk
Live Functional Programming with Typed Holes
Research Papers
Cyrus OmarUniversity of Chicago, Ian VoyseyCarnegie Mellon University, Ravi ChughUniversity of Chicago, Matthew HammerNone
Link to publication DOI Pre-print Media Attached File Attached