A Partial Ordering of some Category Theory applied to Haskell

I've had a few requests from people wanting to teach themselves applications of Category Theory to Haskell based on posts I've made. I've made things difficult by posting stuff at random levels of difficulty and without any kind of organising thread through them. So here's an attempt to list a bunch of posts related to aspects of category theory. I've grouped them by themes and within each theme I've tried to list the articles in order of difficulty. Unfortunately there can be big gaps between one article and the next as none of this material was intended to be linked together continuously. Nonetheless, I hope this is of some help.

First a warning: Category Theory Screws You Up!.

Monads
The first theme has to be monads of course. But don't forget: monads don't do anything. They're simply an interface to something that you must already have implemented some other way. So don't believe all that hype about how monads are what allow Haskell to use side effects and I/O.

1. If you just want to use IO and don't care about monads: The IO Monad for People who Simply Don't Care


2. This gets more hits than anything else on my blog: You Could Have Invented Monads! (And Maybe You Already Have.)


3. The Trivial Monad


4. Homeland Security Threat Level Monad


5. Monads, Kleisli Arrows, Comonads and other Rambling Thoughts


6. The idea that monads give a way to describe substitutions in a tree forms the basis for this and the next two posts: Variable substitution gives a...


7. Monads are Trees with Grafting


8. Where do monads come from?


9. From Monoids to Monads


10. Some thoughts on reasoning and monads


11. The Mother of all Monads


12. Beyond Monads
    

Fold and Unfold
I think this is one of the great applications of Category Theory to Computer Science. Structural recursion can be characterised really nicely in terms of F-algebras. That's cool. But even cooler is that when you dualise the definitions you get a great way to look at non-terminating computations on things like streams.

1. Data and Codata


2. Coalgebras and Automata


3. Purely functional recursive types in Haskell and Python

Commutative Monads and Vector Spaces
Trying to order these is tricky. I'm not sure I define the term commutative monad until the talk.

1. I realised a while back that the operation to build a vector space from a basis is a monad. In fact, like many well known algebraic structures, we get a commutative monad. Monads for vector spaces, probability and quantum mechanics pt. I


2. Monads, Vector Spaces and Quantum Mechanics pt. II


3. Trace Diagrams with Monads


4. A talk this time: Commutative Monads, Diagrams and Knots


5. And what happens when you try to use a non-commutative monad when a commutative monad is expected: Why isn't ListT a monad?

Comonads
I'm not sure the killer application for comonads has been found yet. But I do think they're good for things like dataflow and cellular automata fit the comonad model very well:

1. Evaluating cellular automata is comonadic


2. Comonadic Arrays


3. Comonads and reading from the future


4. The Monads Hidden Behind Every Zipper


5. Categories of polynomials and comonadic plumbing

Category Theory
And these are generally categorical articles

1. You Could Have Defined Natural Transformations


2. Reverse Engineering Machines with the Yoneda Lemma


3. A Yonedic Addendum


4. Applying the Yoneda lemma to memoize functions that at first seem unmemoizable: Memoizing Polymorphic Functions with High School Algebra and Quantifiers


5. Products, Limits and Parametric Polymorphism


6. Dinatural Transformations and Coends


7. The goal here was not to understand what Category Theory applies to Haskell, but how Haskell code can be interpreted in other categories: "What Category do Haskell Types and Functions Live In?"


8. A first step towards 2-category theory: The Interchange Law

---

Products, Limits and Parametric Polymorphism

> {-# LANGUAGE RankNTypes #-}

When I wrote about memoizing polymorphic types I mentioned that you can think of forall a. F(a) as the product over all types a of F(a), where F is some type level function. For example F might be a type constructor like []. That's not completely accurate, as I hope to now explain. Along the way we should get some insight into the meaning of the limit of a functor in a category.

Suppose we have two types, A and B. We can form their product (A, B). We have the two projections fst and snd and if we have an element x in (A, B) we know that there is no necessary relationship between fst x and snd x. We can freely choose x so that each of fst x and snd x can take on any values we like in A and B.

But now consider an element of forall a. F(a). For each concrete type X we have a projection π_X::forall a. F(a) -> F(X). So it looks like a product of all types. However, we can't freely choose elements of forall a. F(a) so as to get any element of F(X) we like for each choice of X. To demonstrate this, consider an element x of the type forall a. [a]. For any choice of X we get a projection. For example, picking X to be Int or String gives:

> p1 :: (forall a. [a]) -> [Int]
> p2 :: (forall a. [a]) -> [String]
> p1 x = x
> p2 x = x

We can draw a simple category diagram representing this:




However, forall a. [a] comes with a free theorem. For this particular type we have a free theorem that says that for any f :: X -> Y, fmap f (p1 x) == p2 x. For example consider the well known function show :: Int -> String. The free theorem tells us that this diagram commutes:




So if p1 x == [3] then p2 x == ["3"]. We have lost free choice. But we have lost a lot more freedom than this. We have a commuting triangle like this for absolutely any function f :: X -> Y. It should be clear that there is no way we can pick elements of our list to satisfy all of these constraints. So x must be the empty list.

Cones
This scenario of having one projection for each type has a name. It's an example of a cone. Let's borrow the definition from Wikipedia:

Let F:J→C be a functor. Let N be an object of C. A cone from N to F is a family of morphisms with one morphism for each X,

π_X:N→F(X)

so that for every morphism f:X→Y, the following diagram commutes:



For any Haskell functor F, the free theorem tells us that we have exactly these diagrams with forall a. F(a) playing the role of N. So forall a. F(a), with its projections to F(X), forms a cone.

Limits
If F is an instance of the Haskell Functor type class, ie. an endofunctor on Hask, then the type forall a. F(a) gives us a cone. But not just any old cone. I don't know how to prove this but I'm pretty sure it's true that the free theorems for a functor are the only non-trivial relations between F(X) and F(Y) that we're forced to obey. If that's true, then, in a sense, forall a. F(a) is the "biggest" type satisfying the free theorems. We can make this more precise by saying that for any cone N with associated projections π_X, we can can map it uniquely to forall a. F(a) so that the following diagram commutes:



This special kind of cone has a name. It's called a limit. In other words, ∀a. F(a) = lim F. In fact, this is exactly how Limit is defined in category-extras.

In a sense you can think of a limit of a functor in any category as being like a product for which a version of the free theorems for a functor holds.

Colimits
A dual story can be told for existential types and colimits. But to do this we need free theorems for existential types. I'll leave that until I've figured out a nice way to derive these free theorems...

Final words
I should have written this article before I wrote one on coends. Think of it as a prequel.

The fact that we don't have complete freedom of choice when defining polymorphic elements in Haskell is what we mean by 'parametric' polymorphism. Instead of specifying one individual value for each type we define the elements in a uniform way. In a language like C++ we can use template specialisation to freely construct a rule for getting a value from a type using 'ad hoc' polymorphism. That freedom comes at a price - it becomes harder to reason about polymorphism.

It's amazing that many definitions in category theory emerge naturally (pun fully intended) from the free theorems. I keep hoping that one day I'll find a paper on exactly what is going on here that I understand. The original free theorems paper is very uncategorical in its language.

---