list - 平面列表和自由单子(monad)

Question

我试图说服自己 List monad(具有平面列表、列表串联和按元素映射的 monad)不是自由 monad(准确地说，是与某个仿函数 T 关联的自由 monad)。据我了解，我应该能够通过

• 首先在 monad List 中找到常用运算符 fmap、join 等之间的关系，

• 然后表明对于所有 T，此关系在仿函数 T 上的任何自由单子(monad)中都不成立。

什么是 List monad 中的特殊关系，将它与自由 monad 区分开来？如果我不知道 T 是什么，我该如何处理 step2？有没有其他策略可以表明平面列表不是免费的？

作为旁注，为了消除任何术语冲突，让我指出与对仿函数关联的自由 monad 是树 monad(或嵌套列表 monad)，它不是平面 List monad。

编辑:对于熟悉 haskell 编程语言的人来说，问题可以表述如下:如何证明不存在仿函数 T 使得 List a = Free T a(对于所有 T以及单子(monad)同构)？

Answer 1

(改编 self 的 post in a different thread 。)

这是为什么列表 monad 不是免费的完整证明，包括一些上下文。

回想一下，我们可以为任何仿函数 f 构造 f 上的自由单子(monad):

data Free f a = Pure a | Roll (f (Free f a))

直觉上，Free f a 是一种 f 型树，叶子类型为 a。join 操作只是将树嫁接在一起，并不执行任何操作进一步的计算。应调用 (Roll _) 形式的值这篇文章中的“不平凡”。任务是证明对于没有仿函数 f，monad Free f 与列表 monad 同构。

之所以如此，直觉上是因为列表 monad 的连接操作(串联)不仅仅是嫁接表达式放在一起，但将它们展平。

更具体地说，在任何仿函数上的自由单子(monad)中，绑定(bind)一个非平凡的结果任何功能的 Action 总是不平凡的，即

(Roll _ >>= _) = Roll _

这可以直接从 (>>=) 的定义中免费检查单子(monad)。

如果列表 monad 同构于自由 monad仿函数，同构只会将单例列表 [x] 映射到的值形式 (Pure _) 和所有其他列表为非平凡的值。这是因为 monad 同构必须通过 "return"和 return x 交换是列表 monad 中的 [x] 和自由 monad 中的 Pure x。

这两个事实相互矛盾，如下图所示示例:

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 _).

在对一些自由单子(monad)应用假设同构之后仿函数，我们会有一个非平凡值的绑定(bind)(图像[False,True] 在同构下)与一些函数结果普通值([47] 的图像，即 return 47)。