Jump to content

Polymorphic recursion

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Ruud Koot (talk | contribs) at 15:43, 8 May 2012 (Example: === Higher-ranked types === {{see also|Higher-ranked type}} {{expand section}}). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

In computer science, polymorphic recursion (also referred to as Milner–Mycroft typability or the Milner–Mycroft calculus) refers to a recursive parametrically polymorph function where the type parameter changes with each recursive invocation made instead of staying constant. Type inference for polymorphic recursion is equivalent to semi-unification and thefore undecidable and requires the use of a semi-algorithm or programmer supplied type annotations.[1]

Example

Nested datatypes

Consider the following nested datatype:

data Nested a = a :<: (Nested [a]) | Epsilon
infixr 5 :<:

nested = 1 :<: [2,3,4] :<: [[4,5],[7],[8,9]] :<: Epsilon

A length function defined over this datatype will be polymorphically recursive, as the type of the argument changes from Nested a to Nested [a] in the recursive call:

length :: Nested a -> Int
length Epsilon    = 0
length (_ :<: xs) = 1 + length xs

In Haskell, unlike for most other functions definitions, the type signature cannot be omitted.

Higher-ranked types

See also

Notes

Further reading