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.^[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

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.

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}}: |access-date= requires |url= (help); Unknown parameter |booktitle= ignored (|book-title= suggested) (help)

External links

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

[FOOTNOTEHenglein1993-1] Henglein 1993.

[2] 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.

[3] 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}}: |access-date= requires |url= (help); Unknown parameter |booktitle= ignored (|book-title= suggested) (help)

[1]

[2]

[3]