-
Notifications
You must be signed in to change notification settings - Fork 1
Home
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 thoughts 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.
-
:
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
- Introduction - why I think this book is great and why I would like more people to read it
-
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
- Note N_P1Ch03a_NatsCat - Non-Hask example 'dependently typed' categories based on
-
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
anddata-category
Bifunctor is the same asCFunctor
- Note N_P1Ch08b_BiFunctorComposition - Bifuntor composition presented as
CFunctor
composition. - Note N_P1Ch08c_BiFunctorNonHask - BiFunctors in more general setting, note about
Control.Arrow
.
- Note N_P1Ch08a_BiFunctorAsFunctor - Product category in Haskell, combining conceptual packages
-
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):
-
Chapter 2. Limits and Colimits.
- Note N_P2Ch02a_LimitsColimitsExtras -
category-extras
Limit and Colimit in the context of the book, some notes aboutControl.Arrow
- 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
- Note N_P2Ch02a_LimitsColimitsExtras -
-
Chapter 3. Free Monoids.
- Note N_P2Ch03_FreeMonoidFoldMap - my eureka moment that
foldMap
is free monoid construction
- Note N_P2Ch03_FreeMonoidFoldMap - my eureka moment that
-
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
- Note N_P2Ch05a_YonedaAndMap - Hask Yoneda Lemma as stronger, freer, and faster
-
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. There is a much better conceptual work available on this: Greg Pfeil 'Monoiad'
-
Chapter 7 Comonads.
- Note N_P3Ch07a_GameOfLife - Conway's Game of Life
- Note N_P3Ch07b_Comonad - Loose notes about comonad.
-
Chapter 8 F-Algebras
- Note N_P3Ch08a_Falg - About F-, iso-equi recursion, uniqueness condition, example using finite category.
- Note N_P3Ch08b_FalgFreeMonad - Relation between Free Monad and F-algebras.
-
Chapter 9 Algebras 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.
- Note N_P3Ch12a_HaskEnrich -
-
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"