## 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