The list monad is not a free monad but …-CodePudding

On page 12 of One Monad to Prove Them All, it is written that "a prominent example [of container] is the list data type. A list can be represented by the length of the list and a function mapping positions within the list".

At first I thought that the free monad on this container would be isomorphic the list monad.

But on page 12, it is written that "the list monad is not a free monad in the sense that the list monad is not isomorphic to an instance of the free monad".

So what is the free monad on the above container? What is it isomorphic to? Why isn't it isomorphic to the list monad? Can it be made isomorphic by quotient?

CodePudding user response：

I think one should be a bit careful.

I don't think it's the case that if M is a free monad, then applying the free monad construction gets you back something isomorphic to M. So your question of "what is the free monad on X" is actually not related to "what functor is X the free monad of?". To show that monad M is not a free monad, the only thing we need to do is exhibit some equality that's true for M but not implied by the monad laws -- since the meaning of the free monad construction is that it guarantees the monad laws and nothing else.

Here's one way to do that for lists:

f False = ""
f True = "x"

g False = "x"
g True = ""

is = [False, True]

Now is >>= f = is >>= g (= "x") even though f != g.

A separate question is what monad you get by applying the free construction to lists. As an intuition, one way to think about the free monad construction is that it is an arbitrarily (and heterogeneously) deeply nested version of the thing it transforms. For lists, that means values like

[[[0], [1, [2, 3], 4]], [5,6,7]]

would be members of the free construction. If you think about that a bit, you'll see that another way to think of this is as a tree with data at its leaves (only) and any number of children being allowed at each internal node.

Just for fun, we can double check that we don't validate the equality from before. This time we get

is >>= f = ["", "x"]
is >>= g = ["x", ""]

so we're good to go.