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 |
Thu 17 JanDisplayed time zone: Belfast change
10:36 - 12:04 | |||
10:36 22mTalk | Type-Driven Gradual Security with ReferencesTOPLAS Research Papers Matías Toro University of Chile, Ronald Garcia University of British Columbia, Éric Tanter University of Chile & Inria Paris DOI Media Attached File Attached | ||
10:58 22mTalk | Gradual Type Theory Research Papers Max S. New Northeastern University, Daniel R. Licata Wesleyan University, Amal Ahmed Northeastern University, USA Link to publication DOI Media Attached File Attached | ||
11:20 22mTalk | Gradual Parametricity, RevisitedDistinguished Paper Research Papers Matías Toro University of Chile, Elizabeth Labrada University of Chile, Éric Tanter University of Chile & Inria Paris Link to publication DOI Pre-print Media Attached File Attached | ||
11:42 22mTalk | Live Functional Programming with Typed Holes Research Papers Cyrus Omar University of Chicago, Ian Voysey Carnegie Mellon University, Ravi Chugh University of Chicago, Matthew Hammer None Link to publication DOI Pre-print Media Attached File Attached |