English
A category is a collection of objects and arrows between them, with a rule for composing arrows and an identity arrow at each object. That description is so abstract as to seem empty — until you notice how many things it describes. Sets with functions. Groups with homomorphisms. Types with programs. Topological spaces with continuous maps. Logical propositions with proofs. The abstraction is the point: category theory studies what all of these have in common, and the common structure turns out to be rich enough to say important things about each.
For computer science, the key concept is the functor — a map between categories that preserves structure. Lists are a functor: there is a map from types to list-types, and every function between types lifts to a function between lists of those types, in a way that respects composition. This captures something real about what lists are that no definition focused on the list data structure alone can express. The monads that structure effectful computation in Haskell are functors with additional algebraic structure. The type constructors of generic programming are functors. The semantics of programming languages is a functor from syntax categories to denotation categories. Category theory did not invent these structures — they existed in scattered form across mathematics and CS — but it gave them a common name and a common theory.
The subject is genuinely specialized within this guide. It rewards practitioners who work in programming language theory (§3.4), type theory (§3.5), formal methods (§3.6), or at the mathematical frontier of computer science. For practitioners whose work is primarily empirical or systems-oriented, the investment required to develop category theory fluency is unlikely to be justified in the short term, though the conceptual vocabulary it provides has long-term value. The section below is written for readers who have decided the investment is warranted.
Prerequisites: Mathematical maturity — comfort with abstract algebra (groups, rings, homomorphisms) and with the style of mathematical proof in §2.2. Programming language theory (§3.4) provides CS grounding for the applications, but category theory can be approached from the mathematical side without it.
How the Language of Structure Was Invented
Category theory was invented to solve a specific problem in algebraic topology and turned out to solve far more than that.
In the early 1940s, Samuel Eilenberg and Saunders Mac Lane were working on the relationship between the homology groups of a topological space. They kept encountering transformations between groups that were, in an intuitive sense, “natural” — not dependent on arbitrary choices made in the construction — but they had no precise way to say this. To state the theorem they wanted to prove, they had to invent the language that could express it. Their 1945 paper “General Theory of Natural Equivalences” introduced categories, functors, and natural transformations all at once, specifically to capture the notion of naturality. The paper’s opening was candid about the motivation: the concepts were introduced for the purpose of expressing a mathematical result that could not be stated otherwise. The abstract formalism was a means to a concrete end.
What Eilenberg and Mac Lane did not anticipate was that the formalism they created would turn out to organize large portions of mathematics. Through the 1950s and 1960s, mathematicians across different fields — Alexander Grothendieck in algebraic geometry, William Lawvere in foundations of mathematics, Peter Freyd in homological algebra — found that categorical concepts were exactly the right tool for their problems. Grothendieck’s 1957 Tôhoku paper, which reformulated homological algebra in categorical terms, demonstrated that categorical language could clarify and generalize results that had previously been stated with great difficulty. Lawvere’s 1963 doctoral thesis, “Functorial Semantics of Algebraic Theories,” showed that algebraic structures like groups and rings could be characterized as functors from a small category of operations, giving a unified framework for all of universal algebra. Mac Lane’s observation that adjoint functors were everywhere — that the free-group construction was the left adjoint of a forgetful functor, that tensor products were left adjoints of hom-sets, that many other constructions in mathematics fit the same pattern — established adjunctions as one of the organizing concepts of mathematics. Mac Lane’s Categories for the Working Mathematician, published in 1971, organized this material into the canonical reference.
The connection to computer science came through logic and type theory. Joachim Lambek noticed in 1969 that the typed lambda calculus corresponded precisely to a certain kind of category — a Cartesian closed category — with types as objects and terms as morphisms. This observation connected Church’s lambda calculus, the foundation of functional programming, to the categorical framework that had been developed for algebra and topology. Dana Scott’s domain-theoretic semantics of the lambda calculus, developed in the early 1970s, provided a categorical model — Scott-continuous functions on domains — that gave denotational semantics a category-theoretic foundation. These connections established that category theory was not just a language for mathematics but a language for computation.
Through the 1970s and 1980s, these connections deepened. Lawvere and Tierney’s work on elementary toposes showed that a topos — a category with certain structure — was simultaneously a generalization of the category of sets and an interpretation of intuitionistic logic. Every topos provided a model of intuitionistic higher-order logic; every model of intuitionistic higher-order logic defined a topos. This Lawvere-Tierney correspondence joined the long list of connections between logic and category theory that were reshaping both subjects. Lambek and Scott’s 1986 book Introduction to Higher-Order Categorical Logic consolidated these connections into a systematic framework showing that Cartesian closed categories, the simply typed lambda calculus, and intuitionistic propositional logic were three presentations of the same mathematical structure.
The development that most directly affected programming practice was Eugenio Moggi’s 1991 paper “Notions of Computation and Monads.” Moggi observed that various computational effects — state, exceptions, nondeterminism, continuations, I/O — could all be uniformly modeled as monads: endofunctors with a unit and a multiplication satisfying specific laws. This was not an observation about Haskell (which did not yet use monads for effects) but about the categorical structure of effects in programming language semantics. Philip Wadler recognized the practical significance and, in his 1992 paper “Monads for Functional Programming,” translated Moggi’s categorical framework into a direct programming technique. Haskell adopted monads for IO and the broader effect structure, and the concept spread across functional programming. Today, any Haskell programmer who writes IO, Maybe, or State is using Moggi’s categorical framework, usually without knowing it.
The contemporary period has brought applied category theory as a deliberate program. John Baez, Brendan Fong, David Spivak, and others have developed categorical frameworks for networks, circuits, open systems, databases, and machine learning, arguing that the compositional structure of these domains is precisely what category theory is designed to express. Fong and Spivak’s Seven Sketches in Compositionality (2018, free) organized this program into an accessible text. The Applied Category Theory conference, started in 2018, has become a substantial venue. Whether applied category theory will produce practically significant engineering results at the scale its proponents envision is still being determined — the program is young — but it represents the most deliberate effort to bring categorical thinking to bear on engineering problems since the original connections to programming language semantics.
The deepest contemporary development is the connection between category theory and homotopy type theory. Voevodsky’s univalent foundations program (§3.5) led to the interpretation of type theory in ∞-categories — categories where the morphisms themselves form spaces, morphisms between morphisms form higher-dimensional spaces, and so on through all dimensions. This connection, developed by Riehl, Shulman, Lumsdaine, and others, relates Martin-Löf type theory to the most abstract and general form of category theory, suggesting that type theory and category theory are, at the deepest level, descriptions of the same mathematical reality.
Functors, Adjunctions, and Monads
Categories and Functors: The Basic Vocabulary
A category C consists of a collection of objects, a collection of morphisms f: A → B for each pair of objects A, B, a composition law that takes f: A → B and g: B → C to g ∘ f: A → C, and identity morphisms id_A: A → A, all satisfying associativity of composition and unit laws for identity. The definition is easy to state and takes months to internalize, because the generality means that the same structure appears in radically different guises.
In the category Set, objects are sets and morphisms are functions. In the category Grp, objects are groups and morphisms are group homomorphisms. In the category Hask (an informal but useful fiction), objects are Haskell types and morphisms are Haskell functions. In a preorder category, objects are elements of a preorder and there is exactly one morphism A → B if A ≤ B (and none otherwise). A monoid is a category with exactly one object. Each of these is a category; theorems proved for all categories apply to all of them simultaneously.
A functor F: C → D between categories assigns to each object A in C an object F(A) in D, and to each morphism f: A → B in C a morphism F(f): F(A) → F(B) in D, preserving composition (F(g ∘ f) = F(g) ∘ F(f)) and identity (F(id_A) = id_{F(A)}). This is the categorical notion of “structure-preserving map.” In the programming context, a functor from Hask to Hask is what Haskell’s Functor typeclass describes: a type constructor F with a function fmap :: (a -> b) -> F a -> F b satisfying the functor laws.
Natural transformations are the morphisms between functors. A natural transformation η: F ⇒ G between functors F, G: C → D consists of morphisms η_A: F(A) → G(A) for each object A, satisfying a naturality condition: for every morphism f: A → B, the square G(f) ∘ η_A = η_B ∘ F(f) commutes. Naturality is the precise expression of the intuition that a transformation is “natural” — not dependent on arbitrary choices. The commuting square condition says that the transformation behaves consistently with respect to all morphisms, not just the specific ones one happens to check.
Adjunctions: The Most Important Relationship
An adjunction between functors F: C → D and G: D → C consists of natural bijections D(F(A), B) ≅ C(A, G(B)), expressing that F and G are “inverse” in a weak, hom-set level sense. F is the left adjoint of G; G is the right adjoint of F. Mac Lane famously wrote that “adjoint functors arise everywhere,” and the claim is only slightly overstated.
In programming terms: the free list functor is left adjoint to the forgetful functor from monoids to sets. This single statement encodes the universal property of lists: a function from a set X to a monoid M uniquely extends to a monoid homomorphism from the free monoid on X (i.e., the list type) to M. The free-forgetful adjunction is why list comprehensions and fold functions have the structure they do.
Currying is an adjunction. The bijection (A × B) → C ≅ A → (B → C) is the natural bijection that characterizes the Cartesian closed structure of Hask: the product functor (- × B) is left adjoint to the exponential functor (B → -). This is why currying and uncurrying are inverses, stated precisely.
Limits and colimits are defined by universal properties that can be expressed as adjunctions to diagonal functors. Products are limits of discrete diagrams; coproducts are colimits; equalizers, pullbacks, pushouts, and many other constructions fit the same framework. In type theory, product types and sum types are the type-theoretic versions of categorical products and coproducts; the dependent types of §3.5 generalize these to dependent products (Π-types) and dependent sums (Σ-types), which are again characterized by universal properties.
Monads: Functors with Algebraic Structure
A monad on a category C is a functor T: C → C with natural transformations η: Id ⇒ T (unit) and μ: T² ⇒ T (multiplication) satisfying the monad laws: μ ∘ Tη = id = μ ∘ ηT (unit laws) and μ ∘ Tμ = μ ∘ μT (associativity). The laws make T an algebraic structure — specifically, a monoid in the category of endofunctors under functor composition.
Monads arise as left-right adjunction composites: if F ⊣ G (F is left adjoint to G), then G ∘ F is a monad. The unit of the monad comes from the unit of the adjunction; the multiplication comes from the counit. Every monad arises this way. This is the mathematical explanation for why monads structure effects: each effect type corresponds to an adjunction between the base category and a category of “computations,” and the monad is the resulting composite.
In programming practice: the Maybe monad handles computations that might fail. The State s monad handles computations that read and write a state of type s. The IO monad handles computations that interact with the world. Each is a monad because each corresponds to an adjunction — Maybe to the adjunction between sets and pointed sets, State to the adjunction between sets and sets-over-(s × s), IO to a free monad construction over a signature of IO operations. Knowing this does not make monadic programming easier day-to-day, but it explains why the interface is the way it is and why different monads can be combined using the same algebraic machinery (monad transformers, effect systems).
The Kleisli category of a monad T on C has the same objects as C and morphisms A → B given by morphisms A → T(B) in C. Monad bind (>>= in Haskell) is composition in the Kleisli category. This is the precise statement of why monadic sequencing has the structure it has: it is ordinary composition in a category where morphisms carry computational effects.
What Studying This Changes
Category theory changes how practitioners organize and interpret the structures they work with.
The most immediate change is pattern recognition across structures. After studying category theory, a practitioner who encounters a new type constructor immediately asks: is this a functor? If it maps types to types and functions to functions in a structure-preserving way, it is. Is it a monad? Does it come with a natural way to inject values and a natural way to flatten double applications? These questions, asked systematically, reveal structure that informal understanding misses and establish what operations the type constructor supports.
The second change is the understanding of why certain programming abstractions have the structure they do. Currying is an adjunction. Lists are the free monad of a specific functor. The Traversable typeclass corresponds to a specific categorical structure. The various Haskell typeclasses — Functor, Applicative, Monad, Foldable, Traversable — form a structured hierarchy that reflects the categorical relationships between the structures they name. Understanding the categorical basis means understanding why the hierarchy is what it is rather than experiencing it as an arbitrary design decision.
The third change is access to the categorical literature. Programming language theory and type theory research papers increasingly use categorical vocabulary without defining it. A practitioner fluent in category theory can read this literature; one who is not encounters a vocabulary gap that grows as the research frontier advances.
The fourth change, which takes longest to materialize, is the habit of asking for universal properties. When encountering a new construction — a new data type, a new algebraic structure, a new programming pattern — the category-theoretically trained practitioner asks: is there a universal property that characterizes this? Is this the initial object, the terminal object, the free construction, the coproduct? These questions often have answers, and the answers give the construction its essential properties without case analysis or ad hoc reasoning.
Resources
Books and Texts
Awodey’s Category Theory (2nd ed., Oxford, 2010) is the best starting point for most learners. It requires less mathematical background than Mac Lane, covers the same core concepts, and is more pedagogically generous. The writing is clear, the examples range across mathematics and computer science, and the pace allows the abstractions to settle before the next layer is introduced. Most computer scientists should start here.
Mac Lane’s Categories for the Working Mathematician (2nd ed., Springer, 1978) is the canonical mathematical reference, written for mathematicians and assuming extensive mathematical preparation. It is denser than Awodey, more comprehensive, and more demanding. Learners with strong mathematical backgrounds may prefer to start here; others should use Awodey first and return to Mac Lane when a more complete treatment of a specific topic is needed.
Milewski’s Category Theory for Programmers (free online and as a print compilation, also on YouTube) develops category theory through Haskell examples. It is the most accessible entry for programmers with no prior mathematical background and is the right choice for learners who are intimidated by mathematical treatments. The limitation is that the mathematical content is lighter than Awodey or Mac Lane; Milewski is the entry, not the destination.
Pierce’s Basic Category Theory for Computer Scientists (MIT Press, 1991) is brief, old, and still the best short CS-oriented introduction. Its compactness makes it appropriate as a first encounter or as a review, and the CS focus means the examples are immediately relevant. The 1991 date means it predates much of the applied category theory work, but the core material is permanent.
Barr and Wells’s Category Theory for Computing Science (free online, 3rd ed.) covers the same core material as Awodey with heavier CS emphasis. It is more comprehensive than Pierce for CS applications, covering algebraic automata theory, categorical semantics of programming languages, and other CS-specific topics that Awodey treats only briefly. The combination of Awodey (for mathematical foundations and clarity) and Barr-Wells (for CS applications) is more effective than either alone.
Riehl’s Category Theory in Context (Dover, 2016, free at math.jhu.edu/~eriehl/context.pdf) is a graduate-level mathematical treatment that is nevertheless clearly written and accessible to motivated readers who have completed Awodey. It covers representability, limits and colimits, adjunctions, and monads with fuller treatment than Awodey, and it bridges the gap between Awodey-level mathematics and the contemporary research literature.
For applied category theory, Fong and Spivak’s Seven Sketches in Compositionality (free at arxiv.org/abs/1803.05316) is the entry. It covers preorders, resource theories, databases, co-design, signal flow graphs, and electrical circuits — all from a categorical perspective — at a level accessible to non-mathematicians. It is the right text for learners interested in applying category theory to engineering and scientific domains.
For categorical logic and programming language semantics, Lambek and Scott’s Introduction to Higher-Order Categorical Logic (Cambridge, 1986) is the canonical reference. It develops the correspondence between Cartesian closed categories, the typed lambda calculus, and intuitionistic logic, and is essential for understanding why PLT and category theory are so deeply connected.
| Book | Role | Type |
|---|---|---|
| Awodey, Category Theory (2nd ed.) | Standard accessible entry | Entry |
| Mac Lane, Categories for the Working Mathematician (2nd ed.) | Canonical mathematical reference | Reference |
| Milewski, Category Theory for Programmers (free) | Programmer-oriented introduction | Entry |
| Pierce, Basic Category Theory for Computer Scientists | Brief CS-oriented entry | Entry |
| Barr & Wells, Category Theory for Computing Science (free) | Comprehensive CS-oriented text | Depth |
| Riehl, Category Theory in Context (free) | Graduate-level treatment | Depth |
| Fong & Spivak, Seven Sketches in Compositionality (free) | Applied category theory entry | Entry |
| Lambek & Scott, Introduction to Higher-Order Categorical Logic | Categorical logic and PLT | Depth |
| Mac Lane & Moerdijk, Sheaves in Geometry and Logic | Topos theory beyond the CS learning path | Auxiliary |
Courses and Lectures
Milewski’s Category Theory for Programmers YouTube series (free) accompanies his book and is the most accessible video introduction available. The lectures develop the material at a pace appropriate for programmers encountering the subject for the first time, with running Haskell examples.
MIT 18.S097 (Category Theory for Machine Learning, free materials when available) represents the emerging connection between category theory and ML research. As materials become available from similar courses, they are worth following.
The Applied Category Theory School (ACT, held annually with accompanying reading groups) produces accessible introductory material aimed at learners outside pure mathematics. ACT reading groups cover Seven Sketches and related texts; the school lectures are available on YouTube.
Emily Riehl’s lectures on category theory at various summer schools (freely available on YouTube) cover the mathematical content of her book at a level accessible to advanced undergraduates. Her treatment of the Yoneda lemma and adjunctions is particularly clear.
The Catsters videos (free on YouTube) are an older but still useful collection of short pedagogical explanations of core category theory concepts. They are not CS-specific, but they often make definitions such as products, coproducts, adjunctions, and natural transformations easier to hear before reading them formally.
The Topos Institute produces talks and seminars on applied category theory, including examples connected to systems, databases, probability, and scientific modeling. The material is uneven in level, but it is a good current-source stream for readers who want to see where applied category theory is being used now.
| Course | Platform | Type |
|---|---|---|
| Milewski, Category Theory for Programmers lectures (free) | YouTube | Entry |
| ACT School lectures (free) | YouTube / ACT site | Entry |
| Emily Riehl lectures on category theory (free) | YouTube | Depth |
| The Catsters category theory videos (free) | YouTube | Auxiliary |
| Topos Institute talks (free) | YouTube / topos.institute | Reference |
Practice, Tools, and Current Sources
The nLab (ncatlab.org) is the essential reference wiki for category theory and its applications. It is uneven — some entries are excellent, others sparse — but it is the most comprehensive online resource for the subject. Use it to look up specific concepts and connections, not as a reading sequence.
Working through the Haskell Functor, Applicative, and Monad typeclasses with explicit attention to the categorical structure — deriving the functor laws, verifying the monad laws for specific instances, implementing the Kleisli composition — builds intuition that reading does not. Implement the State, Maybe, and Reader monads from scratch and verify that they satisfy the monad laws.
The Agda proof assistant can be used to formalize categorical definitions and prove categorical laws, which makes the abstract definitions operational in a way that reading cannot. Category theory formalized in Agda — where a functor is a dependent record type with fields for the object map, the morphism map, and the proofs of functoriality — is the most precise engagement with the definitions available to a programmer.
Catlab.jl (free, Julia package) provides a framework for applied category theory in Julia, with implementations of operads, functors, diagrams, and C-sets. It is the most mature programming environment for applied category theory work.
| Resource | Platform | Type |
|---|---|---|
| nLab (free) | ncatlab.org | Reference |
| Haskell typeclass implementations (functor laws, monad laws) | Local | Practice |
| Agda category theory formalization | Local / agda.readthedocs.io | Practice |
| Catlab.jl (free) | Julia package | Practice |
Traps
| Trap | Why it misleads | Better response |
|---|---|---|
| Treating category theory as “Haskell theory” | The historical accident that Haskell adopted monads, functors, and foldables as first-class programming concepts has produced the impression that category theory is fundamentally about Haskell. Category theory predates Haskell by forty years and applies across mathematics, physics, and all of CS. The Haskell perspective is useful but peripheral. | Study Awodey’s book rather than Milewski’s as the primary text, using Milewski for programming intuition and Awodey for the mathematical substance. The mathematical perspective reveals the generality; the Haskell perspective provides a concrete instantiation that can be run. |
| Engaging with the abstraction without grounding in examples | Category theory is so abstract that it is possible to learn the formal definitions and manipulate them correctly while having no genuine understanding of what they mean. The definitions describe structures that appear in many concrete cases, and without knowing those cases, the abstractions are empty. | For every new categorical concept, identify at least three concrete examples in different domains: one from mathematics (sets, groups, topological spaces), one from programming (types, programs, effects), one from logic (propositions, proofs, inference). The abstractions are only as meaningful as the concrete cases that ground them. |
| Attempting higher category theory before mastering basic category theory | 2-categories, ∞-categories, and the categorical foundations of homotopy type theory are important and advanced. They require solid fluency in ordinary category theory — natural transformations, adjunctions, limits, monads — that typically takes a year or more to develop. Learners who attempt higher categories without this foundation reliably fail to make progress. | Complete Awodey and substantial parts of Riehl before engaging with higher categories. A good test: can you state and explain the Yoneda lemma precisely, including the proof? If not, the basic category theory is not yet solid enough for higher categories. |
| Learning the definitions without doing exercises | Category theory exercises require constructing functors, verifying naturality conditions, computing limits, and constructing adjunctions for specific examples. These constructions develop the categorical intuition that reading cannot. The subject is impossible to learn purely by following exposition. | Work every exercise in the primary text. The exercises in Awodey are not optional elaborations; they are the primary site where the learning happens. Checking that a proposed functor actually satisfies the functoriality laws, for a dozen different examples, builds an intuition that reading twenty explanations does not. |
| Treating monads as the destination rather than one concept | Monads are the categorical concept that programming has adopted most visibly, and learners often treat acquiring monad intuition as the goal of category theory study. But monads are one construction among many, and the perspective that makes them useful — understanding what algebraic structure functors can carry, what the Kleisli category is, why effects compose the way they do — requires the broader categorical framework. | Treat monads as the first significant CS application, not the final destination. After understanding monads categorically, continue to adjunctions and their relationship to monads, to monoidal categories and profunctors, to categorical semantics. The categorical perspective on monads is most valuable when monads are understood within their broader categorical context. |
| Skipping the Yoneda lemma | The Yoneda lemma — that any functor F: C → Set is naturally isomorphic to the hom-functor Hom(-, A) for some object A — is the most important theorem in basic category theory. It reveals that objects are fully determined by the morphisms into (or out of) them, that abstract categorical structure is faithfully represented by concrete set-valued functors, and that the hom-functor is the bridge between abstract and concrete. Many learners find it mysterious and give it insufficient attention. | Spend at least a week on the Yoneda lemma. Work through the proof line by line. Verify it for three specific cases: sets, groups, and types. Then read Mac Lane’s comment that “Yoneda’s lemma is a consequence of the fact that hom-functors are representable” and explain what this means. The time investment pays dividends throughout all subsequent category theory study. |
中文
范畴是对象以及对象之间箭头的集合，带有一个箭头复合规则，并且每个对象上都有一个恒等箭头。这个描述抽象到几乎像是空的——直到你注意到它描述了多少东西。集合与函数。群与同态。类型与程序。拓扑空间与连续映射。逻辑命题与证明。抽象性正是重点：范畴论研究所有这些结构共有的东西，而这种共同结构足够丰富，可以对每一个领域说出重要内容。
对计算机科学来说，关键概念是函子——一种保持结构的范畴之间的映射。列表是一个函子：存在一个从类型到列表类型的映射，并且每个类型之间的函数都可以提升为这些类型的列表之间的函数，同时尊重复合。这捕捉了关于列表是什么的某种真实内容，而只关注列表数据结构本身的定义无法表达这一点。Haskell 中组织有副作用计算的 monad，就是带有额外代数结构的函子。泛型编程中的类型构造子是函子。编程语言语义是从语法范畴到指称范畴的函子。范畴论并没有发明这些结构——它们早已以分散形式存在于数学和 CS 中——但它给了它们共同名称和共同理论。
在本指南中，这个主题确实很专门。它会奖励那些从事编程语言理论（§3.4）、类型论（§3.5）、形式化方法（§3.6），或计算机科学数学前沿工作的实践者。对于主要从事实证或系统方向工作的实践者，发展范畴论流利度所需投入，在短期内很可能不值得；不过它提供的概念词汇具有长期价值。下面这一节面向已经判断这项投入值得的读者。
前置知识：数学成熟度——熟悉抽象代数（群、环、同态）以及 §2.2 中的数学证明风格。编程语言理论（§3.4）为应用提供 CS grounding，但也可以从数学侧进入范畴论。
结构语言如何被发明
范畴论最初是为了解决代数拓扑中的一个具体问题而发明的，后来却证明它能解决远不止这个问题。
1940 年代初，Samuel Eilenberg 和 Saunders Mac Lane 正在研究拓扑空间的同调群之间的关系。他们不断遇到一些群之间的变换，这些变换在直觉上是“自然的”——不依赖构造过程中作出的任意选择——但他们没有精确方式表达这一点。为了陈述他们想证明的定理，他们必须发明能够表达它的语言。他们 1945 年的论文 “General Theory of Natural Equivalences” 一次性引入了范畴、函子和自然变换，具体目的就是捕捉自然性的概念。论文开头坦率说明了动机：这些概念被引入，是为了表达一个无法用其他方式陈述的数学结果。抽象形式主义只是服务具体目的的手段。
Eilenberg 和 Mac Lane 没有预料到的是，他们创造出的形式系统后来会组织数学的大量部分。1950 年代和 1960 年代，不同领域的数学家——代数几何中的 Alexander Grothendieck、数学基础中的 William Lawvere、同调代数中的 Peter Freyd——发现范畴概念恰好是处理他们问题的正确工具。Grothendieck 1957 年的 Tôhoku 论文用范畴语言重新表述同调代数，展示了范畴语言可以澄清并推广那些此前极难陈述的结果。Lawvere 1963 年的博士论文 “Functorial Semantics of Algebraic Theories” 表明，群和环等代数结构可以被刻画为从一个小型运算范畴出发的函子，从而为整个泛代数提供统一框架。Mac Lane 观察到伴随函子无处不在——自由群构造是遗忘函子的左伴随，张量积是 hom-set 的左伴随，数学中许多其他构造也符合相同模式——这确立了伴随作为数学组织性概念之一的地位。Mac Lane 的 Categories for the Working Mathematician 于 1971 年出版，并把这些材料组织成经典参考。
与计算机科学的连接来自逻辑和类型论。Joachim Lambek 在 1969 年注意到，类型化 λ 演算精确对应一种特定范畴——Cartesian closed category，其中类型作为对象，项作为态射。这一观察把 Church 的 λ 演算，也就是函数式编程的基础，连接到为代数和拓扑发展出的范畴框架。Dana Scott 在 1970 年代初发展出的 λ 演算 domain-theoretic 语义提供了一个范畴模型——定义在 domain 上的 Scott-continuous 函数——这为指称语义提供了范畴论基础。这些连接确立了：范畴论不只是数学语言，也是计算语言。
1970 年代和 1980 年代，这些连接继续加深。Lawvere 和 Tierney 关于 elementary topos 的工作表明，topos——一种具有特定结构的范畴——同时是集合范畴的推广，以及直觉主义逻辑的一种解释。每个 topos 都提供一个直觉主义高阶逻辑模型；每个直觉主义高阶逻辑模型也定义一个 topos。这个 Lawvere-Tierney 对应加入了逻辑与范畴论之间的长串联系，并重塑了这两个主题。Lambek 和 Scott 1986 年的书 Introduction to Higher-Order Categorical Logic 把这些连接整合成系统框架，表明 Cartesian closed categories、简单类型 λ 演算和直觉主义命题逻辑，是同一数学结构的三种呈现。
最直接影响编程实践的发展，是 Eugenio Moggi 1991 年的论文 “Notions of Computation and Monads”。Moggi 观察到，各种计算效应——状态、异常、非确定性、continuations、I/O——都可以统一建模为 monad：带有 unit 和 multiplication、并满足特定律的自函子。这不是关于 Haskell 的观察，当时 Haskell 还没有使用 monad 处理效应；它是关于编程语言语义中效应的范畴结构的观察。Philip Wadler 认识到了其实践意义，并在 1992 年的论文 “Monads for Functional Programming” 中，把 Moggi 的范畴框架翻译成直接的编程技术。Haskell 采用 monad 处理 IO 和更广泛的效应结构，这一概念随后在函数式编程中传播开来。今天，任何写 IO、Maybe 或 State 的 Haskell 程序员，通常是在不知情的情况下使用 Moggi 的范畴框架。
当代时期带来了有意识作为纲领的应用范畴论。John Baez、Brendan Fong、David Spivak 等人发展了面向网络、电路、开放系统、数据库和机器学习的范畴框架，并主张这些领域的组合结构正是范畴论被设计用来表达的东西。Fong 和 Spivak 的 Seven Sketches in Compositionality（2018，免费）把这一纲领组织成一本可读文本。Applied Category Theory conference 于 2018 年开始举办，并已成为一个重要场所。应用范畴论是否会在其倡导者设想的尺度上产生具有实践意义的工程结果，目前仍在观察中——这个纲领还年轻——但它代表了自范畴论最初连接到编程语言语义以来，最有意识地把范畴思维应用于工程问题的一次努力。
最深的当代发展，是范畴论与同伦类型论之间的连接。Voevodsky 的单价基础纲领（§3.5）通向了在 ∞-categories 中解释类型论——在这种范畴中，态射本身形成空间，态射之间的态射形成更高维空间，如此延展到所有维度。这一连接由 Riehl、Shulman、Lumsdaine 等人发展，把 Martin-Löf 类型论与最抽象、最一般形式的范畴论联系起来，并暗示类型论和范畴论在最深层上是同一数学现实的两种描述。
函子、伴随与 Monads
范畴与函子：基本词汇
一个范畴 C 由一组对象、每对对象 A 和 B 之间的一组态射 f: A → B、一个复合律，以及每个对象上的恒等态射组成。复合律把 f: A → B 和 g: B → C 送到 g ∘ f: A → C；恒等态射为 id_A: A → A；所有这些满足复合结合律和恒等元律。这个定义很容易陈述，却需要数月才能内化，因为它的一般性意味着同一结构会以极其不同的面貌出现。
在范畴 Set 中，对象是集合，态射是函数。在范畴 Grp 中，对象是群，态射是群同态。在范畴 Hask 中——这是一个非形式但有用的虚构——对象是 Haskell 类型，态射是 Haskell 函数。在预序范畴中，对象是预序中的元素；当且仅当 A ≤ B 时，恰好存在一个态射 A → B，否则不存在。一个幺半群就是恰好只有一个对象的范畴。这些都是范畴；为所有范畴证明的定理，会同时适用于它们全部。
范畴之间的函子 F: C → D 会把 C 中每个对象 A 指派到 D 中的对象 F(A)，并把 C 中每个态射 f: A → B 指派到 D 中的态射 F(f): F(A) → F(B)，同时保持复合（F(g ∘ f) = F(g) ∘ F(f)）和恒等（F(id_A) = id_{F(A)}）。这就是范畴论中的“保持结构的映射”。在编程语境中，从 Hask 到 Hask 的函子，就是 Haskell 的 Functor typeclass 所描述的东西：一个类型构造子 F，以及一个函数 fmap :: (a -> b) -> F a -> F b，并满足函子律。
自然变换是函子之间的态射。函子 F, G: C → D 之间的自然变换 η: F ⇒ G，由每个对象 A 上的态射 η_A: F(A) → G(A) 构成，并满足自然性条件：对于每个态射 f: A → B，方块 G(f) ∘ η_A = η_B ∘ F(f) 可交换。自然性精确表达了这样一种直觉：一个变换是“自然的”——不依赖任意选择。可交换方块条件说的是，这个变换相对于所有态射都表现一致，而不只是相对于人们恰好检查的那些态射一致。
伴随：最重要的关系
函子 F: C → D 和 G: D → C 之间的伴随，由自然双射 D(F(A), B) ≅ C(A, G(B)) 构成，表达的是 F 和 G 在较弱的、hom-set 层面上是“逆”的。F 是 G 的左伴随；G 是 F 的右伴随。Mac Lane 著名地写道，“伴随函子无处不在”，这个说法只是稍微夸张。
用编程语言来说：自由列表函子是从幺半群到集合的遗忘函子的左伴随。这个单一句子编码了列表的泛性质：从集合 X 到幺半群 M 的函数，可以唯一扩展为从 X 上的自由幺半群，也就是列表类型，到 M 的幺半群同态。自由—遗忘伴随解释了为什么 list comprehensions 和 fold 函数具有它们现在的结构。
柯里化是一个伴随。双射 (A × B) → C ≅ A → (B → C) 是刻画 Hask 的 Cartesian closed 结构的自然双射：积函子 (- × B) 是指数函子 (B → -) 的左伴随。这精确说明了为什么 currying 和 uncurrying 互为逆。
极限和余极限由泛性质定义，而这些泛性质可以表达为到对角函子的伴随。积是离散图式的极限；余积是余极限；等化子、拉回、推出以及许多其他构造都符合相同框架。在类型论中，积类型和和类型是范畴论中积与余积的类型论版本；§3.5 的依赖类型把它们推广到依赖积（Π-types）和依赖和（Σ-types），它们同样由泛性质刻画。
Monads：带有代数结构的函子
范畴 C 上的 monad 是一个函子 T: C → C，并配有自然变换 η: Id ⇒ T（unit）和 μ: T² ⇒ T（multiplication），满足 monad 律：μ ∘ Tη = id = μ ∘ ηT（unit laws）以及 μ ∘ Tμ = μ ∘ μT（associativity）。这些律使 T 成为一种代数结构——更具体地说，它是在函子复合下的自函子范畴中的幺半群。
Monad 来自左右伴随的复合：如果 F ⊣ G，也就是 F 是 G 的左伴随，那么 G ∘ F 是一个 monad。Monad 的 unit 来自伴随的 unit；multiplication 来自 counit。每个 monad 都以这种方式出现。这就是为什么 monad 能组织效应的数学解释：每种 effect type 都对应基础范畴和某种“计算”范畴之间的伴随，而 monad 就是所得复合。
在编程实践中：Maybe monad 处理可能失败的计算。State s monad 处理读写类型为 s 的状态的计算。IO monad 处理与世界交互的计算。它们每一个都是 monad，因为每一个都对应某个伴随——Maybe 对应集合与 pointed sets 之间的伴随，State 对应集合与 sets-over-(s × s) 之间的伴随，IO 对应基于 IO 操作签名的自由 monad 构造。知道这一点不会让日常 monadic programming 更容易，但它解释了为什么接口会是现在这样，也解释了为什么不同 monad 可以使用同一套代数机器组合起来，例如 monad transformers 和 effect systems。
范畴 C 上 monad T 的 Kleisli 范畴，与 C 拥有相同对象，而态射 A → B 由 C 中的态射 A → T(B) 给出。Monad bind（Haskell 中的 >>=）就是 Kleisli 范畴中的复合。这精确说明了 monadic sequencing 为什么具有它拥有的结构：它是在一个态射携带计算效应的范畴中的普通复合。
学习这个主题会改变什么
范畴论会改变实践者组织和解释自身所处理结构的方式。
最直接的变化，是跨结构的模式识别。学习范畴论之后，实践者遇到一个新的类型构造子，会立刻问：这是函子吗？如果它以保持结构的方式把类型映射到类型、把函数映射到函数，那么它就是。它是 monad 吗？它是否带有自然方式把值注入进去，并带有自然方式把双重应用压平？系统地提出这些问题，会揭示非形式理解看不见的结构，并确定这个类型构造子支持哪些操作。
第二种变化，是理解为什么某些编程抽象具有它们的结构。柯里化是伴随。列表是某个特定函子的自由 monad。Traversable typeclass 对应某种特定范畴结构。各种 Haskell typeclass——Functor、Applicative、Monad、Foldable、Traversable——形成了一个结构化层级，反映这些名称背后结构之间的范畴关系。理解范畴基础，意味着理解这个层级为什么如此，而不是把它体验成任意设计决策。
第三种变化，是能够进入范畴论文献。编程语言理论和类型论研究论文越来越多地使用范畴词汇而不加定义。熟练掌握范畴论的实践者可以阅读这些文献；没有这种能力的人，则会遇到一个随着研究前沿推进而不断扩大的词汇缺口。
第四种变化最久才会显现，即养成追问泛性质的习惯。遇到一个新构造——新的数据类型、新的代数结构、新的编程模式——受范畴论训练的实践者会问：是否存在一个刻画它的泛性质？它是初始对象、终端对象、自由构造、余积吗？这些问题常常有答案，而答案会给出该构造的本质性质，不需要分类讨论或 ad hoc 推理。
资源
书籍与文本
Awodey 的 Category Theory（第 2 版，Oxford，2010）是多数学习者的最佳起点。它要求的数学背景少于 Mac Lane，覆盖相同核心概念，并且在教学上更慷慨。写作清晰，例子横跨数学与计算机科学，节奏允许抽象沉淀后再进入下一层。多数计算机科学学习者应从这里开始。
Mac Lane 的 Categories for the Working Mathematician（第 2 版，Springer，1978）是经典数学参考，面向数学家写成，并预设大量数学准备。它比 Awodey 更密集、更综合，也要求更高。数学背景很强的学习者可能更愿意从这里开始；其他人应先读 Awodey，然后在需要某个具体主题更完整处理时回到 Mac Lane。
Milewski 的 Category Theory for Programmers（在线免费，也有纸质合集和 YouTube 版）通过 Haskell 例子发展范畴论。对于没有数学背景的程序员来说，它是最易进入的入口；对于被数学处理方式吓住的学习者，这是正确选择。限制在于，其数学内容比 Awodey 或 Mac Lane 更轻；Milewski 是入口，而不是终点。
Pierce 的 Basic Category Theory for Computer Scientists（MIT Press，1991）篇幅短、年代较早，但仍然是最好的简短 CS 向导论。它的紧凑性使它适合作为第一次接触或复习；CS 取向意味着例子立刻相关。1991 年这个时间意味着它早于大量应用范畴论工作，但核心材料是永久的。
Barr 和 Wells 的 Category Theory for Computing Science（免费在线，第 3 版）覆盖与 Awodey 相同的核心材料，但更强调 CS。它比 Pierce 更全面地处理 CS 应用，覆盖代数自动机理论、编程语言的范畴语义，以及其他 CS 专门主题，而这些在 Awodey 中只被简要处理。Awodey（用于数学基础和清晰性）与 Barr-Wells（用于 CS 应用）的组合，比单独读任一本更有效。
Riehl 的 Category Theory in Context（Dover，2016，可在 math.jhu.edu/~eriehl/context.pdf 免费获取）是研究生水平数学处理，但写作清楚，对完成 Awodey 的积极读者而言可以进入。它以比 Awodey 更完整的方式覆盖 representability、极限与余极限、伴随和 monads，并在 Awodey 水平的数学与当代研究文献之间架桥。
对于 应用范畴论，Fong 和 Spivak 的 Seven Sketches in Compositionality（arxiv.org/abs/1803.05316 免费）是入口。它从范畴视角覆盖预序、资源理论、数据库、co-design、信号流图和电路，且非数学家也可以进入。对于有兴趣把范畴论应用到工程和科学领域的学习者，这是正确文本。
对于 范畴逻辑和编程语言语义，Lambek 和 Scott 的 Introduction to Higher-Order Categorical Logic（Cambridge，1986）是经典参考。它发展了 Cartesian closed categories、类型化 λ 演算和直觉主义逻辑之间的对应，对于理解 PLT 与范畴论为何如此深度连接是必要的。
| 书籍 | 作用 | 类型 |
|---|---|---|
| Awodey，Category Theory（第 2 版） | 标准且易进入的入口 | 入门 |
| Mac Lane，Categories for the Working Mathematician（第 2 版） | 经典数学参考 | 参考 |
| Milewski，Category Theory for Programmers（免费） | 面向程序员的导论 | 入门 |
| Pierce，Basic Category Theory for Computer Scientists | 简短 CS 向入口 | 入门 |
| Barr & Wells，Category Theory for Computing Science（免费） | 综合 CS 向文本 | 深入 |
| Riehl，Category Theory in Context（免费） | 研究生水平处理 | 深入 |
| Fong & Spivak，Seven Sketches in Compositionality（免费） | 应用范畴论入口 | 入门 |
| Lambek & Scott，Introduction to Higher-Order Categorical Logic | 范畴逻辑与 PLT | 深入 |
| Mac Lane & Moerdijk，Sheaves in Geometry and Logic | 超出 CS 学习路径的 Topos 理论 | 辅助 |
课程与讲座
Milewski 的 Category Theory for Programmers YouTube series（免费）配套其书，是目前最易进入的视频导论。讲座用适合首次接触该主题的程序员的节奏展开材料，并持续使用 Haskell 例子。
MIT 18.S097（Category Theory for Machine Learning，在材料可用时免费）代表范畴论与 ML 研究之间正在出现的连接。来自类似课程的材料一旦出现，都值得关注。
Applied Category Theory School（ACT，每年举办，并配有 reading groups）产出面向纯数学之外学习者的易进入导论材料。ACT reading groups 会覆盖 Seven Sketches 和相关文本；学校讲座可以在 YouTube 获取。
Emily Riehl 的讲座，包括各种 summer school 中关于范畴论的讲座（YouTube 免费），以高级本科生可进入的层级覆盖她书中的数学内容。她对 Yoneda lemma 和伴随的处理尤其清楚。
The Catsters 视频（YouTube 免费）是一组较早但仍有用的短教学解释，讲解核心范畴论概念。它们不面向 CS，但在正式阅读定义前，常能让积、余积、伴随和自然变换等定义更容易被“听懂”。
Topos Institute 产出关于应用范畴论的报告和研讨会，包括与系统、数据库、概率和科学建模相关的例子。材料层级不一，但对于想了解应用范畴论当前使用方向的读者来说，这是良好的当前来源。
| 课程 | 平台 | 类型 |
|---|---|---|
| Milewski，Category Theory for Programmers lectures（免费） | YouTube | 入门 |
| ACT School lectures（免费） | YouTube / ACT site | 入门 |
| Emily Riehl category theory lectures（免费） | YouTube | 深入 |
| The Catsters category theory videos（免费） | YouTube | 辅助 |
| Topos Institute talks（免费） | YouTube / topos.institute | 参考 |
实践、工具与当前来源
nLab（ncatlab.org）是范畴论及其应用的核心参考 wiki。它质量不均——有些条目优秀，有些稀疏——但它是这个主题最综合的在线资源。用它查询具体概念和连接，不要把它当作阅读顺序。
带着对范畴结构的明确关注，推导 Haskell 的 Functor、Applicative 和 Monad typeclasses——推导函子律，验证具体实例的 monad 律，实现 Kleisli composition——可以建立阅读无法提供的直觉。从零实现 State、Maybe 和 Reader monads，并验证它们满足 monad 律。
Agda 证明助手可以用来形式化范畴定义并证明范畴律，这使抽象定义以阅读无法做到的方式变得可操作。在 Agda 中形式化的范畴论——其中函子是一个依赖 record type，带有对象映射、态射映射和函子性证明等字段——是程序员能够获得的最精确的定义接触方式。
Catlab.jl（免费，Julia package）提供了一个用于应用范畴论的 Julia 框架，实现了 operads、functors、diagrams 和 C-sets。它是目前应用范畴论工作中最成熟的编程环境。
| 资源 | 平台 | 类型 |
|---|---|---|
| nLab（免费） | ncatlab.org | 参考 |
| Haskell typeclass 实现（函子律、monad 律） | 本地 | 实践 |
| Agda 范畴论形式化 | 本地 / agda.readthedocs.io | 实践 |
| Catlab.jl（免费） | Julia package | 实践 |
陷阱
| 陷阱 | 为什么会误导 | 更好的回应 |
|---|---|---|
| 把范畴论当成 “Haskell 理论” | Haskell 把 monads、functors 和 foldables 作为一等编程概念，这个历史偶然造成了一个印象：范畴论本质上是关于 Haskell 的。范畴论比 Haskell 早四十年，并且适用于数学、物理和整个 CS。Haskell 视角有用，但只是外围。 | 把 Awodey 的书作为主文本，而不是 Milewski；用 Milewski 建立编程直觉，用 Awodey 建立数学实质。数学视角揭示一般性；Haskell 视角提供可以运行的具体实例。 |
| 接触抽象却缺少例子 grounding | 范畴论如此抽象，以至于人可以学会形式定义并正确操纵它们，却完全不真正理解它们意味着什么。这些定义描述的是许多具体情形中出现的结构；如果不知道这些情形，抽象就是空的。 | 对每一个新的范畴概念，至少找出三个来自不同领域的具体例子：一个来自数学（集合、群、拓扑空间），一个来自编程（类型、程序、效应），一个来自逻辑（命题、证明、推理）。抽象是否有意义，取决于支撑它的具体案例是否充分。 |
| 在掌握基本范畴论前尝试高阶范畴论 | 2-categories、∞-categories 以及同伦类型论的范畴基础都重要且高级。它们需要对普通范畴论有扎实流利度——自然变换、伴随、极限、monads——而这通常需要一年以上形成。没有这个基础就尝试高阶范畴的学习者，通常无法取得进展。 | 在进入高阶范畴前，完成 Awodey，并学习 Riehl 的大量内容。一个好的测试是：你能否精确陈述并解释 Yoneda lemma，包括其证明？如果不能，基本范畴论还不够扎实，不足以进入高阶范畴。 |
| 只学定义，不做习题 | 范畴论习题要求构造函子、验证自然性条件、计算极限，并为具体例子构造伴随。这些构造会发展范畴直觉，而阅读无法替代。这个主题不可能只靠跟随讲解学会。 | 完成主教材中的每一道习题。Awodey 中的习题不是可选补充；它们是学习实际发生的主要场所。对十几个不同例子检查一个候选函子是否真正满足函子性律，会建立二十个解释都无法提供的直觉。 |
| 把 monad 当作终点，而不是一个概念 | Monad 是编程最显性采用的范畴概念，学习者常把获得 monad 直觉当成范畴论学习目标。但 monad 只是众多构造之一；真正使它有用的视角——理解函子可以承载什么代数结构、Kleisli 范畴是什么、为什么效应以这种方式复合——需要更广阔的范畴框架。 | 把 monad 当作第一个重要 CS 应用，而不是终点。在从范畴角度理解 monad 之后，继续学习伴随及其与 monad 的关系、monoidal categories 和 profunctors、范畴语义。只有在更广范畴语境中理解 monad，monad 的范畴视角才最有价值。 |
| 跳过 Yoneda lemma | Yoneda lemma——任何函子 F: C → Set 都自然同构于某个对象 A 的 hom-functor Hom(-, A)——是基本范畴论中最重要的定理。它揭示了对象完全由进入它们或从它们出发的态射决定，揭示了抽象范畴结构可以被具体的集合值函子忠实表示，也揭示了 hom-functor 是抽象与具体之间的桥梁。许多学习者觉得它神秘，并投入不足。 | 至少花一周学习 Yoneda lemma。逐行推导证明。分别在集合、群和类型三个具体情形中验证它。然后阅读 Mac Lane 的评论：“Yoneda’s lemma is a consequence of the fact that hom-functors are representable”，并解释这句话是什么意思。这项时间投入会在后续所有范畴论学习中持续回报。 |