Parametric polymorphism

(Redirected from Impredicative 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.[1]: 340  Parametrically polymorphic functions and data types are sometimes called generic functions and generic datatypes, respectively, and they form the basis of generic programming.

Parametric polymorphism may be contrasted with ad hoc polymorphism. Parametrically polymorphic definitions are uniform: they behave identically regardless of the type they are instantiated at.[1]: 340 [2]: 37  In contrast, ad hoc polymorphic definitions are given a distinct definition for each type. 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.

Basic definition

edit

It is possible to write functions that do not depend on the types of their arguments. For example, the identity function   simply returns its argument unmodified. This naturally gives rise to a family of potential types, such as  ,  ,  , and so on. Parametric polymorphism allows   to be given a single, most general type by introducing a universally quantified type variable:

 

The polymorphic definition can then be instantiated by substituting any concrete type for  , yielding the full family of potential types.[3]

The identity function is a particularly extreme example, but many other functions also benefit from parametric polymorphism. For example, an   function that concatenates two lists does not inspect the elements of the list, only the list structure itself. Therefore,   can be given a similar family of types, such as  ,  , and so on, where   denotes a list of elements of type  . The most general type is therefore

 

which can be instantiated to any type in the family.

Parametrically polymorphic functions like   and   are said to be parameterized over an arbitrary type  .[4] Both   and   are parameterized over a single type, but functions may be parameterized over arbitrarily many types. For example, the   and   functions that return the first and second elements of a pair, respectively, can be given the following types:

 

In the expression  ,   is instantiated to   and   is instantiated to   in the call to  , so the type of the overall expression is  .

The syntax used to introduce parametric polymorphism varies significantly between programming languages. For example, in some programming languages, such as Haskell, the   quantifier is implicit and may be omitted.[5] Other languages require types to be instantiated explicitly at some or all of a parametrically polymorphic function's call sites.

History

edit

Parametric polymorphism was first introduced to programming languages in ML in 1975.[6] Today it exists in Standard ML, OCaml, F#, Ada, Haskell, Mercury, Visual Prolog, Scala, Julia, Python, TypeScript, C++ and others. Java, C#, Visual Basic .NET and Delphi have each introduced "generics" for parametric polymorphism. Some implementations of type polymorphism are superficially similar to parametric polymorphism while also introducing ad hoc aspects. One example is C++ template specialization.

Predicativity, impredicativity, and higher-rank polymorphism

edit

Rank-1 (predicative) polymorphism

edit

In a predicative type system (also known as a prenex polymorphic system), type variables may not be instantiated with polymorphic types.[1]: 359–360  Predicative type theories include Martin-Löf type theory and Nuprl. This is very similar to what is called "ML-style" or "Let-polymorphism" (technically ML's Let-polymorphism has a few other syntactic restrictions). This restriction makes the distinction between polymorphic and non-polymorphic types very important; thus in predicative systems polymorphic types are sometimes referred to as type schemas to distinguish them from ordinary (monomorphic) types, which are sometimes called monotypes.

A consequence of predicativity is that all types can be written in a form that places all quantifiers at the outermost (prenex) position. For example, consider the   function described above, which has the following type:

 

In order to apply this function to a pair of lists, a concrete type   must be substituted for the variable   such that the resulting function type is consistent with the types of the arguments. In an impredicative system,   may be any type whatsoever, including a type that is itself polymorphic; thus   can be applied to pairs of lists with elements of any type—even to lists of polymorphic functions such as   itself. Polymorphism in the language ML is predicative.[citation needed] This is because predicativity, together with other restrictions, makes the type system simple enough that full type inference is always possible.

As a practical example, OCaml (a descendant or dialect of ML) performs type inference and supports impredicative polymorphism, but in some cases when impredicative polymorphism is used, the system's type inference is incomplete unless some explicit type annotations are provided by the programmer.

Higher-rank polymorphism

edit

Some type systems support an impredicative function type constructor even though other type constructors remain predicative. For example, the type   is permitted in a system that supports higher-rank polymorphism, even though   may not be.[7]

A type is said to be of rank k (for some fixed integer k) if no path from its root to a   quantifier passes to the left of k or more arrows, when the type is drawn as a tree.[1]: 359  A type system is said to support rank-k polymorphism if it admits types with rank less than or equal to k. For example, a type system that supports rank-2 polymorphism would allow   but not  . A type system that admits types of arbitrary rank is said to be "rank-n polymorphic".

Type inference for rank-2 polymorphism is decidable, but for rank-3 and above, it is not.[8][1]: 359 

Impredicative polymorphism

edit

Impredicative polymorphism (also called first-class polymorphism) is the most powerful form of parametric polymorphism.[1]: 340  In formal logic, a definition is said to be impredicative if it is self-referential; in type theory, it refers to the ability for a type to be in the domain of a quantifier it contains. This allows the instantiation of any type variable with any type, including polymorphic types. An example of a system supporting full impredicativity is System F, which allows instantiating   at any type, including itself.

In type theory, the most frequently studied impredicative typed λ-calculi are based on those of the lambda cube, especially System F.

Bounded parametric polymorphism

edit

In 1985, Luca Cardelli and Peter Wegner recognized the advantages of allowing bounds on the type parameters.[9] Many operations require some knowledge of the data types, but can otherwise work parametrically. For example, to check whether an item is included in a list, we need to compare the items for equality. In Standard ML, type parameters of the form ’’a are restricted so that the equality operation is available, thus the function would have the type ’’a × ’’a list → bool and ’’a can only be a type with defined equality. In Haskell, bounding is achieved by requiring types to belong to a type class; thus the same function has the type   in Haskell. In most object-oriented programming languages that support parametric polymorphism, parameters can be constrained to be subtypes of a given type (see the articles Subtype polymorphism and Generic programming).

See also

edit

Notes

edit
  1. ^ a b c d e f Benjamin C. Pierce (2002). Types and Programming Languages. MIT Press. ISBN 978-0-262-16209-8.
  2. ^ Strachey, Christopher (1967), Fundamental Concepts in Programming Languages (Lecture notes), Copenhagen: International Summer School in Computer Programming. Republished in: Strachey, Christopher (1 April 2000). "Fundamental Concepts in Programming Languages". Higher-Order and Symbolic Computation. 13 (1): 11–49. doi:10.1023/A:1010000313106. ISSN 1573-0557. S2CID 14124601.
  3. ^ Yorgey, Brent. "More polymorphism and type classes". www.seas.upenn.edu. Retrieved 1 October 2022.
  4. ^ Wu, Brandon. "Parametric Polymorphism - SML Help". smlhelp.github.io. Retrieved 1 October 2022.
  5. ^ "Haskell 2010 Language Report § 4.1.2 Syntax of Types". www.haskell.org. Retrieved 1 October 2022. With one exception (that of the distinguished type variable in a class declaration (Section 4.3.1)), the type variables in a Haskell type expression are all assumed to be universally quantified; there is no explicit syntax for universal quantification.
  6. ^ 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)
  7. ^ Kwang Yul Seo. "Kwang's Haskell Blog - Higher rank polymorphism". kseo.github.io. Retrieved 30 September 2022.
  8. ^ Kfoury, A. J.; Wells, J. B. (1 January 1999). "Principality and decidable type inference for finite-rank intersection types". Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Association for Computing Machinery. pp. 161–174. doi:10.1145/292540.292556. ISBN 1581130953. S2CID 14183560.
  9. ^ Cardelli & Wegner 1985.

References

edit