In programming languages and type theory, parametric polymorphism is a way to make a language more expressive, while still maintaining full static type-safety. Using parametric polymorphism, a function or a data type can be written generically so that it can handle values identically without depending on their type.[1] Such functions and data types are called generic functions and generic datatypes respectively and form the basis of generic programming. For example, a function append that joins two lists can be constructed so that it does not care about the type of elements: it can append lists of integers, lists of real numbers, lists of strings, and so on. Let the type variable a denote the type of elements in the lists. Then append can be typed forall a. [a] × [a] -> [a] where [a] denotes the type of lists with elements of type a. We say that the type of append is parameterized by a for all values of a. (Note that since there is only one type variable, the function cannot be applied to just any pair of lists: the pair, as well as the result list, must consist of the same type of elements.) For each place where append is applied, a value is decided for a. Following Christopher Strachey,[2] parametric polymorphism may be contrasted with ad hoc polymorphism, in which a single polymorphic function can have a number of distinct and potentially heterogeneous implementations depending on the type of argument(s) to which it is applied. Thus, ad hoc polymorphism can generally only support a limited number of such distinct types, since a separate implementation has to be provided for each type. Contents 1 History 2 Higher-ranked polymorphism 2.1 Rank-1 (prenex) polymorphism 2.2 Rank-k polymorphism 2.3 Rank-n ("higher-rank") polymorphism 3 Predicativity and impredicativity 3.1 Predicative polymorphism
3.2
4 Bounded parametric polymorphism 5 See also 6 Notes 7 References History[edit]
forall a. [a] × [a] -> [a] In order to apply this function to a pair of lists, a type must be substituted for the variable a in the type of the function such that the type of the arguments matches up with the resulting function type. In an impredicative system, the type being substituted may be any type whatsoever, including a type that is itself polymorphic; thus append can be applied to pairs of lists with elements of any type—even to lists of polymorphic functions such as append itself. Polymorphism in the language ML and its close relatives is predicative. This is because predicativity, together with other restrictions, makes the type system simple enough that type inference is possible. In languages where explicit type annotations are necessary when applying a polymorphic function, the predicativity restriction is less important; thus these languages are generally impredicative. Rank-k polymorphism[edit] This section needs expansion. You can help by adding to it. (November 2013) For some fixed value k, rank-k polymorphism is a system in which a
quantifier may not appear to the left of k or more arrows (when the
type is drawn as a tree).[1]
This section needs expansion. You can help by adding to it. (November 2013) Rank-n polymorphism is polymorphism in which quantifiers may appear to the left of arbitrarily many arrows. Predicativity and impredicativity[edit] Predicative polymorphism[edit] In a predicative parametric polymorphic system, a type τ displaystyle tau containing a type variable α displaystyle alpha may not be used in such a way that α displaystyle alpha is instantiated to a polymorphic type. Predicative type theories
include Martin-Löf Type Theory and NuPRL.
τ displaystyle tau with any type, including polymorphic types, such as τ displaystyle tau itself. An example of this is the
T = ∀ X . X → X displaystyle T=forall X.Xto X , where X could even refer to T itself.
In type theory, the most frequently studied impredicative typed
λ-calculi are based on those of the lambda cube, especially System
F.[1]
Bounded parametric polymorphism[edit]
Main article: Bounded quantification
In 1985,
E q α ⇒ α → [ α ] → B o o l displaystyle scriptstyle Eq,alpha ,Rightarrow alpha ,rightarrow left[alpha right]rightarrow Bool in Haskell. In most object-oriented programming languages that
support parametric polymorphism, parameters can be constrained to be
subtypes of a given type (see
Polymorphic recursion Type class#Higher-kinded polymorphism Notes[edit] ^ a b c Pierce 2002. ^ Strachey 1967. ^ Milner, R., Morris, L., Newey, M. "A Logic for Computable Functions with reflexive and polymorphic types", Proc. Conference on Proving and Improving Programs, Arc-et-Senans (1975) ^ Pierce 2002, p. 359. ^ Pierce 2002, p. 340. ^ Cardelli & Wegner 1985. References[edit] Strachey, Christopher (1967), Fundamental Concepts in Programming Languages (Lecture notes), Copenhagen: International Summer School in Computer Programming . Republished in: Higher-Order and Symbolic Computation. 13: 11–49. 2000. doi:10.1023/A:1010000313106. Missing or empty title= (help) Hindley, J. Roger (1969), "The principal type scheme of an object in combinatory logic", Transactions of the American Mathematical Society, American Mathematical Society, 146: 29–60, doi:10.2307/1995158, JSTOR 1995158, MR 0253905 . Girard, Jean-Yves (1971). "Une Extension de l'Interpretation de Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types". Proceedings of the Second Scandinavian Logic Symposium (in French). Amsterdam. pp. 63–92. doi:10.1016/S0049-237X(08)70843-7. Girard, Jean-Yves (1972), Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur (Ph.D. thesis) (in French), Université Paris 7 . Reynolds, John C. (1974), "Towards a Theory of Type Structure", Colloque sur la programmation, Lecture Notes in Computer Science, Paris, 19: 408–425, doi:10.1007/3-540-06859-7_148 . Milner, Robin (1978). "A Theory of Type Polymorphism in Programming". Journal of Computer and System Sciences. 17 (3): 348—375. doi:10.1016/0022-0000(78)90014-4. Cardelli, Luca; Wegner, Peter (December 1985). "On Understanding Types, Data Abstraction, and Polymorphism" (PDF). ACM Computing Surveys. New York, NY, USA: ACM. 17 (4): 471–523. doi:10.1145/6041.6042. ISSN 0360-0300. Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press. ISBN 978-0-262-16209-8. v t e Data types Uninterpreted Bit
Byte
Trit
Tryte
Word
Numeric Arbitrary-precision or bignum Complex Decimal Fixed point Floating point Double precision Extended precision Half precision Long double Minifloat Octuple precision Quadruple precision Single precision Integer signedness Interval Rational Pointer Address physical virtual Reference Text Character String null-terminated Composite Algebraic data type generalized Array Associative array Class Dependent Equality Inductive List Object metaobject Option type Product Record Set Union tagged Other Boolean Bottom type Collection Enumerated type Exception Function type Opaque data type Recursive data type Semaphore Stream Top type Type class Unit type Void Related topics Abstract data type Data structure Generic Kind metaclass Parametric polymorphism Primitive data type Protocol interface Subtyping Type constructor Type conversion Type system Type theory See also platform-dependent and independent un |