Category Theory for Programmers

Description

Category Theory is one of the most abstract branches of mathematics. It is usually taught to graduate students after they have mastered several other branches of mathematics, like algebra, topology, and group theory. It might, therefore, come as a shock that the basic concepts of category theory can be explained in relatively simple terms to anybody with some experience in programming. That's because, just like programming, category theory is about structure. Mathematicians discover structure in mathematical theories, programmers discover structure in computer programs. Well-structured programs are easier to understand and maintain and are less likely to contain bugs. Category theory provides the language to talk about structure and learning it will make you a better programmer. 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