Content deleted Content added
Lexi.lambda (talk | contribs) →Rank-1 (predicative) polymorphism: Update notation to match new definition section |
→Basic definition: I've added some brackets because it looked to me like a pair "(list,function)" rather than a function "pair -> list" |
||
Line 13:
The polymorphic definition can then be ''instantiated'' by substituting any concrete type for <math>\alpha</math>, yielding the full family of potential types.<ref>{{cite web |last1=Yorgey |first1=Brent |title=More polymorphism and type classes |url=https://www.seas.upenn.edu/~cis1940/spring13/lectures/05-type-classes.html |website=www.seas.upenn.edu |access-date=1 October 2022}}</ref>
The identity function is a particularly extreme example, but many other functions also benefit from parametric polymorphism. For example, an <math>\mathsf{append}</math> function that [[append]]s two [[linked list|lists]] does not inspect the elements of the list, only the list structure itself. Therefore, <math>\mathsf{append}</math> can be given a similar family of types, such as <math>(([\mathsf{Int}], [\mathsf{Int}]) \to [\mathsf{Int}])</math>, <math>(([\mathsf{Bool}], [\mathsf{Bool}]) \to [\mathsf{Bool}])</math>, and so on, where <math>[T]</math> denotes a list of elements of type <math>T</math>. The most general type is therefore
:<math>\mathsf{append} : \forall \alpha. ([\alpha], [\alpha]) \to [\alpha]</math>
which can be instantiated to any type in the family.
| |||