nLab catamorphism




Category theory



In the study of recursion schemes, a catamorphism is the simple case of a fold over an inductive data type. In category theoretic terms, this is simply the unique homomorphism out of an initial algebra.


Given an endofunctor FF such that the category of F F -algebras has an initial object (μF,in)(\mu F, in), the catamorphism for an FF-algebra (A,φ)(A, \varphi) is the unique homomorphism from the initial F F -algebra (μF,in)(\mu F, in) to (A,φ)(A, \varphi). The unique morphism between the carriers is also denoted cataφ:μFAcata \varphi \colon \mu F \rightarrow A.

From the commuting square of the homomorphism, we have (cataφ)in=φF(cataφ)(cata \varphi) \circ in = \varphi \circ F (cata \varphi). By Lambek's theorem, in\mathit{in} has an inverse out\mathit{out}, so the catamorphism can be recursively defined by cataφ=φF(cataφ)outcata \varphi = \varphi \circ F (cata \varphi) \circ out.


Fusion law


Let h:ABh \colon A \rightarrow B be a homomorphism between two FF-algebras φ:FAA\varphi \colon F A \rightarrow A and ψ:FBB\psi \colon F B \rightarrow B so that hφ=ψFhh \circ \varphi = \psi \circ F h. Then hcataφ=cataψh \circ cata \varphi = cata \psi.

As a recursion scheme

If μF\mu F is an inductive type, then the catamorphism is a fold over the type. Some recursive functions can then be implemented in terms of a catamorphism.

Example: Natural numbers

Let FF be the functor FX=1+XF X = 1 + X so that the naturals =μF\mathbb{N} = \mu F are represented by the fixed point of FF (i.e. the carrier of the initial F-algebra). The recursor for the naturals can then be defined by a catamorphism.

natrec :A.A(AA)A natrec Azs=cataφ,where φ(inl*)=z φ(inrn)=sn \begin{array}{l l} natrec &: \forall A. A \rightarrow (A \rightarrow A) \rightarrow \mathbb{N} \rightarrow A \\ natrec & A z s = cata \varphi, where \\ & \varphi (inl \ast) = z \\ & \varphi (inr n) = s n \end{array}


Last revised on December 15, 2022 at 23:35:07. See the history of this page for a list of all contributions to it.