# Bounded quantification

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Bounded_quantification
> Markdown URL: https://mediated.wiki/source/Bounded_quantification.md
> Source: https://en.wikipedia.org/wiki/Bounded_quantification
> Source revision: 1346157724
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

{{About|bounded quantification in type theory|bounded quantification in mathematical logic|Bounded quantifier}}

In [type theory](/source/type_theory), '''bounded quantification''' (also '''bounded polymorphism''' or '''constrained genericity''') refers to [universal](/source/universally_quantified) or [existential quantifier](/source/existential_type)s which are restricted ("bounded") to range only over the subtypes of a particular type. Bounded quantification is an interaction of [parametric polymorphism](/source/parametric_polymorphism) with [subtyping](/source/subtyping). Bounded quantification has traditionally been studied in the [functional](/source/functional_programming) setting of [System F<sub><:</sub>](/source/System_F-sub), but is available in modern [object-oriented language](/source/object-oriented_language)s supporting [parametric polymorphism](/source/parametric_polymorphism) ([generics](/source/Generic_programming)) such as [Java](/source/Java_(programming_language)), [C#](/source/C_Sharp_(programming_language)) and [Scala](/source/Scala_(programming_language)).

== Overview ==
The purpose of bounded quantification is to allow for [polymorphic function](/source/polymorphic_function)s to depend on some specific behaviour of objects instead of [type inheritance](/source/type_inheritance). It assumes a record-based model for object classes, where every class member is a record element and all class members are named functions. Object attributes are represented as functions that take no argument and return an object. The specific behaviour is then some function name along with the types of the arguments and the return type. Bounded quantification considers all objects with such a function. An example would be a polymorphic <code>min</code> function that considers all objects that are comparable to each other.{{cn|date=November 2022}}

=== F-bounded quantification ===
'''''F''-bounded quantification''' or '''recursively bounded quantification''', introduced in 1989, allows for more precise typing of functions that are applied on recursive types. A recursive type is one that features as a constructor a function that uses it as a type for some argument, or the return value of a functional argument, or some argument of the functional return value of a functional argument, or so on: that is, in positive position.<ref>''F''-bounded polymorphism for object-oriented programming. Canning, [Cook](/source/William_Cook_(computer_scientist)), Hill, Olthof and [Mitchell](/source/John_C._Mitchell). http://dl.acm.org/citation.cfm?id=99392</ref>

== Example ==
This kind of type constraint can be expressed in [Java](/source/Java_(programming_language)) with a generic interface. The following example demonstrates how to describe types that can be compared to each other and use this as typing information in [polymorphic function](/source/polymorphic_function)s. The <code>Test::min</code> function uses simple bounded quantification and does not ensure the objects are mutually comparable, in contrast with the <code>Test::fMin</code> function which uses F-bounded quantification.

In mathematical notation, the types of the two functions are

* <math>\texttt{min}: \forall T, \forall S \subseteq \{\texttt{compareTo}: T \to \texttt{int}\}, S \to S \to S</math>
* <math>\texttt{fmin}: \forall T \subseteq \texttt{Comparable<}T\texttt{>}, T \to T \to T</math>
where
<math>
\texttt{Comparable<}T\texttt{>} = \{\texttt{compareTo}: T \to \texttt{int}\}
</math>

Consider the following possible declarations in <code>java.lang</code>:
<syntaxhighlight lang="java">
package java.lang;

public interface Comparable<T> {
    int compareTo(T other);
}

public class Integer implements Comparable<Integer> {
    @Override
    public int compareTo(Integer other) {
        // ...
    }
}

public class String implements Comparable<String> {
    @Override
    public int compareTo(String other) {
        // ...
    }
}
</syntaxhighlight>

Then, in use:
<syntaxhighlight lang="java">
package org.wikipedia.examples;

public class Test {
    public static <S extends Comparable> S min(S a, S b) {
        if (a.compareTo(b) <= 0) {
            return a;
        } else {
            return b;
        }
    }

    public static <T extends Comparable<T>> T fMin(T a, T b) {
        if (a.compareTo(b) <= 0) {
            return a;
        } else {
            return b;
        }
    }

    public static void main(String[] args) {
        String a = min("cat", "dog");
        Integer b = min(10, 3);
        Comparable c = min("cat", 3); // Throws ClassCastException at runtime
        String str = fMin("cat", "dog");
        Integer i = fMin(10, 3);
        // Object o = fMin("cat", 3); // Does not compile
    }
}
</syntaxhighlight>

== See also ==
* [Covariance and contravariance (computer science)](/source/Covariance_and_contravariance_(computer_science))
* [Curiously recurring template pattern](/source/Curiously_recurring_template_pattern)
* [Wildcard (Java)](/source/Wildcard_(Java))

== Notes ==
{{Reflist}}

== References ==
* {{cite journal|last1 = Cardelli|first1=Luca|authorlink1=Luca Cardelli|last2=Wegner|first2=Peter|authorlink2=Peter Wegner (computer scientist)|title = On Understanding Types, Data Abstraction, and Polymorphism|url=http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf|journal = [ACM Computing Surveys](/source/ACM_Computing_Surveys)|date = December 1985| volume = 17|issue=4|issn = 0360-0300|pages = 471&ndash;523|doi = 10.1145/6041.6042|citeseerx=10.1.1.117.695|s2cid=2921816 }}
* [Peter S. Canning](/source/Peter_S._Canning), [William R. Cook](/source/William_Cook_(computer_scientist)), [Walter L. Hill](/source/Walter_L._Hill), [John C. Mitchell](/source/John_C._Mitchell), and [William Olthoff](/source/William_Olthoff). [http://dl.acm.org/citation.cfm?id=99392 "F-bounded polymorphism for object-oriented programming"]. In ''Conference on Functional Programming Languages and Computer Architecture'', 1989.
* [Benjamin C. Pierce](/source/Benjamin_C._Pierce) "Intersection types and bounded polymorphism". ''Lecture Notes in Computer Science'' '''664''', 1993.
* [Gilad Bracha](/source/Gilad_Bracha), [Martin Odersky](/source/Martin_Odersky), [David Stoutamire](/source/David_Stoutamire), and [Philip Wadler](/source/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](/source/Andrew_Kennedy_(computer_scientist)) and [Don Syme](/source/Don_Syme). "Design and Implementation of Generics for the .NET Common Language Runtime". In ''Programming Language Design and Implementation'', 2001.
* {{cite book|last=Pierce|first=Benjamin C.|authorlink=Benjamin C. Pierce|title=Types and Programming Languages|publisher=MIT Press|date=2002|isbn=978-0-262-16209-8}}, Chapter 26: Bounded quantification

== External links ==
* [http://www.c2.com/cgi/wiki?BoundedPolymorphism Bounded Polymorphism] at the [Portland Pattern Repository](/source/Portland_Pattern_Repository)
* [http://www.cs.washington.edu/research/projects/cecil/www/Vortex-Three-Zero/doc-cecil-lang/cecil-spec-86.html "F-bounded Polymorphism"] in ''The Cecil Language: Specification and Rationale''

Category:Polymorphism (computer science)
Category:Object-oriented programming
Category:Type theory
Category:Articles with example Java code

---
Adapted from the Wikipedia article [Bounded quantification](https://en.wikipedia.org/wiki/Bounded_quantification) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Bounded_quantification?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.