INTRODUCTION TO CATEGORY THEORY
Graham Hutton
Lecture 5  Case Study
INTRODUCTION

Recall that the four constructions
0 = initial object
1 = terminal object
= product
= coproduct
are defined by "universal properties"
For anything that "looks like" an X,
there is a unique arrow that factorises
the lookalike X in terms of a real X
and are valid "definitions" in that
There may be more than one X, but they
will all be "uniquely isomorphic".
Examples:

 SET REL Preordered sets
+

0  empty empty minimal
 set set element

1  singleton empty maximal
 set set element

x  Cartesian disjoint maximal
 product sum lower bound

+  disjoint disjoint mimimal
 sum sum upper bound
This lecture:

++
 Case study = a simple categorical calculus 
 for defining and reasoning about recursive 
 datatypes and recursive programs. 
++
ALGEBRAS

The categorical notion of an "Falgebra" generalises
the settheoretic notion of an algebra.
Definition: an "Falgebra" for a functor
F : C > C on a category C is a pair
where
A is a "carrier" object;
f : FA > A is a "operator" arrow.
Examples:

o A monoid can be viewed as an algebra for a
functor M : SET > SET by first interpreting the
constant a in A as a function a : 1 > A, and then
"joining" together the two functions + and a:
+ : AxA > A ^ a : 1 > A
=> { typing rule for v }
+ v a : AxA + 1 > A
<=> { define MX = XxX + 1 }
+ v a : MA > A
<=> { definition of Falgebra }
is an Malgebra
o The recursive datatype of natural numbers
Nat ::= Zero  Succ Nat
can be viewed as an algebra for a functor N : SET
> SET by first interpreting the constant Zero in
Nat as a function Zero : 1 > Nat, and then "joining"
together the two functions Zero and Succ:
Zero : 1 > Nat ^ Succ : Nat > Nat
=> { typing rule for v }
Zero v Succ : 1+Nat > Nat
<=> { define NA = 1+A }
Zero v Succ : N Nat > Nat
<=> { definiton of Falgebra }
is an Nalgebra
Notes:

o It is common to only define the "object" part
of a functor, leaving the "arrow" part implicit,
e.g. we implicitly define Mf = fxf + id_1 and
Nf = id_1 + f in the two examples above.
o The "arrow" part of a functor F plays no role
yet. It only comes into play when we consider
"homomorphisms" between Falgebras.
HOMOMORPHISMS

The categorical notion of an "Fhomomorphism"
generalises the algebraic notion of a homomorphism.
Definition: an Fhomomorphism
h : >
from one Falgebra to another is an arrow h :
A > B such that the following square commutes:
Fh
FA > FB
 
f   g
 
v v
A > B
h
Example:

Suppose that and are monoids, i.e.
algebras for the functor M. Then the following
calculation shows that an Mhomomorphism between
Malgebras is precisely a monoid homomorphism:
h : >
<=> { definition of Fhomomorphism }
h . (+ v a) = (x v b) . Mh
<=> { definition of M }
h . (+ v a) = (x v b) . (hxh + id_1)
<=> { properties of sums }
(h . +) v (h . a) = (x . hxh) v (b . id_1)
<=> { property of v }
h . + = x . hxh ^ h . a = b
<=> { extensionality }
forall a1,a2 in A. h (a1 + a2) = h (a1) x h (a2)
h a = b
HOMOMORPHISMS AS ARROWS

Definition: if F : C > C is a functor, then the
"algebra category" Alg(F) is defined as follows:
Objects  Falgebras.
Arrows  Fhomomorphisms.
Identities  as in C.
Composition  as in C.
For this definition to be valid:
o Identities must be Fhomomorphisms, i.e.
F(id_A)
FA > FA
 
f   f
 
v v
A > A
id_A
commutes for each f. The holds because
F is a functor and hence F(id_A) = id_FA.
o Composition must preserve Fhomomorphisms.
Consider the following diagram:
F(joi)

/ (4) \
 Fi Fj v
FA > FB > FC
  
f  (1) g  (2)  h
  
v v v
A > B > C
 i j ^
\ (3) /

joi
Assuming that i and j are Fhomomorphisms,
then it is easy to see that because
(1) and (2) commute (by assumption)
(3) commutes (by composition)
(4) commutes (F is a functor)
the outer rectangle also commutes, which shows
that joi is an Fhomomorphism, as required.
INITIAL ALGEBRAS

The categorical notion of an "initial algebra"
generalises the notion of a recursive datatype.
Definition: if F : C > C is a functor, then an
"initial Falgebra" is an initial object in Alg(F).
Notes:
o We often write uF for the carrier of an initial
Falgebra and in for the operator, i.e.
in : F uF > uF
o It can be shown that in is invertible, which means
that we have an isomorphism F uF ~ uF. The unique
inverse of in is written as out, i.e.
out : uF > F uF
o There may be more than one initial Falgebra for a
functor F, but they are all "uniquely isomorphic".
Examples:

