平铺列表和自由Monad

Question

我试图说服自己，List单子（使用平面列表、列表连接和元素映射）不是自由单子（确切地说，与某些函子T相关联的自由单子）。据我所知，我应该能通过以下步骤来实现：

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

• 然后证明这个关系在任何functor T的自由单子中都不成立，对于所有T。

List单子中存在一种奇特的关系，使得它与自由单子有所区别。如果我不知道T是什么，我该如何处理第二步？是否有其他策略可以显示出平面列表不是自由的？

作为一个副笔，为了消除任何术语冲突，让我注意一下：与一对函子相关联的自由单子是一个树单子（或嵌套列表单子），而不是平面List单子。

编辑：对于熟悉Haskell编程语言的人，问题可以这样表述：如何显示不存在functor T，使得List a = Free T a（对于所有T和monad同构）？

- stackman

---

自由单子是广义的外部标记树；a出现在Return构造函数中，而不是Free构造函数中。列表是内部标记的；它们沿着整个列表都有a，而不仅仅在叶子节点上。 - Benjamin Hodgson

@Hodgson，我不确定我理解你的评论。例如，整数的幺半群可以被实现为与一个对象（和一个单一的态射）的范畴上的恒等函子相关联的自由单子。但这并不代表所有自由单子都是树形结构。 - stackman

你是在指 type Nat = Free Identity () 吗？这是一个分支因子为1的树（因为 Identity a 包含一个 a）。Free ((->) r) 是一个分支因子为 r 的树，Free (Const Void) 是一个分支因子为0的树。等等。 - Benjamin Hodgson

是的，这就是重点。考虑整数（数学上的整数，通常实现为大整数），它们可以被构建为树或自由单子，正如你刚才提到的那样。但为什么对于平面列表来说却不是这样呢？我不是要求哲学上的答案，而是要一些明确的结构（最好是关系），表明List单子不能同构于自由单子。 - stackman

Answer 1

（改编自我在另一个帖子中的回答。）

以下是完整的证明，说明列表单子不是自由单子，包括一些背景知识。

回想一下，我们可以为任何函子f构建自由单子：

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

直观地说，Free f a 是具有类型为 a 的叶子节点的 f 形树的类型。合并操作仅仅是将树连接在一起而不执行任何进一步的计算。本篇文章中形如 (Roll _) 的值被称为“非平凡”的。任务是证明对于任何 functor f，单子函子 Free f 都不等同于列表 monad。

这个结论正确的直觉原因是列表 monad 的合并操作（连接）不仅仅将表达式接在一起，而是将它们展平。

更具体地说，在任何 functor 上的自由单子函子中，将一个非平凡的 action 绑定到任何函数的结果总是非平凡的。

(Roll _ >>= _) = Roll _

这可以直接从自由单子的(>>=)定义中检查。

如果列表单子作为单子与某个函子的自由单子同构，则同构仅将单例列表[x]映射到形如(Pure _)的值，而将所有其他列表映射到非平凡的值。这是因为单子同构必须与“返回”和return x一起交换，列表单子中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）。

- Ingo Blechschmidt

Answer 2

如果您认为自由单子应用于特定类型是可以接受的，这似乎是情况，因为您考虑评论中给出的Nat示例，则可以使用Free来描述List:

type List a = Free ((,) a) ()

这里的基本思想是，一个 List a 是一个带有标签为 a 的 Suc 节点的 Nat（因此使用了 (a,) 函子而不是 Identity 函子）。

以下是一个小模块，用于证明同构以及一个示例：

module FreeList where

import Data.Function
import Control.Monad.Free

type List a = Free ((,) a) ()

toList :: [a] -> List a
toList = foldr (curry Free) (Pure ())

fromList :: List a -> [a]
fromList = iter (uncurry (:)) . fmap (const [])

append :: List a -> List a -> List a
append xs ys = xs >>= const ys

example :: [Integer]
example = fromList $ (append `on` toList) [1..5] [6..10]

- gallais

---

请注意，List a 的绑定方式与 [] 的不同。因此，您可能需要重新考虑接受将 Free f 应用于像 Nat 这样的固定类型。 - gallais

太聪明了！令人惊讶的是，<< Free 运算符对应于追加列表。如果这个结构是一个单子同构，那么 Free.(<<) 将对应于标准的 [].(<<) 运算符，这与追加非常不同。但在某些情况下它确实有效，即当 a = () 时，我们恢复 Nat。 - stackman