Polymorphic recursion

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.

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.

See also

• Higher-ranked polymorphism

Further reading

• Meertens, Lambert (1983). "Incremental polymorphic type checking in B" (PDF). ACM Symposium on Principles of Programming Languages (POPL), Austin, Texas.
• 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.
• 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)
• Kfoury, A. J.; Tiuryn, J.; Urzyczyn, P. (April 1993). "Type reconstruction in the presence of polymorphic recursion". ACM Transactions on Programming Languages and Systems. 15 (2). New York, NY, USA: ACM: 290–311. doi:10.1145/169701.169687. ISSN 0164-0925.
• Michael I. Schwartzbach (June 1995). "Polymorphic type inference". Technical Report BRICS-LS-95-3. BRICS.
• 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".
• Hallett, J. J; Kfoury, A. J. (July 2005). "Programming Examples Needing Polymorphic Recursion". Electronic Notes in Theoretical Computer Science. 136. Amsterdam, The Netherlands: Elsevier Science Publishers B. V.: 57–102. doi:10.1016/j.entcs.2005.06.014. ISSN 1571-0661.

External links

• Standard ML with polymorphic recursion by Hans Leiß, University of Munich