Inductive and Coinductive Types with Iteration and Recursion
J.H. Geuvers · Radboud Repository (Radboud University) · 1992
We study extensions of simply and polymorphically typed lambda calculus from a point o f v i e w o f h o w iterative and recursive functions on inductive t ypes are represented.The inductive t ypes can usually be understood as initial algebras in a certain category and then recursion can be dened in terms of iteration.However, in the syntax we often have only weak initiality, w h i c h makes the denition of recursion in terms of iteration inecient or just impossible.We propose a categorical notion of primitive recursion which can easily be added as computation rule to a typed lambda calculus and gives us a clear view on what the dual of recursion, corecursion, on coinductive t ypes is.The same notion has, independently, been proposed by Mendler 1991.We l o o k a t h o w these syntactic notions work out in the simply typed lambda calculus and the polymorphic lambda calculus.It will turn out that in the syntax, recursion can be dened in terms of corecursion and vice versa using polymorphism: Polymorphic lambda calculus with a scheme for either recursion or corecursion suces to be able to dene the other.We compare our syntax for recursion and corecursion with that of Mendler Mendler 1987 and use the latter to obtain meta properties as conuence and normalization.Denition 2.1 Let C be a c ategory, T a functor from C to C.1.A T-algebra in C i s a p air A f, w i t h A an object and f : TA! A.