[Haskell-cafe] A proof that the list monad is not a free monad
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 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/
More information about the Haskell-Cafe
mailing list