Gradual Typing: A New Perspective

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 three gradual type systems - Hindley-Milner, with subtyping, and with union and intersection types- in terms of two preorders, subtyping and materialization. These systems are defined both declaratively and algorithmically. The declarative presentation consists in adding two subsumption-like rules, one for each preorder, to the standard rules of each type system. This yields more intelligible and streamlined definitions and shows a direct correlation between cast insertion and materialization. For the algorithmic presentation, we show how it can be defined by reusing existing techniques such as unification and tallying.