Catamorphism

A catamorphism is the generalization of the fold over lists to every recursive data type. It replaces each constructor in a value with a given function, so the value is consumed from the leaves upward: evaluating an expression tree, computing its depth or printing it are catamorphisms. In category theory a catamorphism is the unique homomorphism from the initial algebra of a functor into any other algebra of that functor^[1][3]. Writing a data type as the fixed point of a base functor lets one function, cata, fold every such type: the recursion is written once, and each computation is reduced to an algebra that handles a single layer. Catamorphisms are the simplest of the recursion schemes, whose duals are anamorphisms and whose composites are hylomorphisms.

A recursive function on a tree typically does two things: it recurses into the subtrees, and it combines the results for one node. The first part is the same for every such function on the type. Separating it out requires a type describing one layer of the tree with the subtrees replaced by the results computed for them. For arithmetic expressions:

This is the base functor of the type; its map applies a function to the recursive positions. The expression type itself is the solution of $E\cong ExprFE$, obtained by tying the knot with a constructor $in:ExprFE\to E$. A function $\phi :ExprFA\to A$, which says how to compute a result for a node from the results for its children, is an algebra, and its catamorphism applies it everywhere:

(* The base functor of arithmetic expressions: one layer of the tree, with
   the recursive positions replaced by a type parameter. *)
type 'r expr_f = Num of int | Add of 'r * 'r | Mul of 'r * 'r | Neg of 'r
 
let map f = function Num n -> Num n | Add (a, b) -> Add (f a, f b) | Mul (a, b) -> Mul (f a, f b) | Neg a -> Neg (f a)
 
(* The recursive type is the fixed point of the functor. *)
type expr = In of expr expr_f
 
(* The catamorphism of an algebra: fold the children, then apply the
   algebra to the layer. The only recursion is here. *)
let rec cata alg (In layer) = alg (map (cata alg) layer)
 
(* Algebras: what to do with one layer whose children are already done. *)
let eval = function Num n -> n | Add (a, b) -> a + b | Mul (a, b) -> a * b | Neg a -> -a
 
let show = function
  | Num n -> string_of_int n
  | Add (a, b) -> "(" ^ a ^ " + " ^ b ^ ")"
  | Mul (a, b) -> a ^ " * " ^ b
  | Neg a -> "-(" ^ a ^ ")"
 
let depth = function Num _ -> 1 | Add (a, b) | Mul (a, b) -> 1 + max a b | Neg a -> 1 + a
 
(* An algebra whose carrier is expr again: simplification, bottom up. *)
let simplify = function
  | Mul (In (Num 0), _) | Mul (_, In (Num 0)) -> In (Num 0)
  | Mul (In (Num 1), e) | Mul (e, In (Num 1)) | Add (In (Num 0), e) | Add (e, In (Num 0)) -> e
  | Neg (In (Neg e)) -> e
  | layer -> In layer
 
let num n = In (Num n) and add a b = In (Add (a, b)) and mul a b = In (Mul (a, b)) and neg a = In (Neg a)

show      (1 * (3 + 0) + -(-(2 * 5)))
eval      13
depth     5
simplify  (3 + 2 * 5)   (eval 13, depth 3)
cata In e = e: true

None of the algebras is recursive. simplify has expressions as its carrier and rewrites each layer after its children have been simplified, so the double negation and the multiplications by one are removed in one bottom-up pass. The algebra $in$, which only rebuilds the layer, gives the identity.

For a functor $F$, an $F$-algebra is an object $A$ with an arrow $\phi :FA\to A$. A homomorphism from $(A,\phi )$ to $(B,\psi )$ is an arrow $h:A\to B$ with $h\circ \phi =\psi \circ Fh$. An initial algebra $(\mu F,in)$ is one with exactly one homomorphism to every algebra; that homomorphism is the catamorphism $(|\phi |)$, and it is characterized by the commuting square^[1][3]:

