Institute for Software Research Talk
- Gates Hillman Centers
- ÉRIC TANTER
- Computer Science Department
- University of Chile
Gradual Parametricity, Revisited
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.
Joint work with Matías Toro and Elizabeth Labrada, published at POPL’19.
Éric Tanter is a Full Professor in the Computer Science Department of the University of Chile, currently a Visiting Researcher in the Prosecco team at Inria Paris. He received his PhD from both the University of Nantes and the University of Chile in 2004. His research interests cover programming languages and software engineering, ranging from the theoretical underpinnings of programming languages to the empirical study of the practice of programming. He has published many articles in, and is regularly involved in the program committees and editorial boards of, major conferences and journals in these areas. Recently, he has been mostly involved in the foundations and practice of gradual typing and verification.
Faculty Host: Jonathan Aldrich