9

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?

Bob
  • 1,713
  • 10
  • 23

1 Answers1

14

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.

Daniel Wagner
  • 145,880
  • 9
  • 220
  • 380
  • `Free []` is isomorphic to `Rose`, right? – n. m. could be an AI Feb 22 '22 at 20:04
  • `Free []` can't (IIUC) represent an empty rose tree, so it depends on what your definition of `Rose` is. – chepner Feb 22 '22 at 20:05
  • @chepner `data Rose a = Root a | Tree [Rose a]`, looks pretty identical to `data Free f a = Pure a | Roll (f (Free f a))`, no? – n. m. could be an AI Feb 22 '22 at 20:16
  • With that definition, sure. But one could also choose `data Rose a = Empty | Tree a [Rose a]`, that allows for an empty tree, which doesn't line up with `Free []`. (Though now you have multiple representations for the same tree, like `Tree 1 []` vs `Tree 1 [Empty]` vs ....) – chepner Feb 22 '22 at 20:19
  • "since the meaning of the free monad construction is that it guarantees the monad laws and nothing else." hence Cyril's quote: [*To be free means to violate as many laws as possible*](https://twitter.com/elvecent_not/status/1314923693320044544) – Iceland_jack Feb 22 '22 at 20:23
  • @n.1.8e9-where's-my-sharem. Sure. That's why I say "another way to think of this is as a tree with data at its leaves". – Daniel Wagner Feb 22 '22 at 20:44