Flat lists and free monads

Question

I am trying to convince myself that the List monad (the one with flat lists, concatenation of lists and map element-wise) is not a free monad (to be precise, the free monad associated to some functor T). As far as I understand, I should be able to achieve that by

• first finding a relation in the monad List between the usual operators fmap, join etc,

• then showing that this relation does not hold in any free monad over a functor T, for all T.

What is a peculiar relation that holds in the List monad, that sets it apart from the free monads? How can I handle step2 if I don't know what T is? Is there some other strategy to show that flat lists are not free?

As a side note, to dispell any terminology clash, let me remark that the free monad associated to the pair functor is a tree monad (or a nested list monad), it is not the flat List monad.

Edit: for people acquainted with the haskell programming language, the question can be formulated as follows: how to show that there is no functor T such that List a = Free T a (for all T and up to monad isomorphism)?

Answer 1

(Adapted from my post in a different thread.)

Here is a full proof why the list monad is not free, including a bit of context.

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. The task is to show that for no functor f, the monad Free f is isomorphic to the list monad.

The intuitive reason why this is true is because the join operation of the list monad (concatenation) doesn't merely graft expressions together, but flattens them.

More specifically, 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.

If the list monad would be 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).

Answer 2

If you're okay with the free monad being applied to a type in particular which seems to be the case given the way you consider the Nat example given in the comments, then List can indeed be described using Free:

type List a = Free ((,) a) ()

The underlying idea here is that a List a is a Nat where each Suc node has been labelled with an a (hence the use of the (a,) functor rather than the Identity one).

Here is a small module witnessing the isomorphism together with an example:

module FreeList where

import Data.Function
import Control.Monad.Free

type List a = Free ((,) a) ()

toList :: [a] -> List a
toList = foldr (curry Free) (Pure ())

fromList :: List a -> [a]
fromList = iter (uncurry (:)) . fmap (const [])

append :: List a -> List a -> List a
append xs ys = xs >>= const ys

example :: [Integer]
example = fromList $ (append `on` toList) [1..5] [6..10]