Category Theory for Programming Language Semantics
This page formalizes category theory concepts for programming language semantics, supporting denotational semantics for languages like Haskell. It covers definitions, theorems, proofs, and examples, with links to implementations in src/CategoryBasics.hs and exercises in exercises/Exercises.md.
Introduction to Category Theory
Category theory provides a unifying language for modeling computational structures. In programming, a category abstracts types and functions, enabling formal semantics for languages like Haskell. The category Hask has Haskell types as objects (e.g., Int, Bool) and functions as morphisms (e.g., length :: String -> Int), with composition defined by function composition.
This document aligns with the goals of Category Theory in Programming Language Semantics:
- Goal (a): Give categorical semantics to programming languages and features.
- Goal (b): Perform basic proofs in category theory.
- Goal (c): Enable further exploration of advanced applications.
- Goal (d): Explain denotational semantics concepts.
Categories
A category \(\mathcal{C}\) consists of:
- A collection of objects (e.g., types in a programming language).
- For each pair of objects \(A, B \in \mathcal{C}\), a set of morphisms \(\text{Hom}_{\mathcal{C}}(A, B)\) (e.g., functions \(A \to B\)).
- Composition \(\circ: \text{Hom}_{\mathcal{C}}(B, C) \times \text{Hom}_{\mathcal{C}}(A, B) \to \text{Hom}_{\mathcal{C}}(A, C)\).
- For each object \(A\), an identity morphism \(\text{id}_A \in \text{Hom}_{\mathcal{C}}(A, A)\).
These satisfy:
- Associativity: For \(f: A \to B\), \(g: B \to C\), \(h: C \to D\), \((h \circ g) \circ f = h \circ (g \circ f)\).
- Identity: For \(f: A \to B\), \(f \circ \text{id}_A = f = \text{id}_B \circ f\).
Example
In Hask, objects are Haskell types (e.g., Int, Bool), and morphisms are functions (e.g., length :: String -> Int). Composition is function composition, e.g., (length . show) :: Int -> Int.
Relevance:
- Goal (a): Categories model programming language structure, enabling semantic definitions.
- Goal (b): Programs are interpreted as morphisms in denotational semantics.
Functors
A functor \(F: \mathcal{C} \to \mathcal{D}\) maps:
- Objects: \(A \in \mathcal{C} \mapsto F(A) \in \mathcal{D}\).
- Morphisms: \(f: A \to B \mapsto F(f): F(A) \to F(B)\).
Satisfying:
- Identity: \(F(\text{id}_A) = \text{id}_{F(A)}\).
- Composition: \(F(g \circ f) = F(g) \circ F(f)\).
Example
The Maybe functor in Hask maps a type A to Maybe A and a function f :: A -> B to:
fmap f :: Maybe A -> Maybe B
fmap f Nothing = Nothing
fmap f (Just x) = Just (f x)
Theorem: Functor Laws
For a functor \(F: \mathcal{C} \to \mathcal{D}\):
- \(F(\text{id}_A) = \text{id}_{F(A)}\).
- \(F(g \circ f) = F(g) \circ F(f)\).
Proof
Identity: By functor definition, \(F\) preserves identities, so \(F(\text{id}_A) = \text{id}_{F(A)}\).
Composition: For \(f: A \to B\), \(g: B \to C\), functoriality ensures \(F(g \circ f) = F(g) \circ F(f)\).
Relevance:
- Goal (a): Functors model type constructors for data transformations.
- Goal (b): Proofs verify functor properties.
- Goal (c): Supports denotational semantics for functional transformations.
See src/CategoryBasics.hs for Maybe and List functor implementations.
Natural Transformations
A natural transformation \(\eta: F \to G\) between functors \(F, G: \mathcal{C} \to \mathcal{D}\) is a family of morphisms \(\eta_A: F(A) \to G(A)\) for each \(A \in \mathcal{C}\), such that for any \(f: A \to B\), the following diagram commutes:
i.e., \(\eta_B \circ F(f) = G(f) \circ \eta_A\).
Example
In Hask, listToMaybe :: [a] -> Maybe a is a natural transformation from the List functor to the Maybe functor:
listToMaybe [] = Nothing
listToMaybe (x:_) = Just x
Proof of Naturality
For listToMaybe, verify:
fmap f (listToMaybe xs) == listToMaybe (fmap f xs)
Left: fmap f (listToMaybe []) = fmap f Nothing = Nothing.
Right: listToMaybe (fmap f []) = listToMaybe [] = Nothing.
For x:xs, both yield Just (f x).
Relevance:
- Goal (a): Models polymorphic transformations in semantics.
- Goal (b): Naturality proofs build rigor.
- Goal (c): Ensures type-consistent program transformations.
Monads
A monad on a category \(\mathcal{C}\) is a functor \(T: \mathcal{C} \to \mathcal{C}\) with natural transformations:
- Unit: \(\eta: \text{Id} \to T\).
- Multiplication: \(\mu: T \circ T \to T\).
Satisfying:
- Left unit: \(\mu \circ T\eta = \text{id}_T\).
- Right unit: \(\mu \circ \eta T = \text{id}_T\).
- Associativity: \(\mu \circ T\mu = \mu \circ \mu T\).
Example
The State monad in Hask models stateful computations:
return x = \s -> (x, s)
(m >>= k) s = let (a, s') = m s in k a s'
Theorem: Left Unit Law
For a monad \((T, \eta, \mu)\), \(\mu \circ T\eta = \text{id}_T\).
Proof
For an object \(A \in \mathcal{C}\), we need \(\mu_A \circ T(\eta_A) = \text{id}_{TA}\). The commutative diagram is:
By the monad’s unit axiom, \(\mu_A \circ T(\eta_A) = \text{id}_{TA}\). In Haskell, for State, return and >>= satisfy this law.
Relevance:
- Goal (a): Monads model effects (e.g., state, I/O) in programming languages.
- Goal (b): Proofs verify monad properties.
- Goal (c): Explains denotational semantics for effectful computations.
See src/CategoryBasics.hs for State monad implementation.
Cartesian Closed Categories
A category \(\mathcal{C}\) is Cartesian closed if it has:
- A terminal object \(1\), with a unique morphism \(!: A \to 1\) for any \(A\).
- Binary products \(A \times B\), with projections \(\pi_1: A \times B \to A\), \(\pi_2: A \times B \to B\).
- Exponential objects \(B^A\), with evaluation \(\text{ev}: B^A \times A \to B\) and currying \(\lambda(f): C \to B^A\) for any \(f: C \times A \to B\).
Example
In Hask, the terminal object is (), products are tuples (A, B), and exponentials are function types A -> B.
Relevance:
- Goal (a): Models typed lambda calculus for functional languages.
- Goal (b): Explains semantics via currying and evaluation.
Yoneda Lemma
Theorem: Yoneda Lemma
For a category \(\mathcal{C}\), object \(A\), and functor \(F: \mathcal{C} \to \mathbf{Set}\), there is a bijection:
\[ \text{Nat}(\text{Hom}_{\mathcal{C}}(A, -), F) \cong F(A). \]Proof
Define \(\phi: \text{Nat}(\text{Hom}_{\mathcal{C}}(A, -), F) \to F(A)\) by \(\phi(\eta) = \eta_A(\text{id}_A)\). The inverse maps \(x \in F(A)\) to \(\eta_B(f) = F(f)(x)\) for \(f: A \to B\). Naturality ensures the bijection.
Relevance:
- Goal (a): Enables exploration of advanced type system semantics.
- Goal (b): Provides a theoretical tool for denotational semantics.