A proof that the list monad is not a free monad

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-... [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...
participants (1)
-
Ingo Blechschmidt