第1页 / 共492页
第2页 / 共492页
第3页 / 共492页
第4页 / 共492页
第5页 / 共492页
第6页 / 共492页
第7页 / 共492页
第8页 / 共492页
category-theory-for-programmers.pdf
Preface
Part One
Category: The Essence of Composition
Arrows as Functions
Properties of Composition
Composition is the Essence of Programming
Challenges
Types and Functions
Who Needs Types?
Types Are About Composability
What Are Types?
Why Do We Need a Mathematical Model?
Pure and Dirty Functions
Examples of Types
Challenges
Categories Great and Small
No Objects
Simple Graphs
Orders
Monoid as Set
Monoid as Category
Challenges
Kleisli Categories
The Writer Category
Writer in Haskell
Kleisli Categories
Challenge
Products and Coproducts
Initial Object
Terminal Object
Duality
Isomorphisms
Products
Coproduct
Asymmetry
Challenges
Bibliography
Simple Algebraic Data Types
Product Types
Records
Sum Types
Algebra of Types
Challenges
Functors
Functors in Programming
The Maybe Functor
Equational Reasoning
Optional
Typeclasses
Functor in C++
The List Functor
The Reader Functor
Functors as Containers
Functor Composition
Challenges
Functoriality
Bifunctors
Product and Coproduct Bifunctors
Functorial Algebraic Data Types
Functors in C++
The Writer Functor
Covariant and Contravariant Functors
Profunctors
The Hom-Functor
Challenges
Function Types
Universal Construction
Currying
Exponentials
Cartesian Closed Categories
Exponentials and Algebraic Data Types
Zeroth Power
Powers of One
First Power
Exponentials of Sums
Exponentials of Exponentials
Exponentials over Products
Curry-Howard Isomorphism
Bibliography
Natural Transformations
Polymorphic Functions
Beyond Naturality
Functor Category
2-Categories
Conclusion
Challenges
Part Two
Declarative Programming
Limits and Colimits
Limit as a Natural Isomorphism
Examples of Limits
Colimits
Continuity
Challenges
Free Monoids
Free Monoid in Haskell
Free Monoid Universal Construction
Challenges
Representable Functors
The Hom Functor
Representable Functors
Challenges
Bibliography
The Yoneda Lemma
Yoneda in Haskell
Co-Yoneda
Challenges
Bibliography
Yoneda Embedding
The Embedding
Application to Haskell
Preorder Example
Naturality
Challenges
Part Three
It's All About Morphisms
Functors
Commuting Diagrams
Natural Transformations
Natural Isomorphisms
Hom-Sets
Hom-Set Isomorphisms
Asymmetry of Hom-Sets
Challenges
Adjunctions
Adjunction and Unit/Counit Pair
Adjunctions and Hom-Sets
Product from Adjunction
Exponential from Adjunction
Challenges
Free/Forgetful Adjunctions
Some Intuitions
Challenges
Monads: Programmer's Definition
The Kleisli Category
Fish Anatomy
The do Notation
Monads and Effects
The Problem
The Solution
Partiality
Nondeterminism
Read-Only State
Write-Only State
State
Exceptions
Continuations
Interactive Input
Interactive Output
Conclusion
Monads Categorically
Monoidal Categories
Monoid in a Monoidal Category
Monads as Monoids
Monads from Adjunctions
Comonads
Programming with Comonads
The Product Comonad
Dissecting the Composition
The Stream Comonad
Comonad Categorically
The Store Comonad
Challenges
F-Algebras
Recursion
Category of F-Algebras
Natural Numbers
Catamorphisms
Folds
Coalgebras
Challenges
Algebras for Monads
T-algebras
The Kleisli Category
Coalgebras for Comonads
Lenses
Challenges
Ends and Coends
Dinatural Transformations
Ends
Ends as Equalizers
Natural Transformations as Ends
Coends
Ninja Yoneda Lemma
Profunctor Composition
Kan Extensions
Right Kan Extension
Kan Extension as Adjunction
Left Kan Extension
Kan Extensions as Ends
Kan Extensions in Haskell
Free Functor
Enriched Categories
Why Monoidal Category?
Monoidal Category
Enriched Category
Preorders
Metric Spaces
Enriched Functors
Self Enrichment
Relation to 2-Categories
Topoi
Subobject Classifier
Topos
Topoi and Logic
Challenges
Lawvere Theories
Universal Algebra
Lawvere Theories
Models of Lawvere Theories
The Theory of Monoids
Lawvere Theories and Monads
Monads as Coends
Lawvere Theory of Side Effects
Challenges
Further Reading
Monads, Monoids, and Categories
Bicategories
Monads
Challenges
Bibliography
Appendices
Index
Acknowledgments
Colophon
Copyleft notice
Category Theory
for Programmers
By Bartosz Milewski
compiled and edited by
Igal Tabachnik
Category Theory for Programmers
Bartosz Milewski
Version v1.0.0-0-g41e0fc3
October 21, 2018
This work is licensed under a Creative Commons
Attribution-ShareAlike 4.0 International License (cc by-sa 4.0).
Converted from a series of blog posts by Bartosz Milewski.
PDF and book compiled by Igal Tabachnik.
LATEX source code is available on GitHub:
https://github.com/hmemcpy/milewski-ctfp-pdf
Contents
Preface
Part One
.
Properties of Composition .
1 Category: The Essence of Composition
.
.
1.1 Arrows as Functions .
.
1.2
.
1.3 Composition is the Essence of Programming .
1.4 Challenges .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2 Types and Functions
.
.
.
.
.
.
2.1 Who Needs Types? .
.
.
2.2 Types Are About Composability .
.
2.3 What Are Types? .
.
.
2.4 Why Do We Need a Mathematical Model?
.
2.5
.
2.6
2.7 Challenges .
.
Pure and Dirty Functions .
.
Examples of Types .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
i
xi
2
2
2
5
8
10
11
11
12
14
17
20
20
24
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Simple Graphs .
.
.
3 Categories Great and Small
.
.
.
.
.
.
.
3.1 No Objects .
.
3.2
.
3.3 Orders
.
3.4 Monoid as Set
.
3.5 Monoid as Category .
.
3.6 Challenges .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
4 Kleisli Categories
4.1 The Writer Category .
.
4.2 Writer in Haskell
.
4.3 Kleisli Categories
4.4 Challenge .
.
.
.
.
.
.
.
.
.
.
.
.
.
5 Products and Coproducts
.
.
.
.
.
.
.
.
.
5.1
.
Initial Object .
5.2 Terminal Object
5.3 Duality .
.
.
Isomorphisms .
5.4
.
.
5.5
Products
.
.
5.6 Coproduct
.
.
.
.
5.7 Asymmetry .
.
5.8 Challenges .
.
5.9 Bibliography .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
6 Simple Algebraic Data Types
.
.
.
.
.
6.1
.
6.2 Records .
6.3
.
6.4 Algebra of Types .
Product Types .
.
.
.
Sum Types .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
27
27
28
28
29
34
36
38
43
46
49
50
52
53
55
56
57
59
65
68
71
72
73
74
78
79
83
ii
6.5 Challenges .
.
.
.
.
.
.
.
.
.
.
.
7 Functors
7.1
.
.
.
.
.
Functors in Programming .
.
7.1.1 The Maybe Functor .
7.1.2
.
.
.
7.1.3 Optional .
.
Typeclasses .
.
7.1.4
.
7.1.5
Functor in C++ .
.
7.1.6 The List Functor .
7.1.7 The Reader Functor .
.
Functors as Containers .
.
.
Functor Composition .
.
.
.
.
.
Equational Reasoning .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
7.2
7.3
7.4 Challenges .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
8 Functoriality
.
8.1 Bifunctors
.
Product and Coproduct Bifunctors .
8.2
.
.
Functorial Algebraic Data Types .
8.3
.
.
.
8.4
Functors in C++ .
.
8.5 The Writer Functor
.
.
.
8.6 Covariant and Contravariant Functors .
.
8.7
.
.
8.8 The Hom-Functor .
8.9 Challenges .
.
.
Profunctors .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
9 Function Types
9.1 Universal Construction .
.
9.2 Currying .
9.3
.
.
Exponentials .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
iii
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
88
89
92
92
94
97
98
100
101
103
105
108
110
112
112
115
117
121
123
125
128
129
130
132
133
138
142
.
.
.
.
.
9.4 Cartesian Closed Categories .
9.5
.
Exponentials and Algebraic Data Types .
9.5.1
.
.
9.5.2
.
9.5.3
9.5.4
.
.
9.5.5
.
9.5.6
.
.
.
.
Zeroth Power .
.
.
Powers of One
.
First Power
.
.
.
Exponentials of Sums .
Exponentials of Exponentials .
.
Exponentials over Products .
.
.
.
.
9.6 Curry-Howard Isomorphism .
9.7 Bibliography .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
10 Natural Transformations
10.1 Polymorphic Functions .
10.2 Beyond Naturality .
.
.
10.3 Functor Category .
.
.
10.4 2-Categories .
10.5 Conclusion .
.
.
.
.
.
.
10.6 Challenges .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Part Two
11 Declarative Programming
12 Limits and Colimits
12.1 Limit as a Natural Isomorphism .
.
12.2 Examples of Limits
.
.
12.3 Colimits
.
12.4 Continuity .
.
.
.
.
12.5 Challenges .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
iv
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
143
144
145
145
146
146
147
147
147
150
151
155
161
163
167
172
173
176
176
184
190
194
202
203
205
13 Free Monoids
13.1 Free Monoid in Haskell
.
13.2 Free Monoid Universal Construction .
.
13.3 Challenges .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
14 Representable Functors
.
14.1 The Hom Functor
.
14.2 Representable Functors .
.
14.3 Challenges .
.
14.4 Bibliography .
.
.
.
.
.
.
.
.
.
.
.
.
.
15 The Yoneda Lemma
15.1 Yoneda in Haskell
.
15.2 Co-Yoneda .
.
.
.
.
15.3 Challenges .
.
15.4 Bibliography .
.
.
.
.
.
.
.
.
.
.
16 Yoneda Embedding
.
16.1 The Embedding .
.
16.2 Application to Haskell
16.3 Preorder Example .
.
.
.
16.4 Naturality .
16.5 Challenges .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Part Three
17 It’s All About Morphisms
.
17.1 Functors
.
17.2 Commuting Diagrams .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
v
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
207
209
210
215
216
218
220
226
226
227
234
236
237
237
238
241
242
243
245
246
249
249
249
250
17.3 Natural Transformations .
.
17.4 Natural Isomorphisms .
.
17.5 Hom-Sets .
.
.
.
17.6 Hom-Set Isomorphisms .
.
17.7 Asymmetry of Hom-Sets .
17.8 Challenges .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
18 Adjunctions
18.1 Adjunction and Unit/Counit Pair .
.
18.2 Adjunctions and Hom-Sets .
.
.
18.3 Product from Adjunction .
.
.
.
18.4 Exponential from Adjunction .
18.5 Challenges .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
19 Free/Forgetful Adjunctions
.
.
19.1 Some Intuitions
19.2 Challenges .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
20 Monads: Programmer’s Definition
.
.
.
.
.
.
20.1 The Kleisli Category .
.
20.2 Fish Anatomy .
.
.
20.3 The do Notation .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
21 Monads and Effects
21.1 The Problem .
21.2 The Solution .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
21.2.1 Partiality .
.
21.2.2 Nondeterminism .
21.2.3 Read-Only State .
.
21.2.4 Write-Only State .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
vi
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
251
253
253
254
255
256
257
258
264
268
273
275
276
280
283
284
286
289
291
295
295
296
297
298
301
302
相关推荐
2023年江西萍乡中考道德与法治真题及答案.doc
2012年重庆南川中考生物真题及答案.doc
2013年江西师范大学地理学综合及文艺理论基础考研真题.doc
2020年四川甘孜小升初语文真题及答案I卷.doc
2020年注册岩土工程师专业基础考试真题及答案.doc
2023-2024学年福建省厦门市九年级上学期数学月考试题及答案.doc
2021-2022学年辽宁省沈阳市大东区九年级上学期语文期末试题及答案.doc
2022-2023学年北京东城区初三第一学期物理期末试卷及答案.doc
2018上半年江西教师资格初中地理学科知识与教学能力真题及答案.doc
2012年河北国家公务员申论考试真题及答案-省级.doc
2020-2021学年江苏省扬州市江都区邵樊片九年级上学期数学第一次质量检测试题及答案.doc
2022下半年黑龙江教师资格证中学综合素质真题及答案.doc
