Gradual Parametricity, Revisited

International audienceBringing the benefits of gradual typing to a language with parametric polymorphism like System F, whilepreserving relational parametricity, has proven extremely challenging: first attempts were formulated a decadeago, and several recent developments have been published in the past year. In addition to leaving someproperties as conjectures or future work, we observe that all prior work improperly handle type instantiationswhen imprecise types are involved. This observation further suggests that existing polymorphic cast calculiare not well suited for supporting a gradual counterpart of System F. Consequently, we revisit the challengeof designing a gradual language with explicit parametric polymorphism, exploring the extent to which theAbstracting Gradual Typing methodology helps us derive such a language, GSF. We present the design andmetatheory of GSF, and provide a reference implementation. In addition to avoiding the uncovered semanticissues, 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 simplyincompatible with parametricity. We nevertheless establish a weaker property that allows us to disprove severalclaims about gradual free theorems, clarifying the kind of reasoning supported by gradual parametricit