We define a new, more semantic interpretation of gradual types and use it to “gradualize” two forms of polymorphism: subtyping polymorphism and implicit parametric polymorphism.

In particular, we use the new interpretation to define two preorders on types, subtyping and materialization, and we employ these preorders to define three gradual type systems —Hindley-Milner, with subtyping, and with union and intersection types— which we present in two different forms: declaratively and algorithmically.

The declarative presentation consists in adding two subsumption-like rules, one for each preorder, to the existing standard rules of the type system. This yields clearer, more intelligible, and streamlined definitions; it also shows a direct correlation between cast insertion and materialization that suggests a logical interpretation of the cast calculus, an essential component of gradual typing systems. For the algorithmic presentation, we show how it can be defined by using already existing constraint solving algorithms simply by adding some pre-/post-processing steps. We relate corresponding declarative and algorithmic presentations by soundness and completeness results.

As customary, the semantics of the various gradually-typed languages is given in terms of a compilation into cast calculi that use blame labels to pinpoint cast failures. To that end, we show how to define the operational semantics for casts in the presence of unions and intersections, which is an important and far-from-obvious result. We also show a direct correlation between the safety of a cast and the “polarity” of its blame label, allowing for a simpler formulation of the so-called blame safety property.