Category Theory in Computer Science

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)}

| Left Adjoint L | Right Adjoint R | Relationship | |---|---|---| | Free functor (free monoid) | Forgetful functor | Free structures | | A x - (product) | A -> - (exponential) | Currying | | Sigma (dependent sum) | Pi (dependent product) | Dependent types | | Existential quantifier | Universal quantifier | Quantifiers | | Left Kan extension | Restriction | Kan extensions | | Suspension | Loop space | Homotopy theory |

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

| Scheme | Type | Description | |---|---|---| | Catamorphism (cata) | mu F -> A | Fold (structural recursion) | | Anamorphism (ana) | A -> nu F | Unfold (corecursion) | | Hylomorphism (hylo) | A -> B | Unfold then fold | | Paramorphism (para) | mu F -> A | Fold with access to subterms | | Apomorphism (apo) | A -> nu F | Unfold with early termination | | Histomorphism (histo) | mu F -> A | Fold with access to history | | Futumorphism (futu) | A -> nu F | Unfold with lookahead |

Topos Theory

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

Finite limits (including terminal object and pullbacks)
Exponentials (internal function spaces)
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

| Optic | Access Pattern | Profunctor Constraint | |---|---|---| | Lens | Part of a product | Strong | | Prism | Variant of a sum | Choice | | Affine | Optional part | Strong + Choice | | Traversal | Multiple parts | Wander | | Iso | Isomorphic transformation | Profunctor (unconstrained) | | Grate | Represented functor | Closed |

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

| Category Theory | Type Theory | Programming | |---|---|---| | Object | Type | Data type | | Morphism | Term/function | Function | | Functor | Type constructor | Functor typeclass | | Natural transformation | Polymorphic function | Parametric polymorphism | | Initial algebra | Inductive type | ADT | | Terminal coalgebra | Coinductive type | Stream/process | | Monad | Computation type | Monad typeclass | | Adjunction | Introduction/elimination | Constructor/pattern match | | Yoneda | CPS transform | Codensity/optimization | | Kan extension | Universal property | Left/right extension |