带有可遍历的任意单子的组合总是单子吗？答案

【问题标题】：Is the composition of an arbitrary monad with a traversable always a monad?带有可遍历的任意单子的组合总是单子吗？
【发布时间】：2017-07-06 05:01:31
【问题描述】：

如果我有两个 monad m 和 n，并且 n 是可遍历的，我是否一定有一个复合 m-over-n monad？

更正式地说，这是我的想法：

import Control.Monad
import Data.Functor.Compose

prebind :: (Monad m, Monad n) =>
         m (n a) -> (a -> m (n b)) -> m (n (m (n b)))
mnx `prebind` f = do nx <- mnx
                     return $ do x <- nx
                                 return $ f x

instance (Monad m, Monad n, Traversable n) => Monad (Compose m n) where
  return = Compose . return . return
  Compose mnmnx >>= f = Compose $ do nmnx <- mnmnx `prebind` (getCompose . f)
                                     nnx  <- sequence nmnx
                                     return $ join nnx

当然，这种类型检查，我相信适用于我检查过的一些情况（Reader over List，State over List）——例如，组合的“monad”满足 monad 法则——但我不确定这是否是通用将任何 monad 分层到可遍历的方法。

【问题讨论】：

Here 是一本很棒的书，它从范畴论的角度涵盖了这个主题（特别是 p257 “分配律”），并给出了一个相对（从点已经知道范畴论的人的观点...）如果M 和N 是单子，则M . N 是单子的必要条件的简单证明。 Here 是另一个问题，它与您给出的代码略有不同 - 也许它会是一个更有用的起点。
剧透：是的。
有点可悲，如果回想起来很明显，以这种方式在 List 上分层 State 不会给你 非确定性状态，这与你分层 StateT 时发生的情况相反超过列表。
如果Traversable n 是完成这项工作的完美约束，那么如果Data.Functor.Compose 有实例就好了。也许你应该建议它？我绝对可以想到我可能会使用它的上下文。
是的，这就是为什么我开始说“如果 Traversable n 是完美的约束……”也许这有点晦涩。我们当然不想要多个实例，只需要最一般（正确）的实例。

标签： haskell monads

【解决方案1】：

不，它并不总是单子。您需要额外的兼容性条件来关联两个 monad 的 monad 操作和分配律 sequence :: n (m a) -> m (n a)，例如在 Wikipedia 上描述的那样。

Your previous question给出了一个不满足兼容条件的例子，即

S = m = []，单元 X -> SX 将 x 发送到 [x]；

T = n = (->) Bool，或等价的 TX = X × X，单元 X -> TX 将 x 发送到 (x,x)。

维基百科页面右下角的图没有通勤，因为组合 S -> TS -> ST 将xs :: [a] 发送到(xs,xs)，然后发送到从xs 抽取的所有对的笛卡尔积；而右侧的映射 S -> ST 将 xs 发送到仅由 (x,x) 对组成的“对角线”，用于 xs 中的 x。这也是导致您提出的 monad 不满足其中一个单位定律的问题。

【讨论】：

我想我遗漏了一些明显的东西。由于[] 是可遍历的，但(->) r 不是，因此上面的方法将提供一种派生Reader-over-List（或Set）monad 的方法，而不是List-over-Reader monad，这是我的上一个问题是问的。
抱歉，我现在明白为什么(->) Bool 确实是可遍历的。对于任何有限的r，(->) r 是否可遍历（沿着您链接到的问题中暗示的行）？
(->) Bool 或 (->) r 对于任何有限类型 r 是可遍历的，因为它等效于 |r|-tuple。
快速跟进。您链接的维基文章中的 if 是文字 if （分配律的存在是复合函子为单子的充分条件）还是数学家的 if（充分，必要）？
我检查了右下图对于 ST 以特定方式成为 monad 是必要的（它遵循 S、T 和 ST 的单位定律）。我猜其他图可以以类似的方式被证明是必要的，因为它们也是态射与 ST 之间的方程，但我没有看到任何特别的理由来先验地认为它们必须 i> 是必要的。

【解决方案2】：

补充几点，让Reid Barton's general answer 和您的具体问题之间的联系更加明确。

在这种情况下，根据join 计算出您的Monad 实例真的很值得：

join' ::  m (n (m (n b))) -> m (n b)
join' = fmap join . join . fmap sequence

通过在适当的位置重新引入compose/getCompose 并使用m >>= f = join (fmap f m)，您可以验证这确实等同于您的定义（请注意，您的prebind 等于该等式中的fmap f） .

这个定义使得用图表验证定律变得很容易¹。这是join . return = id 即(fmap join . join . fmap sequence) . (return . return) = id：

3210 MT id MT id MT id MT ----> ----> ----> rT2 | | rT1 | | rT1 | | ID rM3 V V rM3 V V V V ----> ----> ----> MTMT sM2 MMTT jM2 MTT jT0 MT

整个矩形是单子定律：

中号 ----> RM1 | | ID 五五 ----> 毫米 jM0 米

忽略两个正方形中必然相同的部分，我们看到最右边的两个正方形等于相同的定律。（考虑到它们拥有的所有id 边，将这些称为“正方形”和“矩形”当然有点愚蠢，但它更适合我有限的 ASCII 艺术技能。）不过，第一个正方形相当于 @987654333 @，这是里德巴顿提到的维基百科页面右下角的图表......

中号 ----> rT1 | | rT0 五五 ----> TM SM1 MT

...正如 Reid Barton 的回答所显示的那样，这并不是给定的。

如果我们对join . fmap return = id 法则应用相同的策略，右上方的图表sequence . fmap return = return 就会出现——然而，这本身并不是问题，因为这只是（直接后果的）Traversable的身份法则。最后，对join . fmap join = join . join 法则做同样的事情，会使另外两个图表——sequence . fmap join = join . fmap sequence . sequence 和sequence . join = fmap join . sequence . fmap sequence——出现。

脚注：

简写图例：r 是 return，s 是 sequence，j 是 join。函数缩写后的大写字母和数字消除了所涉及的 monad 及其引入或更改层的位置结束于 -- 在s 的情况下，它指的是最初是内层，因为在这种情况下，我们知道外层始终是T。层从下到上编号，从零开始。通过在第一个函数下方写第二个函数的简写来表示组合。

【讨论】：