Category theory for programmers

Preface......Page 13
Part One......Page 19
  Arrows as Functions......Page 20
  Properties of Composition......Page 23
  Composition is the Essence of Programming......Page 26
  Challenges......Page 28
  Who Needs Types?......Page 29
  Types Are About Composability......Page 30
  What Are Types?......Page 32
  Why Do We Need a Mathematical Model?......Page 35
  Examples of Types......Page 38
  Challenges......Page 43
  Simple Graphs......Page 45
  Orders......Page 46
  Monoid as Set......Page 47
  Monoid as Category......Page 51
  Challenges......Page 54
 Kleisli Categories......Page 56
  The Writer Category......Page 61
  Writer in Haskell......Page 64
  Kleisli Categories......Page 66
  Challenge......Page 67
 Products and Coproducts......Page 69
  Initial Object......Page 70
  Terminal Object......Page 72
  Duality......Page 73
  Isomorphisms......Page 74
  Products......Page 76
  Coproduct......Page 82
  Asymmetry......Page 85
  Challenges......Page 88
  Bibliography......Page 89
  Product Types......Page 90
  Records......Page 95
  Sum Types......Page 96
  Algebra of Types......Page 101
  Challenges......Page 105
 Functors......Page 107
  Functors in Programming......Page 109
   The Maybe Functor......Page 110
   Equational Reasoning......Page 112
   Optional......Page 115
   Typeclasses......Page 117
   The List Functor......Page 119
   The Reader Functor......Page 122
  Functors as Containers......Page 124
  Functor Composition......Page 127
  Challenges......Page 129
  Bifunctors......Page 131
  Product and Coproduct Bifunctors......Page 134
  Functorial Algebraic Data Types......Page 136
  Functors in C++......Page 140
  The Writer Functor......Page 142
  Covariant and Contravariant Functors......Page 144
  Profunctors......Page 148
  The Hom-Functor......Page 149
  Challenges......Page 150
 Function Types......Page 152
  Universal Construction......Page 154
  Currying......Page 159
  Exponentials......Page 162
  Cartesian Closed Categories......Page 164
   Zeroth Power......Page 165
   First Power......Page 166
   Exponentials of Sums......Page 167
  Curry-Howard Isomorphism......Page 168
  Bibliography......Page 171
 Natural Transformations......Page 172
  Polymorphic Functions......Page 176
  Beyond Naturality......Page 183
  Functor Category......Page 185
  2-Categories......Page 189
  Conclusion......Page 194
  Challenges......Page 195
Part Two......Page 197
 Declarative Programming......Page 198
 Limits and Colimits......Page 206
  Limit as a Natural Isomorphism......Page 212
  Examples of Limits......Page 216
  Colimits......Page 224
  Continuity......Page 225
  Challenges......Page 227
 Free Monoids......Page 229
  Free Monoid in Haskell......Page 231
  Free Monoid Universal Construction......Page 232
  Challenges......Page 237
 Representable Functors......Page 238
  The Hom Functor......Page 239
  Representable Functors......Page 242
  Bibliography......Page 248
 The Yoneda Lemma......Page 249
  Yoneda in Haskell......Page 256
  Co-Yoneda......Page 258
  Challenges......Page 259
  Bibliography......Page 260
 Yoneda Embedding......Page 261
  The Embedding......Page 263
  Application to Haskell......Page 264
  Preorder Example......Page 266
  Naturality......Page 268
  Challenges......Page 269
Part Three......Page 271
  Functors......Page 272
  Commuting Diagrams......Page 273
  Natural Transformations......Page 274
  Hom-Sets......Page 276
  Hom-Set Isomorphisms......Page 277
  Asymmetry of Hom-Sets......Page 278
  Challenges......Page 279
 Adjunctions......Page 280
  Adjunction and Unit/Counit Pair......Page 281
  Adjunctions and Hom-Sets......Page 286
  Product from Adjunction......Page 291
  Exponential from Adjunction......Page 296
  Challenges......Page 297
 Free/Forgetful Adjunctions......Page 299
  Some Intuitions......Page 303
  Challenges......Page 306
 Monads: Programmer's Definition......Page 307
  The Kleisli Category......Page 309
  Fish Anatomy......Page 312
  The do Notation......Page 314
  The Problem......Page 319
  The Solution......Page 320
   Partiality......Page 321
   Nondeterminism......Page 322
   Read-Only State......Page 325
   Write-Only State......Page 326
   State......Page 327
   Continuations......Page 329
   Interactive Input......Page 331
   Interactive Output......Page 334
  Conclusion......Page 335
 Monads Categorically......Page 336
  Monoidal Categories......Page 341
  Monoid in a Monoidal Category......Page 347
  Monads as Monoids......Page 348
  Monads from Adjunctions......Page 351
 Comonads......Page 355
  Programming with Comonads......Page 356
  The Product Comonad......Page 357
  Dissecting the Composition......Page 358
  The Stream Comonad......Page 361
  Comonad Categorically......Page 363
  The Store Comonad......Page 366
  Challenges......Page 369
 F-Algebras......Page 370
  Recursion......Page 374
  Category of F-Algebras......Page 377
  Natural Numbers......Page 380
  Catamorphisms......Page 381
  Folds......Page 383
  Coalgebras......Page 384
  Challenges......Page 388
 Algebras for Monads......Page 389
  T-algebras......Page 392
  The Kleisli Category......Page 396
  Coalgebras for Comonads......Page 398
  Lenses......Page 399
  Challenges......Page 401
 Ends and Coends......Page 402
  Dinatural Transformations......Page 404
  Ends......Page 406
  Ends as Equalizers......Page 409
  Natural Transformations as Ends......Page 410
  Coends......Page 412
  Ninja Yoneda Lemma......Page 415
  Profunctor Composition......Page 417
 Kan Extensions......Page 419
  Right Kan Extension......Page 422
  Kan Extension as Adjunction......Page 424
  Left Kan Extension......Page 426
  Kan Extensions as Ends......Page 429
  Kan Extensions in Haskell......Page 432
  Free Functor......Page 435
 Enriched Categories......Page 438
  Why Monoidal Category?......Page 439
  Monoidal Category......Page 440
  Enriched Category......Page 443
  Preorders......Page 445
  Metric Spaces......Page 446
  Enriched Functors......Page 448
  Self Enrichment......Page 449
  Relation to 2-Categories......Page 451
 Topoi......Page 452
  Subobject Classifier......Page 453
  Topoi and Logic......Page 458
  Challenges......Page 459
  Universal Algebra......Page 461
  Lawvere Theories......Page 463
  Models of Lawvere Theories......Page 467
  The Theory of Monoids......Page 469
  Lawvere Theories and Monads......Page 470
  Monads as Coends......Page 473
  Lawvere Theory of Side Effects......Page 477
  Further Reading......Page 479
  Bicategories......Page 480
  Monads......Page 486
  Challenges......Page 490
Appendices......Page 491
 Index......Page 492
 Acknowledgments......Page 495
 Colophon......Page 496
 Copyleft notice......Page 497