Polymorphic recursion
In computer science, polymorphic recursion (also referred to as Milner–Mycroft typability or the Milner–Mycroft calculus) refers to a recursive parametrically polymorphic 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 therefore 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
Note that Haskell normally infers the type signature for a function as simple-looking as this, but here it cannot be omitted without triggering a type error.
Higher-ranked types
![[icon]](/wiki/File:Wiki_letter_w_cropped.svg){kind=small} | This section needs expansion. You can help by adding to it. (May 2012) |
Applications
Program analysis
In type-based program analysis polymorphic recursion is often essential in gaining high precision of the analysis. Notable examples of systems employing polymorphic recursion include Dussart, Henglein and Mossin's binding-time analysis[2] and the Tofte–Talpin region-based memory management system.[3] As these systems assume the expressions have already been typed in an underlying type system (not necessary employing polymorphic recursion), inference can be made decidable again.
Data structures, error detection, graph solutions
Functional programming data structures often use polymorphic recursion to simplify type error checks and solve problems with nasty "middle" temporary solutions that devour memory in more traditional data structures such as trees. In the two citations that follow, Okasaki (pp. 144-146) gives a CONS example in Haskell wherein the polymorphic type system automatically flags programmer errors.[4] The recursive aspect is that the type definition assures that the outermost constructor has a single element, the second a pair, the third a pair of pairs, etc. recursively, setting an automatic error finding pattern in the data type. Roberts (p. 171) gives a related example in Java, using a Class to represent a stack frame. The example given is a solution to the Tower of Hanoi problem wherein a stack simulates polymorphic recursion with a beginning, temporary and ending nested stack substitution structure.[5]
See also
Notes
- ^ Henglein 1993.
- ^ Dussart, Dirk; Henglein, Fritz; Mossin, Christian. "Polymorphic Recursion and Subtype Qualifications: Polymorphic Binding-Time Analysis in Polynomial Time". Proceedings of the 2nd International Static Analysis Symposium (SAS). Springer-Verlag.
- ^
Tofte, Mads; Talpin, Jean-Pierre (1994). "Implementation of the Typed Call-by-Value λ-calculus using a Stack of Regions". POPL '94: Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM. pp. 188–201. doi:10.1145/174675.177855. ISBN 0-89791-636-0.
{{cite conference}}: Unknown parameter|booktitle=ignored (|book-title=suggested) (help) - ^ Chris Okasaki (1999). Purely Functional Data Structures. New York: Cambridge. p. 144. ISBN 978-0521663502.
- ^ Eric Roberts (2006). Thinking Recursively with Java. New York: Wiley. p. 171. ISBN 978-0471701460.
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
 | This computer-programming-related article is a stub. You can help Wikipedia by expanding it. |