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:
- 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
)
- 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:
if you only use folds, avoiding unstructured recursion, programs are guaranteed to terminate. This eliminates the class of mistakes "accidental infinite loop".
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.
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.
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.