Fixpoint Computations and Coiteration (Extended Abstract)

) Brian T. Howard Department of Computer and Information Sciences Kansas State University bhoward@cis.ksu.edu Abstract An extension of the simply-typed lambda calculus is presented which contains both wellstructured inductive and coinductive types, and which also identifies a class of types for which general recursion is possible. The motivations for this work are certain natural constructions in category theory, in particular the notion of an algebraically bounded functor, due to Freyd. We propose that this is a particularly elegant language in which to work with recursive objects, since the potential for general recursion is contained in a single operator which interacts well with the facilities for bounded iteration and coiteration. 1 Introduction In designing typed languages that include recursion, there has long been a tension between the structure provided by types based on well-founded induction and the freedom permitted by types based on general recursion. Very few languages..