问题描述
我试图说服自己，List Monad(具有平面列表、列表连接和映射元素的Monad)不是自由Monad(准确地说，是与某个函数器T关联的自由Monad)。据我所知，我应该能够在
年实现这一目标。首先在单体列表中查找常用运算符FMAP、Join等之间的关系
然后证明了这种关系不存在于函子T上的任何自由单子中，对于所有T
列表单子中的特殊关系是什么，使其有别于自由单子？如果我不知道T是什么，我怎么处理第二步？有没有其他策略来表明平面列表不是免费的？顺便提一句，为了消除术语冲突，让我说明一下，与配对函数器关联的自由monad是树monad(或嵌套列表monad)，它不是平面列表monad。
编辑：对于熟悉Haskell编程语言的人来说，问题可以表述为：如何证明没有函数符T使得list a=Free Ta(对于所有T和单数同构)？
推荐答案
(改编自我的post in a different thread。)
下面是List Monad不是免费的完整证明，包括一些上下文。
回想一下，我们可以为任何函子f构造f上的自由单体：
data Free f a = Pure a | Roll (f (Free f a))
直观地说，Free f a是具有a型叶片的f型树。
连接操作只是将树嫁接在一起，而不执行任何
进一步的计算。(Roll _)形式的值应被调用
在这篇帖子中"不是微不足道的"。证明了对于无函子f，单子Free f与列表单子同构。
(Roll _ >>= _) = Roll _
(>>=)的定义中免费查看
Monad。
如果列表单子同构于某些上的自由单子
函数器，同构将仅将单个列表[x]映射到
形式(Pure _)和所有其他列表到非平凡的值。这是
因为单子同构必须与"返回"和return x交换
[x]在列表单子中，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 _).
在将假设同构应用于一些
函数器，我们将拥有一个非平凡值(图像)的绑定
[False,True]在同构下)与某些函数产生一个
平凡值([47]图片，即return 47)。