Content deleted Content added
Lexi.lambda (talk | contribs) →Basic definition: Add parentheses around the types for append to make them easier to separate from the prose |
Lexi.lambda (talk | contribs) →Rank-1 (predicative) polymorphism: Update notation to match new definition section |
||
Line 40:
{{refimprove section|date=February 2019}}
In a ''[[Impredicativity|predicative]]'' type system (also known as a ''[[prenex]] polymorphic'' system), type variables may not be instantiated with polymorphic types.<ref name="TAPL">{{cite book|author1=Benjamin C. Pierce|author2=Benjamin C. (Professor Pierce, University of Pennsylvania)|title=Types and Programming Languages|url=https://books.google.com/books?id=ti6zoAC9Ph8C|year=2002|publisher=MIT Press|isbn=978-0-262-16209-8}}</ref>{{rp|pages=359–360}} Predicative type theories include [[Intuitionistic type theory|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 <math>\mathsf{append}</math> function described above, which has the following type: :<math>\mathsf{append} : \forall \alpha. [\alpha], [\alpha] \to [\alpha]</math>
In order to apply this function to a pair of lists, a concrete type <math>T</math> must be substituted for the variable
▲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 <code>append</code> can be applied to pairs of lists with elements of any type—even to lists of polymorphic functions such as <code>append</code> itself.
Polymorphism in the language ML is predicative.{{citation needed|date=February 2019}} This is because predicativity, together with other restrictions, makes the [[type system]] simple enough that full [[type inference]] is always possible.
| |||