[Haskell-cafe] A proof that the list monad is not a free monad

[Ingo Blechschmidt]

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 Partiality monad is the free monad over Maybe.

* 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 [1], rendering Free (StateF s) what
    -- Oleg and Hiromi Ishii call a "freer monad" [2].

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 [1]
and is also talked about in an StackOverflow thread [3]. 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 [4].

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 [3] and [5] 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
monad or alternatively with Reid Barton's trick of exploiting a monad
morphism to Maybe, see [3].

If the list monad was isomorphic-as-a-monad to the free monad over some
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 [47], 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 [47], i.e. return 47).

Cheers,
Ingo

[1] http://projects.haskell.org/operational/Documentation.html
[2] http://okmij.org/ftp/Haskell/extensible/more.pdf
[3] http://stackoverflow.com/questions/14641864/what-monads-can-be-expressed-as-free-over-some-functor
[4] https://hackage.haskell.org/package/free-4.12.4/docs/Control-Monad-Free.html
[5] https://www.reddit.com/r/haskell/comments/50zvyb/why_is_liststate_not_a_free_monad/