The data types of functional languages are initial algebras: lists over $a$ of $FX=1+a\times X$, natural numbers of $FX=1+X$, binary trees of $FX=1+X\times a\times X$. An algebra for lists is a value for the empty list and a function for ::, and its catamorphism is fold_right. Lambek's lemma says that $in$ is an isomorphism, so the initial algebra is a fixed point of $F$, $\mu F\cong F\mu F$^[4]. The notation $(|\phi |)$, with "banana brackets", is from Meijer, Fokkinga and Paterson^[1].

Uniqueness gives a proof principle, the universal property: any $h$ satisfying the defining equation of the catamorphism is equal to it^[7].

From it follow the reflection law, the fusion law and the banana-split law^[1][9]:

Fusion moves a function applied after a fold into the fold, removing an intermediate result; the foldr/build rule of the Glasgow Haskell Compiler is an instance for lists^[10]. Banana split combines two folds over the same structure into one fold that computes both, with a single traversal.

A catamorphism's algebra sees only the results for the children. Some functions also need the children themselves: factorial needs $n$ as well as $(n-1)!$. A paramorphism provides both, with an algebra of type $F(\mu F\times A)\to A$^[5]. It corresponds to primitive recursion, as the catamorphism corresponds to iteration.

(* Lists and natural numbers as fixed points, with their catamorphisms. *)
type ('a, 'r) list_f = Nil | Cons of 'a * 'r
let rec cata_list alg = function [] -> alg Nil | x :: xs -> alg (Cons (x, cata_list alg xs))
 
type 'r nat_f = Z | S of 'r
let rec cata_nat alg n = if n = 0 then alg Z else alg (S (cata_nat alg (n - 1)))
 
(* Two catamorphisms over the same structure combine into one whose
   algebra works on pairs ("banana split"). *)
let sum_alg = function Nil -> 0 | Cons (x, s) -> x + s
let len_alg = function Nil -> 0 | Cons (_, n) -> n + 1
let split a1 a2 = function
  | Nil -> (a1 Nil, a2 Nil)
  | Cons (x, (r1, r2)) -> (a1 (Cons (x, r1)), a2 (Cons (x, r2)))
 
(* A paramorphism also sees the original substructure, not only its fold.
   Factorial needs n as well as (n-1)!. *)
let rec para_nat alg n = if n = 0 then alg Z else alg (S (n - 1, para_nat alg (n - 1)))
let fact = para_nat (function Z -> 1 | S (m, r) -> (m + 1) * r)
 
(* Suffixes of a list: each step keeps the list it was given. *)
let rec para_list alg = function [] -> alg Nil | x :: xs -> alg (Cons (x, (xs, para_list alg xs)))
let suffixes = para_list (function Nil -> [ [] ] | Cons (x, (xs, r)) -> (x :: xs) :: r)

sum and length in one pass: 108, 6
2^10 as a catamorphism on naturals: 1024
fact 10 as a paramorphism: 3628800
suffixes [1; 2; 3]: [1;2;3] [2;3] [3] []

A histomorphism gives the algebra the results for all earlier substructures, not only the immediate children, which expresses dynamic programming such as the Fibonacci recurrence^[6]. The duals of these schemes build structures instead of consuming them: anamorphisms dual to catamorphisms, apomorphisms to paramorphisms and futumorphisms to histomorphisms. A hylomorphism builds a structure with an anamorphism and consumes it with a catamorphism. Hinze, Wu and Gibbons showed that all of these are instances of one scheme, the adjoint fold^[8].

A catamorphism over a finite value terminates if its algebra does, since each recursive call is on a proper substructure. Programs written only with catamorphisms over inductive types therefore always terminate, which is why total languages and proof assistants allow structural recursion and reject general recursion. In a lazy language such as Haskell a type may also contain infinite values, and a catamorphism over one need not terminate.

