INTRODUCTION TO CATEGORY THEORY Graham Hutton Lecture 5 - Case Study INTRODUCTION ------------ Recall that the four constructions 0 = initial object 1 = terminal object = product = co-product are defined by "universal properties" For anything that "looks like" an X, there is a unique arrow that factorises the look-a-like 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 Pre-ordered 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 "F-algebra" generalises the set-theoretic notion of an algebra. Definition: an "F-algebra" 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 F-algebra } is an M-algebra 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 F-algebra } is an N-algebra 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 F-algebras. HOMOMORPHISMS ------------- The categorical notion of an "F-homomorphism" generalises the algebraic notion of a homomorphism. Definition: an F-homomorphism h : -> from one F-algebra 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 M-homomorphism between M-algebras is precisely a monoid homomorphism: h : -> <=> { definition of F-homomorphism } 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 - F-algebras. Arrows - F-homomorphisms. Identities - as in C. Composition - as in C. For this definition to be valid: o Identities must be F-homomorphisms, 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 F-homomorphisms. 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 F-homomorphisms, 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 F-homomorphism, 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 F-algebra" is an initial object in Alg(F). Notes: o We often write uF for the carrier of an initial F-algebra 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 F-algebra 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 F-algebra and is an F-algebra, 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 N-algebra, 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 L-algebra, 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 F-algebra 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 F-algebra; and are F-algebras; h : -> is an F-homomorphism. 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 F-homomorphism } h . f . F{f} = g . Fh . F{f} <= { cancellation } h . f = g . Fh <=> { h is an F-homomorphism } 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 F-algebra; and are F-algebras. 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 F-homomorphisms } ({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)