Category Theory in Computer Science

Categories

A category C consists of:

• A collection of objects Ob(C)
• For each pair of objects A, B, a collection of morphisms Hom(A, B)
• Composition: g . f : A -> C for f : A -> B, g : B -> C
• Identity: id_A : A -> A for each object A

Laws: Associativity ((h . g) . f = h . (g . f)) and identity (id . f = f = f . id).

Key Examples in CS

Important Constructions

Product A x B: Universal object with projections pi_1 : A x B -> A, pi_2 : A x B -> B, satisfying the universal property: for any f : C -> A, g : C -> B, there exists unique (f, g) : C -> A x B.

Coproduct A + B: Dual of product. Injections inl : A -> A + B, inr : B -> A + B. For any f : A -> C, g : B -> C, there exists unique [f, g] : A + B -> C.

Exponential B^A (internal hom): Object representing functions A -> B. Satisfies Hom(C x A, B) ≅ Hom(C, B^A) (currying).

A Cartesian closed category (CCC) has all finite products and exponentials. CCCs are the categorical semantics of the simply typed lambda calculus.

Functors

A functor F : C -> D maps objects to objects and morphisms to morphisms, preserving composition and identities:

• F(g . f) = F(g) . F(f)
• F(id_A) = id_{F(A)}

Functors in Programming

In Haskell, Functor is an endofunctor on Hask:

class Functor f where
  fmap :: (a -> b) -> f a -> f b
  -- fmap id = id
  -- fmap (g . f) = fmap g . fmap f

Contravariant functors reverse morphism direction:

class Contravariant f where
  contramap :: (b -> a) -> f a -> f b

Example: Predicate a = a -> Bool is contravariant. Given f : B -> A, contramap f (p : A -> Bool) = p . f : B -> Bool.

Bifunctors: Functors of two arguments. Either and (,) are bifunctors (covariant in both arguments). (->) is a profunctor (contravariant in the first, covariant in the second).

Natural Transformations

A natural transformation alpha : F => G between functors F, G : C -> D is a family of morphisms alpha_A : F(A) -> G(A) indexed by objects A in C, satisfying naturality:

For every f : A -> B: alpha_B . F(f) = G(f) . alpha_A

Examples in programming:

• head : [a] -> Maybe a is a natural transformation from List to Maybe
• return : a -> m a is a natural transformation from Id to m
• reverse : [a] -> [a] is a natural transformation from List to List
• Parametric polymorphism = natural transformations (by parametricity)

Functor categories: [C, D] has functors C -> D as objects and natural transformations as morphisms. This is again a category.

The Yoneda Lemma

Yoneda Lemma: For a functor F : C^{op} -> Set and an object A in C:

Nat(Hom(-, A), F) ≅ F(A)

Natural transformations from the representable functor Hom(-, A) to F are in bijection with elements of F(A).

Corollary (Yoneda embedding): The functor y : C -> [C^{op}, Set] defined by y(A) = Hom(-, A) is fully faithful. Objects are determined (up to isomorphism) by their morphisms.

Computational Reading

In type theory, Yoneda says: for any type constructor F, a polymorphic function forall b. (a -> b) -> F b is equivalent to F a. The isomorphism is:

• Forward: Given alpha : forall b. (a -> b) -> F b, apply it to id to get alpha id : F a
• Backward: Given x : F a, define alpha f = fmap f x

This is the continuation-passing transform for functors. It appears in:

• CPS encoding of data types
• The codensity monad (performance optimization)
• Lens definitions (van Laarhoven lenses)

Adjunctions

An adjunction L -| R (L left adjoint to R) between functors L : C -> D and R : D -> C is a natural bijection:

Hom_D(L(A), B) ≅ Hom_C(A, R(B))

with natural transformations:

• Unit: eta : Id_C => R . L (eta_A : A -> R(L(A)))
• Counit: epsilon : L . R => Id_D (epsilon_B : L(R(B)) -> B)

satisfying the triangle identities:

• epsilon_{L(A)} . L(eta_A) = id_{L(A)}
• R(epsilon_B) . eta_{R(B)} = id_{R(B)}

Adjunctions in CS

Key theorem: Every adjunction gives rise to a monad R . L with unit eta and multiplication R(epsilon_{L}).

Monads Categorically

A monad on category C is a triple (T, eta, mu) where:

• T : C -> C is an endofunctor
• eta : Id => T (unit)
• mu : T . T => T (multiplication / join)

satisfying:

• mu . T(mu) = mu . mu_T (associativity)
• mu . eta_T = id = mu . T(eta) (unit laws)

Kleisli Category

The Kleisli category C_T has:

