Bounded quantification

This article is about bounded quantification in type theory. For bounded quantification in mathematical logic, see Bounded quantifier.

In type theory, bounded quantification (also bounded polymorphism or constrained genericity) refers to universal or existential quantifiers which are restricted ("bounded") to range only over the subtypes of a particular type. Bounded quantification is an interaction of parametric polymorphism with subtyping. Bounded quantification has traditionally been studied in the functional setting of System F_<:, but is available in modern object-oriented languages supporting parametric polymorphism (generics) such as Java, C# and Scala.

Example

In the following Java sample the type parameter T is bounded to range only over I and its subclasses:

class I {
}

class A <T extends I> {
    public T id(T x) {
        return x;
    }
}

F-bounded quantification

F-bounded quantification or recursively bounded quantification, first explained in 1989, describes the case where subtype constraint itself is parameterized by one of the binders occurring on the left-hand side.

Here is an application of this idiom in Java for a well-typed clone method:

abstract class I<T extends I<T>> {
  public T clone(T original);
}

class A extends I<A> {
    @Override
    public A clone(A original) {
       //...
    }
}

See also

• Covariance and contravariance (computer science)
• Curiously recurring template pattern
• Wildcard (Java)

References

• Peter S. Canning, William R. Cook, Walter L. Hill, John C. Mitchell, and William Olthoff. "F-bounded quantification for object-oriented programming". In Conference on Functional Programming Languages and Computer Architecture, 1989.
• Benjamin C. Pierce "Intersection types and bounded polymorphism". Lecture Notes in Computer Science 664, 1993.
• Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler. "Making the future safe for the past: Adding genericity to the Java programming language". In Object-Oriented Programming: Systems, Languages, Applications (OOPSLA). ACM, October 1998.
• Andrew Kennedy and Don Syme. "Design and Implementation of Generics for the .NET Common Language Runtime". In Programming Language Design and Implementation, 2001.
• , Chapter 26: Bounded quantification

External links

• Bounded Polymorphism at the Portland Pattern Repository
• "F-bounded Polymorphism" in The Cecil Language: Specification and Rationale
• WTF is F-Bounded Polymorphism
• The Java Program: OrderedList.java