Programming with intersection types and bounded polymorphism
Benjamin C. Pierce · 1992
Intersection types and bounded quantification are complementary mechanisms for extending the expressive power of statically typed programming languages. They begin with a common framework: a simple, typed language with higher-order functions and a notion of subtyping. Intersection types extend this framework by giving every pair of types oe and ø a greatest lower bound, oeø , corresponding intuitively to the intersection of the sets of values described by oe and ø . Bounded quantification extends the basic framework along a different axis by adding polymorphic functions that operate uniformly on all the subtypes of a given type. This thesis unifies and extends prior work on intersection types and bounded quantification, previously studied only in isolation, by investigating theoretical and practical aspects of a typed -calculus incorporating both. The practical utility of this calculus, called F , is established by examples showing, for instance, that it allows a rich form of "cohere...