• Objects: Same as C
• Morphisms A -> B in C_T: Morphisms A -> T(B) in C (Kleisli arrows)
• Composition: g <=< f = mu . T(g) . f (Kleisli composition, >=> in Haskell)

The Kleisli category models "effectful functions." Haskell's >>= is composition in the Kleisli category: m >>= f = join (fmap f m).

Eilenberg-Moore Category

The Eilenberg-Moore category C^T (the category of T-algebras) has:

• Objects: T-algebras (A, h : T(A) -> A) satisfying h . eta = id and h . T(h) = h . mu
• Morphisms: Homomorphisms of algebras

Examples:

• Algebras for the list monad = monoids
• Algebras for the powerset monad = complete join-semilattices
• Algebras for the free group monad = groups

Theorem (Beck's monadicity theorem): A functor U : D -> C is monadic (D is equivalent to C^T for some monad T) iff U has a left adjoint and U creates coequalizers of U-split pairs.

F-Algebras and Coalgebras

An F-algebra for a functor F : C -> C is a pair (A, alpha : F(A) -> A).

The initial F-algebra (mu F, in : F(mu F) -> mu F) satisfies Lambek's lemma: in is an isomorphism. Initial algebras model inductive data types.

Example: F(X) = 1 + X. Initial algebra is Nat with in = [zero, succ] : 1 + Nat -> Nat.

Catamorphism (fold): For any F-algebra (B, phi : F(B) -> B), there is a unique morphism cata(phi) : mu F -> B such that cata(phi) . in = phi . F(cata(phi)).

cata(phi) = phi . F(cata(phi)) . in^{-1}

In Haskell: foldr :: (a -> b -> b) -> b -> [a] -> b is the catamorphism for lists.

F-Coalgebras

An F-coalgebra is (A, alpha : A -> F(A)). The terminal coalgebra (nu F, out : nu F -> F(nu F)) models coinductive data (streams, infinite trees, processes).

Anamorphism (unfold): For any coalgebra (A, psi : A -> F(A)), there is a unique morphism ana(psi) : A -> nu F.

unfoldr :: (b -> Maybe (a, b)) -> b -> [a]  -- anamorphism for lists

Hylomorphism: Composition of anamorphism followed by catamorphism: hylo phi psi = cata(phi) . ana(psi). Computes by first unfolding then folding -- but can be fused (deforested) into a single recursive function.

Recursion Schemes Summary

Topos Theory

A topos is a category that behaves like a generalized universe of sets. An elementary topos is a category with:

1. Finite limits (including terminal object and pullbacks)
2. Exponentials (internal function spaces)
3. A subobject classifier Omega: an object with a morphism true : 1 -> Omega such that every monomorphism (subobject) is a pullback of true

Key properties:

• Every topos has an internal logic (intuitionistic higher-order logic)
• Set is a topos (Omega = {true, false}, giving classical logic)
• Presheaf categories [C^{op}, Set] are topoi
• Sheaf categories Sh(X) over a topological space X are topoi

Topoi in CS

• Presheaf models: Semantics for modal and temporal logics, Kripke semantics
• Realizability topoi: Models of constructive mathematics (effective topos)
• Synthetic domain theory: Topoi where all functions are computable

Profunctors

A profunctor P : C -|-> D is a functor P : D^{op} x C -> Set. Profunctors generalize relations between categories (as opposed to functors, which generalize functions).

Composition of profunctors uses coends: (Q . P)(C, E) = integral^D P(C, D) x Q(D, E).

Profunctors model bidirectional data access patterns and are the theoretical foundation of optics.

Optics

Optics are bidirectional data accessors, unified through profunctor representation.

Lenses

A lens accesses a part S of a whole A:

Lens s t a b = forall p. Strong p => p a b -> p s t   (profunctor representation)
-- equivalently:
Lens' s a = (get : s -> a, set : a -> s -> s)

Laws: GetPut (set (get s) s = s), PutGet (get (set a s) = a), PutPut (set a (set a' s) = set a s).

Prisms

A prism accesses one variant of a sum type:

Prism s t a b = forall p. Choice p => p a b -> p s t
-- equivalently:
Prism' s a = (match : s -> Either s a, build : a -> s)

Other Optics

Unified Optic Framework

All optics can be expressed as:

Optic c s t a b = forall p. c p => p a b -> p s t

where c is a constraint on the profunctor p. Optics compose via ordinary function composition, and the resulting constraint is the intersection (conjunction) of the component constraints.

Categorical formulation: An optic from (S, T) to (A, B) in a monoidal category is an element of the coend integral^M Hom(S, M tensor A) x Hom(M tensor B, T). Different choices of monoidal structure give different optic families.

Summary of Correspondences