Composition with recursion in functions between types

Question

I always understood functions in functional programming to be modeled by morphisms in the category of types, where any powerful function you write in your code is a morphism that is the composition of other morphisms within that category (in Haskell there are bottoms, I know. I'm speaking in general terms here).

But I can't grasp how that interacts with recursion. Putting F-algebras aside for now (I'll get there), the naive representation is that a composition of morphisms can be one of the morphisms in the composition; i.e. for some morphisms f, g, h you could have g = f ￮ g ￮ h, which is surely an impossible equality in general, as f and h need not be identity morphisms.

So then there are recursion schemes (catamorphism and friends). If you're modeling, say, using factorial in a function, do you compose with a functor into the category of F-algebras (or F-coalgebras), do all the magic there, and come back to the category of types for the rest of the composition? Do all the F-algebras (and F-coalgebras) exist already in the category of types, with the right initial and terminal morphisms between them? And in either case, how does one construct the polynomial functor for factorial?

I'm assuming that whatever the answer to this question is, it's the most common/standard method of modeling looping computation in category theory; correct me if this is incorrect.

Answer 1

(I'm going to try to write an answer for functional programmers, with Haskell-like code.)

First, you should know that using higher-order functions, recursive definitions can be turned into fixed-point equations. Typically, defining

fac :: Int -> Int
fac n = if n <= 0 then 1 else n * fact (n-1)

amounts to asking that fac satisfies the fixed-point equation fac == f fac (in other words that fac is a fixed point of f), for

f :: (Int -> Int) -> Int -> Int
f rec n = if n <= 0 then 1 else n * rec (n-1)

This f has a completely non-circular definition, so to give meaning to recursive definitions it suffices to have a "fixed-point operator"

fix :: (a -> a) -> a

that guarantees fix g == g (fix g) for every function g, because then we can define fact = fix f (instantiating a to Int -> Int), cf. https://hackage.haskell.org/package/base/docs/Data-Function.html#v:fix

So now, the category-theoretic counterpart of fix is going to be a family of morphisms $fix_A : (A \to A) \to A$ satisfying a bunch of conditions (such as the fixed-point equation and dinaturality); such categorical fixed-point operators have been studied in the literature, for example here (this paper involves the domain theory that Andrej mentioned). And that gives you a categorical treatment of general recursion!

(I'll let someone else explain the catamorphism stuff, but for now let me note that there is no "polynomial functor for factorial", but there is a functor whose initial algebra is the natural numbers.)

Answer 2

The theory behind recursion schemes is that algebraic data types are initial algebras.

1. Recursive types and folds

The programmer's point of view is that, given a recursive type,

data Tree = Node Tree Tree | Leaf

... there is a standard way to consume it, which is a fold:

fold :: (a -> a -> a) -> a -> Tree -> a
fold node leaf (Node l r) = node (fold node leaf l) (fold node leaf r)
fold node leaf Leaf = leaf

fold pattern-matches on a tree, makes recursive calls on the children, and combines the result somehow. The point is that:

1. many recursive functions fit this mold (including factorial; it's not the best example, but for that exact reason it's a good exercise for the reader to (1) write the fold for Peano Nat; (2) define factorial using fold)
2. if you disallow explicit recursion, and program only using folds, then your functions are guaranteed to terminate.

See also Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. It is the inspiration for the recursion-schemes library in Haskell, whose description used to read "Generalized bananas, lenses and barbed wire".

2. Initial algebras

The mathematician's point of view is that a data type such as Tree is a language, i.e., a set/type of expressions:

Tree :: Type

Constructors are the words of that language:

Node :: Tree -> Tree -> Tree
Leaf :: Tree

Given a semantic domain a, and an interpretation of those words in that domain:

node :: a -> a -> a
leaf :: a

... we obtain an interpretation of whole expressions, which is precisely a fold:

fold node leaf :: Tree -> a

An "interpretation" is also called an algebra, or algebraic structure:

In mathematics, an algebraic structure consists of a nonempty set A (called the underlying set, carrier set or domain), [and] a collection of operations on A (typically binary operations such as addition and multiplication) (...).

--- Algebraic structure, Wikipedia

In the case of binary trees, the structures they describe are called magmas. Most other data types don't correspond to a notable class of algebraic structures, if they have a name at all. So the individual structures are not what's interesting about this point of view. Instead, meditate on the idea that words don't have intrinsic value, and their worth is in their meaning.

A language, can be viewed as a trivial interpretation---an algebra---of itself.

fold Node Leaf :: Tree -> Tree
= id

And in the category of algebras, it is an initial object, also called "free algebra". It is the most general algebra (for a given signature, here of node and leaf): it can be mapped (in a respectful manner, i.e., via a homomorphism) into any other algebra, and there is only one way to do so, using fold.

The basic method of introducing a new concrete data type, as in a number of other languages, is to declare a free algebra.

--- Miranda: A non-strict functional language with polymorphic types, D. A. Turner, 1985

3. Initial F-algebras

The notion of F-algebra in category theory generalizes the idea of algebras further. As mentioned above, an algebra is a set a equipped with some operations.

node :: a -> a -> a
leaf :: a

This can be rearranged into an F-algebra: a set a equipped with one morphism of this form:

alg :: F a -> a

for some endofunctor F which encodes the shape of the operations. Here, for node and leaf, the relevant functor is F a = (a × a) + 1 (in Haskell, × is the tuple type (,), + is Either, 1 is the unit type ()).

alg :: (a × a) + 1 -> a

-- gives the same information as ---

node :: a -> a -> a
leaf :: a

The point is that the definition of an algebra is seemingly tied to the notion of sets: "a SET equipped with operations"). In contrast, we can talk about F-algebras in any category, for example in a category of domains. Whereas the category of sets has total functions, domains give semantics to programming languages with nontermination. We don't need to reinvent universal algebra---where algebras are traditionally carried by sets---from sets to domain theory or whatever, because instead we can prove general theorems about F-algebras in any category and then apply them to the relevant category.

To sum up, folds are a principled way of implementing recursive functions, in many senses:

1. if you only use folds, avoiding unstructured recursion, programs are guaranteed to terminate. This eliminates the class of mistakes "accidental infinite loop".

2. Folds play a natural role in programming language theory: a fold gives a compositional intepretation of a language in terms of its individual constructors. It can also be quite illuminating to to go the other way, viewing arbitrary data types as languages. I would argue that it can be a good perspective from which to appreciate general ideas such as Church encodings or defunctionalization.

3. Data types and their folds can be represented as initial F-algebras and catamorphisms, which make sense in categories which may model your programming language more accurately than sets and total functions, with the prime example of domains for modelling nontermination.

4. What about final F-coalgebras, aka., unfolds? This is getting too long so I'll briefly make the following points.

   a. F-coalgebras s -> F s can be thought of as an extremely general class of state machines, using the functor F to encode various forms of inputs and outputs. Unfolding an F-coalgebra turns it into an infinite tree, which may be more intuitive to manipulate.

   b. fold and unfold recover Turing-completess. And now you have algebraically inspired primitives instead of unstructured loops. A possible application is that optimizations like deforestation (removing intermediate data structures) become "just" an exercise in equational reasoning.