《Category Theory For Programmers》

【实例截图】

【核心代码】

Contents
Preface xiii
Part One 3
1 Category: The Essence of Composition 3
1.1 Arrows as Functions . . . . . . . . . . . . . . . . . . . . 3
1.2 Properties of Composition . . . . . . . . . . . . . . . . 6
1.3 Composition is the Essence of Programming . . . . . . 9
1.4 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 11
2 Types and Functions 13
2.1 Who Needs Types? . . . . . . . . . . . . . . . . . . . . 13
2.2 Types Are About Composability . . . . . . . . . . . . . 14
2.3 What Are Types? . . . . . . . . . . . . . . . . . . . . . 16
2.4 Why Do We Need a Mathematical Model? . . . . . . . 19
2.5 Pure and Dirty Functions . . . . . . . . . . . . . . . . . 22
2.6 Examples of Types . . . . . . . . . . . . . . . . . . . . . 22
2.7 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 26
iii
3 Categories Great and Small 29
3.1 No Objects . . . . . . . . . . . . . . . . . . . . . . . . . 29
3.2 Simple Graphs . . . . . . . . . . . . . . . . . . . . . . . 30
3.3 Orders . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3.4 Monoid as Set . . . . . . . . . . . . . . . . . . . . . . . 31
3.5 Monoid as Category . . . . . . . . . . . . . . . . . . . . 36
3.6 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 38
4 Kleisli Categories 41
4.1 The Writer Category . . . . . . . . . . . . . . . . . . . 46
4.2 Writer in Haskell . . . . . . . . . . . . . . . . . . . . . 49
4.3 Kleisli Categories . . . . . . . . . . . . . . . . . . . . . 52
4.4 Challenge . . . . . . . . . . . . . . . . . . . . . . . . . . 53
5 Products and Coproducts 55
5.1 Initial Object . . . . . . . . . . . . . . . . . . . . . . . . 56
5.2 Terminal Object . . . . . . . . . . . . . . . . . . . . . . 58
5.3 Duality . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
5.4 Isomorphisms . . . . . . . . . . . . . . . . . . . . . . . 60
5.5 Products . . . . . . . . . . . . . . . . . . . . . . . . . . 62
5.6 Coproduct . . . . . . . . . . . . . . . . . . . . . . . . . 68
5.7 Asymmetry . . . . . . . . . . . . . . . . . . . . . . . . . 71
5.8 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 74
5.9 Bibliography . . . . . . . . . . . . . . . . . . . . . . . . 75
6 Simple Algebraic Data Types 77
6.1 Product Types . . . . . . . . . . . . . . . . . . . . . . . 78
6.2 Records . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
6.3 Sum Types . . . . . . . . . . . . . . . . . . . . . . . . . 83
6.4 Algebra of Types . . . . . . . . . . . . . . . . . . . . . . 87
iv
6.5 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 92
7 Functors 93
7.1 Functors in Programming . . . . . . . . . . . . . . . . . 96
7.1.1 The Maybe Functor . . . . . . . . . . . . . . . . 96
7.1.2 Equational Reasoning . . . . . . . . . . . . . . 98
7.1.3 Optional . . . . . . . . . . . . . . . . . . . . . . 101
7.1.4 Typeclasses . . . . . . . . . . . . . . . . . . . . 102
7.1.5 Functor in C . . . . . . . . . . . . . . . . . . 104
7.1.6 The List Functor . . . . . . . . . . . . . . . . . . 105
7.1.7 The Reader Functor . . . . . . . . . . . . . . . . 107
7.2 Functors as Containers . . . . . . . . . . . . . . . . . . 109
7.3 Functor Composition . . . . . . . . . . . . . . . . . . . 112
7.4 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 114
8 Functoriality 117
8.1 Bifunctors . . . . . . . . . . . . . . . . . . . . . . . . . 117
8.2 Product and Coproduct Bifunctors . . . . . . . . . . . . 120
8.3 Functorial Algebraic Data Types . . . . . . . . . . . . . 122
8.4 Functors in C . . . . . . . . . . . . . . . . . . . . . . 126
8.5 The Writer Functor . . . . . . . . . . . . . . . . . . . . 128
8.6 Covariant and Contravariant Functors . . . . . . . . . . 130
8.7 Profunctors . . . . . . . . . . . . . . . . . . . . . . . . . 133
8.8 The Hom-Functor . . . . . . . . . . . . . . . . . . . . . 134
8.9 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 135
9 Function Types 137
9.1 Universal Construction . . . . . . . . . . . . . . . . . . 138
9.2 Currying . . . . . . . . . . . . . . . . . . . . . . . . . . 143
9.3 Exponentials . . . . . . . . . . . . . . . . . . . . . . . . 146
v
9.4 Cartesian Closed Categories . . . . . . . . . . . . . . . 148
9.5 Exponentials and Algebraic Data Types . . . . . . . . . 149
9.5.1 Zeroth Power . . . . . . . . . . . . . . . . . . . 149
9.5.2 Powers of One . . . . . . . . . . . . . . . . . . 150
9.5.3 First Power . . . . . . . . . . . . . . . . . . . . 150
9.5.4 Exponentials of Sums . . . . . . . . . . . . . . . 150
9.5.5 Exponentials of Exponentials . . . . . . . . . . 151
9.5.6 Exponentials over Products . . . . . . . . . . . 151
9.6 Curry-Howard Isomorphism . . . . . . . . . . . . . . . 152
9.7 Bibliography . . . . . . . . . . . . . . . . . . . . . . . . 155
10 Natural Transformations 157
10.1 Polymorphic Functions . . . . . . . . . . . . . . . . . . 161
10.2 Beyond Naturality . . . . . . . . . . . . . . . . . . . . . 167
10.3 Functor Category . . . . . . . . . . . . . . . . . . . . . 169
10.4 2-Categories . . . . . . . . . . . . . . . . . . . . . . . . 173
10.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . 178
10.6 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 179
Part Two 183
11 Declarative Programming 183
12 Limits and Colimits 191
12.1 Limit as a Natural Isomorphism . . . . . . . . . . . . . 197
12.2 Examples of Limits . . . . . . . . . . . . . . . . . . . . 201
12.3 Colimits . . . . . . . . . . . . . . . . . . . . . . . . . . 209
12.4 Continuity . . . . . . . . . . . . . . . . . . . . . . . . . 210
12.5 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 212
vi
13 Free Monoids 215
13.1 Free Monoid in Haskell . . . . . . . . . . . . . . . . . . 217
13.2 Free Monoid Universal Construction . . . . . . . . . . 218
13.3 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 223
14 Representable Functors 225
14.1 The Hom Functor . . . . . . . . . . . . . . . . . . . . . 227
14.2 Representable Functors . . . . . . . . . . . . . . . . . . 229
14.3 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 235
14.4 Bibliography . . . . . . . . . . . . . . . . . . . . . . . . 235
15 The Yoneda Lemma 237
15.1 Yoneda in Haskell . . . . . . . . . . . . . . . . . . . . . 244
15.2 Co-Yoneda . . . . . . . . . . . . . . . . . . . . . . . . . 246
15.3 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 247
15.4 Bibliography . . . . . . . . . . . . . . . . . . . . . . . . 247
16 Yoneda Embedding 249
16.1 The Embedding . . . . . . . . . . . . . . . . . . . . . . 252
16.2 Application to Haskell . . . . . . . . . . . . . . . . . . 253
16.3 Preorder Example . . . . . . . . . . . . . . . . . . . . . 254
16.4 Naturality . . . . . . . . . . . . . . . . . . . . . . . . . 256
16.5 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 257
Part Three 261
17 It’s All About Morphisms 261
17.1 Functors . . . . . . . . . . . . . . . . . . . . . . . . . . 261
17.2 Commuting Diagrams . . . . . . . . . . . . . . . . . . . 262
vii
17.3 Natural Transformations . . . . . . . . . . . . . . . . . 263
17.4 Natural Isomorphisms . . . . . . . . . . . . . . . . . . . 265
17.5 Hom-Sets . . . . . . . . . . . . . . . . . . . . . . . . . . 265
17.6 Hom-Set Isomorphisms . . . . . . . . . . . . . . . . . . 266
17.7 Asymmetry of Hom-Sets . . . . . . . . . . . . . . . . . 267
17.8 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 268
18 Adjunctions 269
18.1 Adjunction and Unit/Counit Pair . . . . . . . . . . . . . 270
18.2 Adjunctions and Hom-Sets . . . . . . . . . . . . . . . . 276
18.3 Product from Adjunction . . . . . . . . . . . . . . . . . 280
18.4 Exponential from Adjunction . . . . . . . . . . . . . . . 285
18.5 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 287
19 Free/Forgetful Adjunctions 289
19.1 Some Intuitions . . . . . . . . . . . . . . . . . . . . . . 293
19.2 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 296
20 Monads: Programmer’s Definition 297
20.1 The Kleisli Category . . . . . . . . . . . . . . . . . . . . 299
20.2 Fish Anatomy . . . . . . . . . . . . . . . . . . . . . . . 302
20.3 The do Notation . . . . . . . . . . . . . . . . . . . . . . 304
21 Monads and Effects 309
21.1 The Problem . . . . . . . . . . . . . . . . . . . . . . . . 309
21.2 The Solution . . . . . . . . . . . . . . . . . . . . . . . . 310
21.2.1 Partiality . . . . . . . . . . . . . . . . . . . . . . 311
21.2.2 Nondeterminism . . . . . . . . . . . . . . . . . 312
21.2.3 Read-Only State . . . . . . . . . . . . . . . . . . 315
21.2.4 Write-Only State . . . . . . . . . . . . . . . . . 316
viii
21.2.5 State . . . . . . . . . . . . . . . . . . . . . . . . 317
21.2.6 Exceptions . . . . . . . . . . . . . . . . . . . . . 318
21.2.7 Continuations . . . . . . . . . . . . . . . . . . . 319
21.2.8 Interactive Input . . . . . . . . . . . . . . . . . 321
21.2.9 Interactive Output . . . . . . . . . . . . . . . . 323
21.3 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . 324
22 Monads Categorically 327
22.1 Monoidal Categories . . . . . . . . . . . . . . . . . . . 333
22.2 Monoid in a Monoidal Category . . . . . . . . . . . . . 338
22.3 Monads as Monoids . . . . . . . . . . . . . . . . . . . . 340
22.4 Monads from Adjunctions . . . . . . . . . . . . . . . . 343
23 Comonads 347
23.1 Programming with Comonads . . . . . . . . . . . . . . 348
23.2 The Product Comonad . . . . . . . . . . . . . . . . . . . 349
23.3 Dissecting the Composition . . . . . . . . . . . . . . . 350
23.4 The Stream Comonad . . . . . . . . . . . . . . . . . . . 353
23.5 Comonad Categorically . . . . . . . . . . . . . . . . . . 355
23.6 The Store Comonad . . . . . . . . . . . . . . . . . . . . 357
23.7 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 360
24 F-Algebras 361
24.1 Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . 365
24.2 Category of F-Algebras . . . . . . . . . . . . . . . . . . 367
24.3 Natural Numbers . . . . . . . . . . . . . . . . . . . . . 371
24.4 Catamorphisms . . . . . . . . . . . . . . . . . . . . . . 372
24.5 Folds . . . . . . . . . . . . . . . . . . . . . . . . . . . . 374
24.6 Coalgebras . . . . . . . . . . . . . . . . . . . . . . . . . 375
24.7 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 379
ix
25 Algebras for Monads 381
25.1 T-algebras . . . . . . . . . . . . . . . . . . . . . . . . . 384
25.2 The Kleisli Category . . . . . . . . . . . . . . . . . . . . 388
25.3 Coalgebras for Comonads . . . . . . . . . . . . . . . . . 390
25.4 Lenses . . . . . . . . . . . . . . . . . . . . . . . . . . . 391
25.5 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 393
26 Ends and Coends 395
26.1 Dinatural Transformations . . . . . . . . . . . . . . . . 397
26.2 Ends . . . . . . . . . . . . . . . . . . . . . . . . . . . . 399
26.3 Ends as Equalizers . . . . . . . . . . . . . . . . . . . . . 402
26.4 Natural Transformations as Ends . . . . . . . . . . . . 403
26.5 Coends . . . . . . . . . . . . . . . . . . . . . . . . . . . 405
26.6 Ninja Yoneda Lemma . . . . . . . . . . . . . . . . . . . 408
26.7 Profunctor Composition . . . . . . . . . . . . . . . . . 410
27 Kan Extensions 413
27.1 Right Kan Extension . . . . . . . . . . . . . . . . . . . . 416
27.2 Kan Extension as Adjunction . . . . . . . . . . . . . . . 418
27.3 Left Kan Extension . . . . . . . . . . . . . . . . . . . . 420
27.4 Kan Extensions as Ends . . . . . . . . . . . . . . . . . . 423
27.5 Kan Extensions in Haskell . . . . . . . . . . . . . . . . 427
27.6 Free Functor . . . . . . . . . . . . . . . . . . . . . . . . 429
28 Enriched Categories 433
28.1 Why Monoidal Category? . . . . . . . . . . . . . . . . . 434
28.2 Monoidal Category . . . . . . . . . . . . . . . . . . . . 435
28.3 Enriched Category . . . . . . . . . . . . . . . . . . . . . 438
28.4 Preorders . . . . . . . . . . . . . . . . . . . . . . . . . . 440
28.5 Metric Spaces . . . . . . . . . . . . . . . . . . . . . . . 441
x
28.6 Enriched Functors . . . . . . . . . . . . . . . . . . . . . 442
28.7 Self Enrichment . . . . . . . . . . . . . . . . . . . . . . 443
28.8 Relation to 𝟐-Categories . . . . . . . . . . . . . . . . . 445
29 Topoi 447
29.1 Subobject Classifier . . . . . . . . . . . . . . . . . . . . 448
29.2 Topos . . . . . . . . . . . . . . . . . . . . . . . . . . . . 453
29.3 Topoi and Logic . . . . . . . . . . . . . . . . . . . . . . 454
29.4 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 455
30 Lawvere Theories 457
30.1 Universal Algebra . . . . . . . . . . . . . . . . . . . . . 457
30.2 Lawvere Theories . . . . . . . . . . . . . . . . . . . . . 459
30.3 Models of Lawvere Theories . . . . . . . . . . . . . . . 463
30.4 The Theory of Monoids . . . . . . . . . . . . . . . . . . 465
30.5 Lawvere Theories and Monads . . . . . . . . . . . . . . 466
30.6 Monads as Coends . . . . . . . . . . . . . . . . . . . . . 469
30.7 Lawvere Theory of Side Effects . . . . . . . . . . . . . . 473
30.8 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 475
30.9 Further Reading . . . . . . . . . . . . . . . . . . . . . . 475
31 Monads, Monoids, and Categories 477
31.1 Bicategories . . . . . . . . . . . . . . . . . . . . . . . . 478
31.2 Monads . . . . . . . . . . . . . . . . . . . . . . . . . . . 483
31.3 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . 488
31.4 Bibliography . . . . . . . . . . . . . . . . . . . . . . . . 488
xi
Appendices 489
Index 489
Acknowledgments 493
Colophon 495
Copyleft notice 497