Type Fixpoints: Iteration vs. Recursion

Positive recursive (fixpoint) types can be added to the polymorphic (Church-style) lambda calculuS\2 (System F) in several different ways, depending on the choice of the elimination operator. We compare several such definitions and we show that they fall into two equivalence classes with respect to mutual interpretability by means of beta-eta reductions. Elimination operators for fixpoint types are thus classified as either "iterators" or "recursors". This classification has an interpretation in terms of the Curry-Howard correspondence: types of iterators and recursors can be seen as images of induction axioms under different dependencyerasing maps. Systems with recursors are beta-eta equivalent to a calculus (lambdal)2U of recursive types with the operators Fold : b(mu.b/a] -> mu.b and Unfold : mu.b->b[mub.b/b], where the composition Unfold o Fold reduces to identity. It is known that systems with iterators can be defined within (lambdal)2, by means of beta reductions. We conjecture that systems with recursors can not. In this paper we show that the system (lambdal)2U does not have such a property. For this we study the notion of polymorphic type embeddability (via (beta) left-iilvertible terms) and we show that if a type a is embedded into another type T then T must be of depth at least equal to the depth of b.