Polymorphic recursion


In computer science, polymorphic recursion 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.

Example

Nested datatypes

Consider the following nested datatype:

data Nested a = a :<: | Epsilon
infixr 5 :<:
nested = 1 :<: :<: 5,6],, in the recursive call:

length :: Nested a -> Int
length Epsilon = 0
length = 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

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 and the Tofte-Talpin region-based memory management system. As these systems assume the expressions have already been typed in an underlying type system, 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 gives a CONS example in Haskell wherein the polymorphic type system automatically flags programmer errors. 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 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.