[Haskell-cafe] What are "free" Monads?
dan.doel at gmail.com
Sat Feb 27 05:03:21 EST 2010
On Saturday 27 February 2010 3:54:25 am Günther Schmidt wrote:
> I see the term "free monad" quite a lot, but don't really see an
> explanation what a free monad is. What sets a monad free and why in this
> day and age are there unfree monads?
Free structures originate (I think) in algebra. There you'll find talk of free
groups, free rings, free monoids, etc. The plain English explanation is that
you want to take some 'underlying' structure, and promote it into the
structure in question, but to do so in the simplest way possible in a sense.
In the algebra case, the underlying structure is typically a set, so you'll
have the free monoid over a set, the free group over a set, etc.
Monoids are pretty simple, so they're probably easiest to explain. So, monoids
A set M
A binary operation m : M x M -> M
An identity element e : M
and follow the laws:
a `m` (b `m` c) = (a `m` b) `m` c
e `m` a = a = a `m` e
So, for a free monoid over a set S, we want to produce a structure satisfying
the above, with an additional constraint that we need to have an:
i : S -> M
to inject elements of S into the monoid. And by "simplest" above, we mean
1) All the elements of M should be required to exist either by i, or by the
operations for the structure.
2) The only equational laws that should hold for the structure should be
those that are required to hold for structures of that type.
These may be kind of vague, and I apologize. They can be made more precise in
category theory (at least). So, for the above rules, we get that the free
monoid over a set is the monoid of lists of elements of that set with
concatenation and nil.
M = [S]
e = 
m = (++)
i = \x -> [x] -- \x -> x : 
 ++ xs = xs = xs ++ 
xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
In category theory, this is usually presented in terms of adjoint functors.
What you do is specify a "forgetful" or "underlying" functor, from, say, the
category of monoids to the category of sets. Then, a left adjoint to that
functor is called (I believe) the free monoid functor, and it takes sets to
the free monoid thereover. I don't really have the wherewithal to give an
explanation of adjoint functors, but adjunctions are what capture the two
rules for "free" things above.
So, now we want free monads over a (endo)functor F. As it turns out, monads
are monoid objects in the category of endofunctors over a category, which is a
generalization of the above monoids to categories other than sets. So, we can
hopefully use the above intuitive idea of a free monoid to figure out what
might be going on with free monads.
So, first we have an endofunctor F which is going to be analogous to the
underlying set. And we'll need some type of injection
i : F -> M
M being the functor part of the free monad over F. But arrows in the category
in question are natural transformations, so in Haskell, this would be more
i :: forall a. F a -> M a
Monads are also required to have a couple operations:
return :: forall a. a -> M a
join :: forall a. M (M a) -> M a
And they should satisfy some monad laws. I can't explain to you how to figure
out what M, return and join should be, because I don't know how myself; I'm
kind of winging it at this point. But Daniel Peebles has given the right
answer. It's datatype:
data M a = Return a | Roll (F (M a))
return = Return
join (Return m) = m
join (Roll fmm) = Roll (fmap join fmm)
i f = Roll (fmap Return f)
-- this should look vaguely similar to to \x -> x : 
which, you might notice, is similar in character to the free monoid above. In
the free monoid, you can inject elements of the set, and you can multiply
together lists to get arbitrarily long strings of elements of the underlying
set. In the free monad, there's a way to 'inject' the functor into the monad,
and you can 'multiply' in the monad to get arbitrarily deep composition
'strings' of F (by repeatedly Rolling).
There are also cofree structures, as was mentioned. The difference is that
while free functors are left adjoints to underlying functors, cofree functors
are right adjoints. I don't have much to say beyond that, though.
Anyhow, hope that gave some insight.
More information about the Haskell-Cafe