Bounded quantification

From Wikipedia, the free encyclopedia
Jump to: navigation, search
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.


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[edit]

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. [1]

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> {
    public A clone(A original) {

See also[edit]


External links[edit]


  1. ^ F-bounded polymorphism for object-oriented programming. Canning, Cook, Hill, Olthof and Mitchell.