Gradual Parametricity, Revisited
Résumé
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. In addition to leaving some
properties as conjectures or future work, we observe that all prior work improperly handle type instantiations
when imprecise types are involved. This observation further suggests 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, and provide a reference implementation. 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