Home

CTFP Notes

This wiki contains markdown versions of literate Haskell notes from reading Bartosz Milewski's book Category Theory for Programmers.

This is my second reading of the book. To get more out of it, I decided to dedicate some time to finding (or coming up with) conceptual code examples.

I think my notes are ready for public. This project will be a perpetual work in progress, I intend to add to the notes and keep rethinking them as I learn more about the subject. These notes are not perfect and I wrote many of them just for myself.

My focus was on

• writing conceptual Haskell code to supplement code already in the book
• including some equational reasoning proofs using Haskell code this is simpler but less general than the mathematical approach in the book
• expressing non-Hask categories in Haskell, in particular a simple directed graph category with the shape A->B=>C
• supplementing topics in the book with examples using that simple A->B=>C category
• writing down some things that helped me internalize the concepts

Reading some of these notes can feel out of context, unless corresponding chapter in the book is read first.
This work is not as polished and thought out as Milewski's book, I will slowly try to make it better and deeper.

Common conventions used in my notes

• : is added to type level operators, for example :. is type level composition
• code blocks without language annotations are used for proofs (like equational reasoning) or for code fragments used for documentation/reference only (like typeclass definitions imported from other packages).
• I use the term 'dependently typed' loosely to mean DataKinds and friends.
• I use literate Haskell Bird Style and all Haskell code is converted to code block with Haskell language annotation

TOC

• Introduction - why I think this book is great and why I would like more people to read it

Notes about Part 1 of the Book.

• Chapter 3. Categories Great and Small.
  • Note N_P1Ch03a_NatsCat - Non-Hask example 'dependently typed' categories based on Nat
  • Note N_P1Ch03b_FiniteCats - Non-Hask simple directed graph categories with GADTs and DataKinds
  • Note N_P1Ch03c_DiscreteCats - Note about discrete categories in Haskell

• Chapter 7. Functors.
  • Note N_P1Ch07_Functors_Composition - Hask Functor Composition
  • Note N_P1Ch07b_Functors_AcrossCats - General (Non-Hask) Functors (CFunctor) in Haskell
• Chapter 8. Functoriality.
  • Note N_P1Ch08a_BiFunctorAsFunctor - Product category in Haskell, combining conceptual packages category-extras and data-category Bifunctor is the same as CFunctor
  • Note N_P1Ch08b_BiFunctorComposition - Bifuntor composition presented as CFunctor composition.
• Chapter 10. Natural Transformations.
  • Note N_P1Ch10_NaturalTransformations - Hask Natural Transformations
  • Note N_P1Ch10b_NTsNonHask - Non-Hask Natural Transformations

Work-in-progress (reader stay away):

• N_P1Ch03c_DiscreteCats

Notes about Part 2.

• Chapter 2. Limits and Colimits.
  • Note N_P2Ch02a_LimitsColimitsExtras - category-extras Limit and Colimit in the context of the book
  • Note N_P2Ch02b_Continuity - Continuity. Some not continuous Hask functors and 'dependently typed' proofs in Haskell
  • Note N_P1Ch02c_Equalizer - Equalizer. see how far I can go trying to define equalizer in Haskell
• Chapter 3. Free Monoids.
  • Note N_P2Ch03_FreeMonoidFoldMap - my eureka moment that foldMap is free monoid construction
• Chapter 5. The Yoneda Lemma.
  • Note N_P2Ch05a_YonedaAndMap - Hask Yoneda Lemma as stronger, freer, and faster fmap
  • Note N_P2Ch05b_YonedaNonHask - non-Hask Yoneda Lemma, pattern match intuition

Notes about Part 3.

• Chapter 2 Adjunctions
  • Note N_P3Ch02a_CurryAdj - Exponential from Adjunction notes.
  • Note N_P3Ch02b_AdjNonHask - non-Hask adjunction, Product adjunction in Haskell
  • Note N_P3Ch02c_AdjProps - loose notes about adjunction properties
• Chapter 6 Monads Categorically
  • Note N_P3Ch06a_CTMonads - loose notes about monads, mostly written for myself
  • Note N_P3Ch06b_FiniteMonads - work in progress about monads on finite cats
  • Note N_P3Ch06c_MonoidalCats - work in progress about monoidal categories in Haskell
• Chapter 7 Comonads.
  • Note N_P3Ch07a_GameOfLife - Conway's Game of Life
  • Note N_P3Ch07b_Comonad - Loose notes about comonad.
• Chapter 8 F-Algeras
  • Note N_P3Ch08a_Falg - About F-algeras, iso-equi recursion, uniqueness condition, example using finite category.
  • Note N_P3Ch08b_FalgFreeMonad - Relation between Free Monad and F-algebras.
• Chapter 9 Algeras for monads
  • Note N_P3Ch09a_Talg - Side-note about structure of the category of monad algebras for the monad obtained from free-forgetful adjunction
• Chapter 11 Kan Extensions
  • Note (N_P3Ch11a_KanExt)](N_P3Ch11a_KanExt) - Various notes on Kan Extensions
• Chapter 12 Enriched Categories.
  • Note N_P3Ch12a_HaskEnrich - PolyKinds is enriching over Hask
  • Note N_P3Ch12b_EnrichedPreorder - Preorder example in conceptual Haskell code.
• Chapter 15 Monads, Monoids, and Categories.
  • Note N_P3Ch15a_Spans - detailed notes about bicategory Span
  • Note N_P3Ch15b_CatsAsMonads - Haskell take on "category is just a monad in the bicategory of spans"