Tags: Programming Language.
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.