列表 monad 不是免费的 monad，但是……

Question

在One Monad to Prove Them All的第 12 页上，写道“ [容器]的一个突出例子是列表数据类型。列表可以由列表的长度和列表中映射位置的函数来表示”。

起初我认为这个容器上的免费 monad 与列表 monad 是同构的。

但在第 12 页上，写道“列表 monad 不是自由 monad，因为列表 monad 与自由 monad 的实例不同构”。

那么上面容器上的free monad是什么呢？它与什么同构？为什么它不与列表单子同构？可以通过商使其同构吗？

Answer 1

我认为人们应该小心一点。

我不认为 ifM是一个自由 monad，那么应用自由 monad 构造可以让你返回与 同构的东西M。所以你的问题“什么是自由单子”实际上与“什么函子是自由单子？”X无关。X为了证明 monad不是一个自由的 monad，我们唯一需要做的就是展示一些对monad 定律M来说正确但不隐含的等式——因为自由 monad 构造的意义在于它保证了 monad 定律而不是任何东西。别的。M

这是对列表执行此操作的一种方法：

f False = ""
f True = "x"

g False = "x"
g True = ""

is = [False, True]

现在is >>= f= is >>= g(= "x") 即使f!= g。

一个单独的问题是，通过将自由构造应用于列表，您会得到什么单子。作为一种直觉，思考自由单子构造的一种方法是，它是它所转换的事物的任意（且异构）深度嵌套版本。对于列表，这意味着像这样的值

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

将成为自由建设的成员。如果您稍微考虑一下，您会发现另一种思考方式是，将其视为一棵树，其叶子（仅）有数据，并且每个内部节点允许任意数量的子节点。

只是为了好玩，我们可以仔细检查我们是否没有验证之前的相等性。这次我们得到

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

那么我们就可以出发了。