HOME

TheInfoList



OR:

In
type theory In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a fou ...
, bounded quantification (also bounded polymorphism or constrained genericity) refers to
universal Universal is the adjective for universe. Universal may also refer to: Companies * NBCUniversal, a media and entertainment company ** Universal Animation Studios, an American Animation studio, and a subsidiary of NBCUniversal ** Universal TV, a ...
or
existential quantifier In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some". It is usually denoted by the logical operator symbol ∃, which, w ...
s which are restricted ("bounded") to range only over the subtypes of a particular type. Bounded quantification is an interaction of
parametric polymorphism In programming languages and type theory, parametric polymorphism allows a single piece of code to be given a "generic" type, using variables in place of actual types, and then instantiated with particular types as needed. Parametrically polymorph ...
with
subtyping In programming language theory, subtyping (also subtype polymorphism or inclusion polymorphism) is a form of type polymorphism in which a subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutability, ...
. Bounded quantification has traditionally been studied in the functional setting of System F<:, but is available in modern
object-oriented language Object-oriented programming (OOP) is a programming paradigm based on the concept of "objects", which can contain data and code. The data is in the form of fields (often known as attributes or ''properties''), and the code is in the form of ...
s supporting
parametric polymorphism In programming languages and type theory, parametric polymorphism allows a single piece of code to be given a "generic" type, using variables in place of actual types, and then instantiated with particular types as needed. Parametrically polymorph ...
( generics) such as
Java Java (; id, Jawa, ; jv, ꦗꦮ; su, ) is one of the Greater Sunda Islands in Indonesia. It is bordered by the Indian Ocean to the south and the Java Sea to the north. With a population of 151.6 million people, Java is the world's mos ...
, C# and Scala.


Overview

The purpose of bounded quantification is to allow for polymorphic functions to depend on some specific behaviour of objects instead of 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 allows to considers all objects with such a function. An example would be a polymorphic min function that considers all objects that are comparable to each other.


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 includes a function that uses it as a type for some argument or its return value.''F''-bounded polymorphism for object-oriented programming. Canning,
Cook Cook or The Cook may refer to: Food preparation * Cooking, the preparation of food * Cook (domestic worker), a household staff member who prepares food * Cook (professional), an individual who prepares food for consumption in the food industry * ...
, Hill, Olthof and Mitchell. http://dl.acm.org/citation.cfm?id=99392


Example

This kind of type constraint can be expressed in
Java Java (; id, Jawa, ; jv, ꦗꦮ; su, ) is one of the Greater Sunda Islands in Indonesia. It is bordered by the Indian Ocean to the south and the Java Sea to the north. With a population of 151.6 million people, Java is the world's mos ...
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 functions. The Test.min function uses simple bounded quantification and does not preserve the type of the assigned types, in contrast with the Test.Fmin function which uses F-bounded quantification. In mathematical notation, the types of the two functions are :min: ∀ T, ∀ S ⊆ . S → S → S :Fmin: ∀ T ⊆ Comparable T → T → T where :Comparable = interface Comparable class Integer implements Comparable class String implements Comparable class Test


See also

*
Covariance and contravariance (computer science) Many programming language type systems support subtyping. For instance, if the type is a subtype of , then an expression of type should be substitutable wherever an expression of type is used. Variance refers to how subtyping between more comp ...
*
Curiously recurring template pattern The curiously recurring template pattern (CRTP) is an idiom, originally in C++, in which a class X derives from a class template instantiation using X itself as a template argument. More generally it is known as F-bound polymorphism, and it is a ...
* Wildcard (Java)


Notes


References

* * Peter S. Canning, William R. Cook, Walter L. Hill, John C. Mitchell, and
William Olthoff William is a male given name of Germanic origin.Hanks, Hardcastle and Hodges, ''Oxford Dictionary of First Names'', Oxford University Press, 2nd edition, , p. 276. It became very popular in the English language after the Norman conquest of Eng ...

"F-bounded polymorphism 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 Gilad Bracha is a software engineer at F5 Networks, and formerly at Google, where he was on the Dart programming language team. He is creator of the Newspeak language, and co-author of the second and third editions of the Java Language Specificati ...
,
Martin Odersky Martin Odersky (born 5 September 1958) is a German computer scientist and professor of programming methods at École Polytechnique Fédérale de Lausanne (EPFL) in Switzerland. He specializes in code analysis and programming languages. He designe ...
, David Stoutamire, and
Philip Wadler Philip Lee Wadler (born April 8, 1956) is an American computer scientist known for his contributions to programming language design and type theory. He is the chair of Theoretical Computer Science at the Laboratory for Foundations of Computer ...
. "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. * {{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


Bounded Polymorphism
at the
Portland Pattern Repository The Portland Pattern Repository (PPR) is a repository for computer programming software design patterns. It was accompanied by a companion website, WikiWikiWeb, which was the world's first wiki. The repository has an emphasis on Extreme Programmin ...

"F-bounded Polymorphism"
in ''The Cecil Language: Specification and Rationale'' Polymorphism (computer science) Object-oriented programming Type theory Articles with example Java code