Intersection Types and Bounded Polymorphism

Benjamin C Pierce

Abstract: 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 omega and rho a greatest lower bound, omega And rho, corresponding intuitively to the intersection of the sets of values described by omega and rho. 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. We describe a new type system incorporating both, illustrate some of its properties, and present a typechecking algorithm.

LFCS report ECS-LFCS-92-200

A revised version will appear in Mathematical Structures in Computer Science, 1995. A summary version appeared in the proceedings on the conference on Typed Lambda Calculi and Applications, March 1993, pp. 346--360.

Previous | Index | Next