Given the recursive datatypes
Nat ::= Zero  Succ Nat
List A ::= Nil  Cons A (List A)
Tree A ::= Leaf A  Node (Tree A) (Tree A)
it can be shown that the corresponding functors
N X = 1 + X
L X = 1 + AxX
T X = A + XxX
each have an initial algebra, defined by
=
=
=
More generally:
++
 Many initial algebras used in computing 
 are similar to these examples, in that: 
 
 uF = a recursive datatype; 
 
 in = the join of the constructors. 
++
CATAMORPHISMS

The categorical notion of a "catamorphism" encapsulates
a common pattern for defining recursive programs.
Definition: if is an initial Falgebra and
is an Falgebra, then the "catamorphism"
{f} : uF > A
is defined as the unique arrow that makes the
following homomorphism diagram commute:
F {f}
F uF > FA
 
in   f
 
v v
uF      > A
{f}
Examples:

o If is an Nalgebra, then {a v f} : Nat
> A is uniquely defined by the equation
{a v f} . (Zero v Succ) = (a v f) . N {a v f}
A simple calculation shows that this equation is
equivalent to the recursive definition
{a v f} (Zero) = a
{a v f} (Succ n) = f ({a v f} (n))
which encapsulates a common pattern of recursion
for processing natural numbers. For example,
eval : Nat > Z
eval = {0 v +1}
+ : Nat x Nat > Nat
m+n = {n v Succ} (m)
o If is an Lalgebra, then {b v f} : List
A > B is uniquely defined by the equations
{b v f} (Nil) = b
{b v f} (Cons a as) = f (a, {b v f} (as))
which encapsulate a common pattern of recursion
for processing lists. For example,
length : List A > Z
length = {0 v (+1 . pi_1)}
++ : List A x List A > List A
xs ++ ys = {ys v Cons} xs
More generally:
++
 Many recursive programs used in computing 
 can be defined in terms of catamorphisms. 
++
Universality:

Formally, the defining commuting diagram for an
initial Falgebra states that rhe equivalence
g . in = f . Fg <=> g = {f}
holds for all g : uF > A. This equivalence is
known as the "universal property" of {_}, and is
the key to proving properties of catamorphisms.
FUSION

Suppose that we are given a commuting diagram
F {f} Fh
F uF > FA > FB
  
in   f  g
  
v v v
uF      > A > B
{f} h
That is,
is an initial Falgebra;
and are Falgebras;
h : > is an Fhomomorphism.
Then the following "fusion" law that states
that the composition of a homomorphism and
catamorphism is again a catamorphism:
h . {f} = {g}
Proof:
h . {f} = {g}
<=> { universal property of {_} }
h . {f} . in = g . F (h . {f})
<=> { F is a functor }
h . {f} . in = g . Fh . F{f}
<=> { {f} is an Fhomomorphism }
h . f . F{f} = g . Fh . F{f}
<= { cancellation }
h . f = g . Fh
<=> { h is an Fhomomorphism }
true
Note: fusion is a "generic" law that applies
uniformly to any recursive datatype uF.
Example:

Multiplying the length of a list by a constant
can be expressed in the form of a catmorphism:
(n*) . length
= { definition of length}
(n*) . {0 v (+1 . pi_1)}
= { fusion for lists }
{0 v (n+ . pi_1)}
The final catamorphism behaves as follows:
f (Nil) = 0
f (Cons x xs) = n + f xs
BANANA SPLIT

Suppose that we are given a commuting diagram
F {f} F {g}
FA < F uF > FB
  
f   in  g
  
v v v
A <      uF     > B
{f} {g}
That is,
is an initial Falgebra;
and are Falgebras.
Then in a category with products the following
"banana split" law states that the split of
two catamorphisms is again a catamorphism:
{f} ^ {g} = {f . F pi_0 ^ g . F pi_1}
Proof: by the universal property of {_}, the
banan split law is equivalent to
{f} ^ {g} . in
=
(f . F pi_0 ^ g . F pi_1) . F ({f} ^ {g})
which can be verified as follows:
(f . F pi_0 ^ g . F pi_1) . F ({f} ^ {g})
= { property of ^ }
(f . F pi_0 . F ({f} ^ {g})) ^
(g . F pi_1 . F ({f} ^ {g}))
= { F is a functor }
(f . F (pi_0 . {f}^{g})) ^
(g . F (pi_1 . {f}^{g}))
= { property of ^ }
(f . F {f}) ^ (g . F {g})
= { {f} and {g} are Fhomomorphisms }
({f} . in) ^ ({g} . in}
= { property of ^ }
{f}^{g} . in
Note: banana split is a "generic" law that applies
uniformly to any recursive datatype uF.
Example:

Copying a list and calculating its length can
be expressed in the form of a catamorphism:
id_(List A) ^ length
= { definition of length}
id_(List A) ^ {0 v (+1 . pi_1)}
= { identity catamorphism }
{Nil v Cons} ^ {0 v (+1 . pi_1}}
= { banana split }
{(Nil v Cons) . L pi_0 ^
(0 v (+1 . pi_1)) . L pi_1}
= { simplification }
{(Nil ^ 0) v
((Cons . (id_A x pi_0)) ^ (+1 . pi_1 . pi_1))}
The final catamorphism behaves as follows:
f (Nil) = (Nil, 0)
f (Cons x xs) = (Cons x xs', n+1)
where
(xs',n) = f (xs)