I plan a set of posts over the next few days on cool things you can do with free monads. This post is an attempt to get all the abstract nonsense out of the way first.
A Brief, Incomplete, and Mostly Wrong History of Programming Languages provides some background1990 - A committee formed by Simon Peyton-Jones, Paul Hudak, Philip Wadler, Ashton Kutcher, and People for the Ethical Treatment of Animals creates Haskell, a pure, non-strict, functional language. Haskell gets some resistance due to the complexity of using monads to control side effects. Wadler tries to appease critics by explaining that "a monad is a monoid in the category of endofunctors, what's the problem?"
A monoidal category is a category C equipped with an additional operation called the tensor product $\otimes$ which is a bifunctor from $C \times C \to C$, an identity object $I$, such that forall objects $x,y,z \in C$, $x \otimes I \cong I \otimes x \cong x$, and $(x \otimes y) \otimes z \cong x \otimes (y \otimes z)$.
Hask (the category of Haskell types...ignoring non-totality) is a monoidal category with product types (two-tuples) serving as the bifunctor, and the terminal object () serving as the identity object. Conveniently, two-tuples are also products in Hask.
In such a category, a monoid object $m$ is any object equipped with two morphism $$\eta : I \to m$$ $$\mu : m \otimes m \to m$$ such that some diagrams commute. We can express this in Haskell as and the diagrams correspond to three laws this class is of course, equivalent to the usual
We can construct a category where the objects are all the endofunctors over Hask, and the morphisms are all the natural transformations over these functors.
Aside: due to parametricity any function (in a large subset of Haskell) with a type like is a natural transformation.This category of endofunctors is a monoidal category with functor composition as the bifunctor and the identity functor so, then we should be able to define monoids in this category with the same laws as above. A moment of reflection and we see this is equivalent to which is what the monad class in Haskell should be.
Okay, so in Hask we also have coproducts of the form we also get coproducts in the cateogry of endofunctors Why is this useful? Well every Haskeller knows that given some type we can construct a monoid over that type which we can express perhaps more explitly as that is, as the coproduct of the tensor identity and the tensor product of a and List a. This is the "free monoid".
Lets translate this structure to funtors which is itself equivalent to lets define the monad instance that was easy, now okay, so the hard part is join. How do we define that?
Recall that so and now we have free monads!
nice
ReplyDelete