Polymorphic recursion
In computer science, polymorphic recursion 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
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.
Notes
Further reading
- Henglein, Fritz (1993). "Type inference with polymorphic recursion". ACM Transactions on Programming Languages and Systems. 15 (2). doi:10.1145/169701.169692.
{{cite journal}}: Invalid|ref=harv(help) - Mycroft, Alan (1984). "Polymorphic type schemes and recursive definitions". International Symposium on Programming, Toulouse, France. Lecture Notes in Computer Science. 167: 217–228. doi:10.1007/3-540-12925-1_41.
- Emms, Martin; Leiß, Hans (1996). "Extending the type checker for SML by polymorphic recursion—A correctness proof". Technical Report 96-101. Centrum für Informations- und Sprachverarbeitung, Universität München.
- Richard Bird and Lambert Meertens (1998). "Nested Datatypes".
- C. Vasconcellos, L. Figueiredo, C. Camarao (2003). "Practical Type Inference for Polymorphic Recursion: an Implementation in Haskell". Journal of Universal Computer Science.
- L. Figueiredo, C. Camarao. "Type Inference for Polymorphic Recursive Definitions: a Specification in Haskell".
External links
- Standard ML with polymorphic recursion by Hans Leiß, University of Munich