AbstractWithin the setting of the categorical approach to total functional programming, we introduce a ``many-in-one'' recursion scheme that neatly unifies a variety of seemingly diverging strengthenings of the basic recursion scheme of iteration. The new scheme is doubly generic: in addition to being parametric in a functor capturing the signature of an inductive type, it is also parametric in a comonad and a distributive law (of the functor over the comonad) that together encode the recursive call pattern of a particular recursion scheme for this inductive type. Specializations of the scheme for particular comonads and distributive laws include (simple) iteration and mild generalizations of primitive recursion and course-of-value iteration.
Categories and Subject Descriptors: D.1.1 [Programming Techniques]: Applicative (Functional) Programming; D.3.3 [Programming Languages]: Language Constructs and Features; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs
Additional Key Words and Phrases: inductive types, iteration, recursion schemes, initial functor-algebras, comonads, distributive laws, functional programming, genericity, category-theoretic
Selected references
- Tarmo Uustalu and Varmo Vene. Mendler-Style Inductive Types, Categorically. Nordic Journal of Computing, 6(3):343-361, Fall 1999.
- Philip Wadler. The essence of functional programming. In Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 1-14, Albequerque, New Mexico, January 1992.