Ingo Blechschmidt iblech at web.de
Mon Jan 23 12:04:00 UTC 2017

```Dear lovers of generalized abstract nonsense,

recall that we can construct, for any functor f, the free monad over f:

data Free f a = Pure a | Roll (f (Free f a))

Intuitively, Free f a is the type of f-shaped trees with leaves of type a.
The join operation merely grafts trees together and doesn't perform any
further computations. Values of the form (Roll _) shall be called
"nontrivial" in this posting.

Some of the usual monads are in fact free monads over some functor:

* The Tree monad is the free monad over the functor Pair, where
data Pair a = MkPair a a. The intuition as Pair-shaped trees
is most strong in this example. Every parent node has a pair of
children.

* The Maybe monad is the free monad over the functor Unit, where
data Unit a = MkUnit. In the graphical picture parent nodes have a
Unit of children, so no children at all. So there are exactly two
Unit-shaped trees: the tree consisting only of a leaf (corresponding
to Just _) and the three consisting of a childless parent node
(corresponding to Nothing).

* The Identity monad is the free monad over the functor Void,
where Void a is a type without constructors.

* The Writer [r] monad is the free monad over the functor (r,).
In an (r,)-shaped tree, a parent node is decorated with a value
of type r and has exactly one child node. Traversing such a path
yields a list of r's and a leaf value of type a, so in total
a value of type ([r],a) = Writer r a.

(In particular, Free (r,) () is isomorphic to [r]. This observation
led to the claim that the list monad is free. But this claim is false
and indeed doesn't follow from the observation. To show that a monad m
is free, one has to exhibit a monad isomorphism forall a. m a -> Free f a
for some functor f. In contrast, exhibiting an isomorphism of m a with
Free (f a) () is neither sufficient nor required.)

Even more monads are quotients of free monads. For instance, State s is
a quotient of Free (StateF s), where

data StateF s a = Put s a | Get (s -> a).
-- NB: This functor is itself a free functor over a type constructor
-- which is sometimes called StateI , rendering Free (StateF s) what
-- Oleg and Hiromi Ishii call a "freer monad" .

The quotient is exhibited by the following monad morphism, which gives
semantics to the purely syntactical values of the free monad.

run :: Free (StateF s) a -> State s a
run (Pure x)         = return x
run (Roll (Put s m)) = put s >> run m
run (Roll (Get k))   = get >>= run . k

This point of view is the basis of the operational package by apfelmus 
and is also talked about in an StackOverflow thread . It's the main
reason why free monads are useful in a programming context.

So, is the list monad a free monad? Intuitively, it's not, because the
join operation of the list monad (concatenation) doesn't merely graft
expressions together, but flattens them .

Here is a proof that the list monad is not free. I'm recording it since
I've been interested in a proof for quite some time, but searching for
it didn't yield any results. The threads  and  came close, though.

In the free monad over any functor, the result of binding a nontrivial
action with any function is always nontrivial, i.e.

(Roll _ >>= _) = Roll _

This can be checked directly from the definition of (>>=) for the free
morphism to Maybe, see .

functor, the isomorphism would map only singleton lists [x] to values of
the form (Pure _) and all other lists to nontrivial values. This is
because monad isomorphisms have to commute with "return" and return x
is [x] in the list monad and Pure x in the free monad.

These two facts contradict each other, as can be seen with the following
example:

do
b <- [False,True]  -- not of the form (return _)
if b
then return 47
else []
-- The result is the singleton list , so of the form (return _).

After applying a hypothetical isomorphism to the free monad over some
functor, we'd have that the binding of a nontrivial value (the image
of [False,True] under the isomorphism) with some function results in a
trivial value (the image of , i.e. return 47).

Cheers,
Ingo