Haskell's recursion-schemes library provides the base functor of a data type through the Base type family and generates it with Template Haskell, and defines cata, para, histo and their duals once for all types. In OCaml, where there are no higher-kinded types, the base functor and its map are written by hand, as above, or with a functor over a module describing the base functor. Compilers use catamorphisms for passes over syntax trees that are compositional, where the result for a node depends only on the results for its children: evaluation, type synthesis in simple type systems, free-variable computation and code generation for expressions.

The word is from the Greek κατά, "downward". Algebraic accounts of data types as initial algebras go back to the work of the ADJ group in the 1970s, and Lambek's lemma to 1968^[4]. Malcolm used the initial-algebra view to derive program transformations for arbitrary data types in 1990^[2], and Meijer, Fokkinga and Paterson named catamorphisms, anamorphisms, hylomorphisms and paramorphisms, with their bracket notations, in 1991^[1]. Meertens analysed paramorphisms in 1992^[5], and Bird and de Moor's Algebra of Programming built a calculus of programs on them in 1997^[3].

• AnamorphismAn anamorphism is the generalization of unfold: it builds a value of a recursive data type from a seed, using a function (a coalgebra) that produces one layer of the structure together with new seeds for its recursive positions. It is the categorical dual of the catamorphism, the unique homomorphism from any coalgebra into the final coalgebra of a functor. Anamorphisms can produce infinite structures such as streams, and they are the way to write corecursive programs that are guaranteed to be productive.
• HylomorphismA function that unfolds a seed into a recursive structure and folds that structure into a result, written so the structure is never built: hylo f g = f . fmap (hylo f g) . g. The call tree of the recursion is the intermediate structure.
• FoldableFoldable is the abstraction of a container whose elements can be combined in order: a list, a tree, an option. A fold replaces the constructors of the structure with a function and a starting value, and every summary of the elements, their sum, length, maximum, list of elements or whether any satisfies a predicate, is derived from it. Equivalently, a foldable container maps each element into a monoid and combines the results (foldMap). The universal property of fold characterizes exactly which functions are folds.
• FunctorIn functional programming, a functor is a type constructor f with an operation fmap : (a -> b) -> f a -> f b that applies a function inside the structure without changing its shape, preserving identity and composition. Lists, options, trees and functions out of a fixed type are functors. The notion comes from category theory. In OCaml the word also names parametrised modules such as Map.Make.
• Algebraic data typeAn algebraic data type is a type built from sums, where a value is one of several alternatives, and products, where a value has several components at once, possibly recursively. The name comes from counting: the number of values of a sum is the sum of the counts, and of a product their product, so types obey the laws of algebra. Values are taken apart by pattern matching, which the compiler checks for missing cases.

1. [1]E. Meijer, M. Fokkinga, R. Paterson, “Functional programming with bananas, lenses, envelopes and barbed wire”, Functional Programming Languages and Computer Architecture (1991).
2. [2]G. Malcolm, “Data structures and program transformation”, Science of Computer Programming 14 (1990).
3. [3]R. Bird, O. de Moor, Algebra of Programming, Prentice Hall (1997).
4. [4]J. Lambek, “A fixpoint theorem for complete categories”, Mathematische Zeitschrift 103 (1968).
5. [5]L. Meertens, “Paramorphisms”, Formal Aspects of Computing 4 (1992).
6. [6]T. Uustalu, V. Vene, “Primitive (co)recursion and course-of-value (co)iteration, categorically”, Informatica 10 (1999).
7. [7]G. Hutton, “A tutorial on the universality and expressiveness of fold”, Journal of Functional Programming 9 (1999).
8. [8]R. Hinze, N. Wu, J. Gibbons, “Unifying structured recursion schemes”, ICFP (2013).
9. [9]M. M. Fokkinga, Law and Order in Algorithmics, PhD thesis, University of Twente (1992).
10. [10]A. Gill, J. Launchbury, S. L. Peyton Jones, “A short cut to deforestation”, Functional Programming Languages and Computer Architecture (1993).

last updated 27 September 2026