Jump to content

Polymorphic recursion

Add links
From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Ruud Koot (talk | contribs) at 20:07, 31 March 2012 (→Further reading: {{cite journal|author1 = Hallett, J. J|author2 = Kfoury, A. J.|title = Programming Examples Needing Polymorphic Recursion | journal = Electronic Notes in Theoretical Computer Science | date = July 2005 | volume = 136 | issn). 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 refered 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

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

Notes

  1. ^ Henglein 1993.

Further reading

  • 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.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Polymorphic_recursion&oldid=484892931"