Category Theory in Computing
Table of Contents
1. Introduction
Category theory provides a unifying mathematical framework for understanding computation, types, and program structure through objects, morphisms, and their compositions (Lane 1971).
2. Fundamental Structures
2.1. Categories, Functors, Natural Transformations
Checked against Mac Lane's own table of contents (Categories for the Working Mathematician, 2nd ed., Springer). Category, Functor, and Natural Transformation are a single chapter -- Chapter I, "Categories, Functors, and Natural Transformations" -- not "ch. 1-2" as the prior note had it. Monad, the diagram's fourth node, is not adjacent: it is Chapter VI, "Monads and Algebras," reached only after Chapters II-V (constructions on categories, universals and limits, adjoints, limits). The diagram's "special case" edge from Natural Transformation to Monad is conceptually sound (a monad is a monoid in the category of endofunctors, itself built from natural transformations) but should not be read as citing the same early chapter.
2.2. Commutative Diagrams
Graphviz diagram structure is standard. Natural transformation commutative square is textbook.
3. Monad Structure
Monad laws (left identity, right identity, associativity) correctly stated in the diagram. Standard formulation following Moggi (1991) and Wadler (1992).
4. Categorical Patterns in Programming
4.1. The Expression Problem
Fetched Wadler's original text directly (homepages.inf.ed.ac.uk/wadler/papers/expression/expression.txt): dated 12 November 1998, sent to the java-genericity mailing list, defining the problem as adding both new data variants and new operations to a datatype "without recompiling existing code, and while retaining static type safety." Matches this diagram's two extension axes (New Type?, New Op?) exactly. The coproduct-based solution this section gestures toward is Swierstra (2008); see the free-monads heading below for that verification.
4.2. Free Monads and Interpreters
Swierstra, "Data Types à la Carte" (JFP 18(4), 2008): represents recursive data types as fixed points of functors and combines functorial signatures with coproducts -- the same "lift" from DSL operations into a free-monad program this diagram shows -- and the paper's own abstract names combining free monads to structure Haskell's IO monad as a direct application. Kiselyov and Ishii, "Freer Monads, More Extensible Effects" (Haskell Symposium 2015), per the paper's own abstract: free monads to extensible effects to freer monads, dropping the Functor constraint Swierstra's construction still carries. The diagram's three-interpreter fan-out (production/testing/logging run over one free-monad program) is the standard free-monad interpreter pattern both papers build on.
5. Strange Loops and Self-Reference
The connection between Hofstadter's strange loops and categorical fixed points is real but the prose overstates it. Lawvere's fixed-point theorem (1969) is the formal version; Hofstadter is the popularization. The section should distinguish the two.
6. Implementation in Scheme
6.1. Category as Record
(use-modules (srfi srfi-9))
(define-record-type <category>
(make-category objects morphisms compose identity)
category?
(objects category-objects)
(morphisms category-morphisms)
(compose category-compose)
(identity category-identity))
(define-record-type <functor>
(make-functor source target fmap)
functor?
(source functor-source)
(target functor-target)
(fmap functor-fmap))
(define (functor-map F f)
"Apply functor F to morphism f"
((functor-fmap F) f))
6.2. Verification Pattern
7. Applications
The prior :REVIEW: note said this list had no citations; [cite:@lambek1986] and [cite:@plotkin2003] were already inline below -- that complaint was stale. Plotkin and Power, "Algebraic Operations and Generic Effects" (Applied Categorical Structures 11, 2003), per the paper's own abstract, defines algebraic operations and generic effects for the computational Lambda Calculus and proves the two notions equivalent -- squarely supports "effect systems and algebraic effects." Lambek and Scott's "Introduction to Higher Order Categorical Logic" establishes the Curry-Howard-Lambek correspondence between simply-typed Lambda Calculus and cartesian closed categories; that is the right citation for "type systems as adjunction," but the book does not treat Hindley-Milner's let-polymorphism by name -- that is a later extension past simply-typed Lambda Calculus. Reworded the bullet to match what the citation actually establishes.
- Type systems (simply-typed Lambda Calculus as adjunction) (Lambek and Scott 1986)
- Functional reactive programming
- Database query optimization
- Concurrent and distributed systems
- Effect systems and algebraic effects (Plotkin and Power 2003)
8. References
9. Related
- Trust Boundaries as a Typed Category: An Open Problem – an open problem stated as a typed category
- Reversible Pipeline Transforms – encode/decode pairs and their type-theory lineage
- Lambda Calculus Implementation in Scheme – the Church encodings underneath, in Scheme