On polymorphic gradual typing

Abstract

We study an extension of gradual typingÐa method to integrate dynamic typing and static typing smoothly in a single languageÐto parametric polymorphism and its theoretical properties, including conservativity of typing and semantics over both statically and dynamically typed languages, type safety, blame-subtyping theorem, and the gradual guaranteeÐthe so-called refined criteria, advocated by Siek et al. We develop System FG, which is a gradually typed extension of System F with the dynamic type and a new type consistency relation, and translation to a new polymorphic blame calculus System FC, which is based on previous polymorphic blame calculi by Ahmed et al. The design of System FG and System FC, geared to the criteria, is influenced by the distinction between static and gradual type variables, first observed by Garcia and Cimini. This distinction is also useful to execute statically typed code without incurring additional overhead to manage type names as in the prior calculi. We prove that System FG satisfies most of the criteria: all but the hardest property of the gradual guarantee on semantics. We show that a key conjecture to prove the gradual guarantee leads to the Jack-of-All-Trades property, conjectured as an important property of the polymorphic blame calculus by Ahmed et al.