是否`数据 PoE a = 空 |对 a a` a monad？答案

【问题标题】：Is `data PoE a = Empty | Pair a a` a monad?是否`数据 PoE a = 空 |对 a a` a monad？
【发布时间】：2018-09-19 09:48:51
【问题描述】：

这个问题来自这个答案 example of a functor that is Applicative but not a Monad: 据称，

data PoE a = Empty | Pair a a deriving (Functor,Eq)

不能有 monad 实例，但我看不到：

instance Applicative PoE where
    pure x = Pair x x
    Pair f g <*> Pair x y = Pair (f x) (g y)
    _        <*> _        = Empty
instance Monad PoE where
    Empty    >>= _ = Empty
    Pair x y >>= f = case (f x, f y) of 
                       (Pair x' _,Pair _ y') -> Pair x' y'
                       _ -> Empty

我认为这是一个 monad 的真正原因是它与 Maybe (Pair a) 和 Pair a = P a a 同构。它们都是 monad，都是可遍历的，所以它们的组合也应该形成一个 monad。 Oh, I just found out not always.

哪个反例不符合哪个单子法则？（以及如何系统地找出它？）

编辑：我没想到对这个问题有这么大的兴趣。现在我必须下定决心，是否接受“系统地”部分的最佳示例或最佳答案。

同时，我想看看join 是如何为更简单的Pair a = P a a 工作的：

                   P
          ________/ \________
         /                   \
        P                     P
       / \                   / \
      1   2                 3   4

它总是采用外部路径，产生P 1 4，通常称为矩阵表示中的对角线。对于 monad 关联我需要三个维度，树可视化效果更好。取自 chi 的回答，这是 join 的失败示例，以及我如何理解它。

                  Pair
          _________/\_________
         /                    \
       Pair                   Pair
        /\                     /\
       /  \                   /  \
    Pair  Empty           Empty  Pair
     /\                           /\
    1  2                         3  4

现在您可以通过首先折叠较低级别来执行join . fmap join，因为join . join 从根折叠。

【问题讨论】：

我确定您已经注意到了这一点，但回复者确实回复了您对您链接的帖子的评论。我个人无法一眼就构建出符合他描述的反例，但我想让你知道他的评论。
使应用程序成为 Monad 的原因是能够压缩它（使用连接）并将一对转换为一对。就像您在示例中所做的那样，您不能在不丢失一些元素（从 4 到 2）的情况下做到这一点。那将触犯法律。例如Pair (Pair 1 2) Empty >>= return 返回空。这不好。
我在TIO 中运行它，但我没有收到Empty
我的意思是>>= id
有趣的是，非常相似的类型实际上是一个 monad：stackoverflow.com/questions/43684258/…

标签： haskell functional-programming monads

【解决方案1】：

显然，它不是单子。单子“join”法则之一是

join . join = join . fmap join

因此，根据上面的规律，这两个输出应该相等，但事实并非如此。

main :: IO ()
main = do
  let x = Pair (Pair (Pair 1 2) Empty) (Pair Empty (Pair 7 8))
  print (join . join $ x)
  -- output: Pair 1 8
  print (join . fmap join $ x)
  -- output: Empty

问题是

join x      = Pair (Pair 1 2) (Pair 7 8)
fmap join x = Pair Empty Empty

对它们执行额外的join 并不会使它们相等。

如何系统地找出答案？

join . join 的类型为 m (m (m a)) -> m (m a)，所以我从三重嵌套的 Pair-of-Pair-of-Pair 开始，使用数字 1..8。那工作得很好。然后，我尝试在里面插入一些Empty，很快就找到了上面的反例。

这种方法是可行的，因为 m (m (m Int)) 内部只包含有限数量的整数，而且我们只有构造函数 Pair 和 Empty 可以尝试。

对于这些检查，我发现join 定律比>>= 的关联性更容易测试。

【讨论】：

玩得很好。您可以通过仔细定位Empty 使其消失。好答案！

【解决方案2】：

QuickCheck 立即找到关联性的反例。

{-# LANGUAGE DeriveFunctor #-}

import Test.QuickCheck

data PoE a = Empty | Pair a a deriving (Functor,Eq, Show)

instance Applicative PoE where
    pure x = Pair x x
    Pair f g <*> Pair x y = Pair (f x) (g y)
    _        <*> _        = Empty
instance Monad PoE where
    Empty    >>= _ = Empty
    Pair x y >>= f = case (f x, f y) of 
                       (Pair x' _,Pair _ y') -> Pair x' y'
                       _ -> Empty

instance Arbitrary a => Arbitrary (PoE a) where
  arbitrary = oneof [pure Empty, Pair <$> arbitrary <*> arbitrary]

prop_assoc :: PoE Bool -> (Bool -> PoE Bool) -> (Bool -> PoE Bool) -> Property
prop_assoc m k h =
  ((m >>= k) >>= h) === (m >>= (\a -> k a >>= h))

main = do
  quickCheck $ \m (Fn k) (Fn h) -> prop_assoc m k h

输出：

*** Failed! Falsifiable (after 35 tests and 3 shrinks):    
Pair True False
{False->Pair False False, True->Pair False True, _->Empty}
{False->Pair False True, _->Empty}
Pair False True /= Empty

【讨论】：

搞笑，我用了Bool，没找到反例；我想也许是因为一些异常，法律只适用于布尔。但我想这只是随机性的不完美..

【解决方案3】：

由于您对如何系统地执行此操作感兴趣，以下是我如何找到一个使用 quickcheck 的反例：

{-# LANGUAGE DeriveFunctor #-}

import Control.Monad ((>=>))
import Test.QuickCheck

-- <your code>

定义任意实例以生成随机PoEs。

instance (Arbitrary a) => Arbitrary (PoE a) where
    arbitrary = do
      emptyq <- arbitrary
      if emptyq
        then return Empty
        else Pair <$> arbitrary <*> arbitrary

并测试单子定律：

prop_right_id m = (m >>= return) == m
    where
    _types = (m :: PoE Int)

prop_left_id fun x = (return x >>= f) == f x
    where
    _types = fun :: Fun Int (PoE Int)
    f = applyFun fun

prop_assoc fun gun hun x = (f >=> (g >=> h)) x == ((f >=> g) >=> h) x
    where
    _types = (fun :: Fun Int (PoE Int),
              gun :: Fun Int (PoE Int),
              hun :: Fun Int (PoE Int),
              x :: Int)
    f = applyFun fun
    g = applyFun gun
    h = applyFun hun

我没有遇到任何关于身份法则的失败，但prop_assoc 确实生成了一个反例：

ghci> quickCheck prop_assoc
*** Failed! Falsifiable (after 7 tests and 36 shrinks):
{6->Pair 1 (-1), _->Empty}
{-1->Pair (-3) (-4), 1->Pair (-1) (-2), _->Empty}
{-3->Empty, _->Pair (-2) (-4)}
6

并不是说它对理解为什么会发生故障非常有帮助，它确实为您提供了一个开始的地方。如果我们仔细看，我们会看到我们正在将(-3) 和(-2) 传递给第三个函数； (-3) 映射到 Empty 和 (-2) 映射到 Pair，所以我们不能遵循 PoE 组成的两个单子中的任何一个的定律。

【讨论】：

【解决方案4】：

这种潜在的Monad实例可以简洁地描述为“走对角线”。如果我们使用join 演示文稿，则更容易理解为什么。这是您提到的Pair 类型的join：

join (P (P a00 a11) (P a10 a11)) = P a00 a11

但是，对于固定长度（或无限）列表，仅保证对角线提供合法的join。那是因为结合律：

join . join = join . fmap join

如果列表列表中的第 n 个列表没有第 n 个元素，则会导致对角线被修剪：它将在其第 n 个元素之前结束。 join . join 首先采用外对角线（列表列表of 列表），而join . fmap join 首先采用内对角线。对于不在外对角线上的不够长的最内层列表可能会修剪join . fmap join，但它不可能影响join . join。（这会更容易用图片而不是文字来展示。）

您的PoE 是一个类似列表的类型，没有固定长度（长度为零或二）。事实证明，取它的对角线并没有给我们一个 monad，因为上面讨论的潜在问题实际上阻碍了我们（如 chi's answer 所示）。

补充说明：

这正是ZipList 不是单子的原因：活泼的行为相当于采用对角线。
无限列表与自然函数同构，固定长度列表与自然函数同构直到适当的值。这意味着您可以从函数实例中为它们获取一个Monad 实例——而您获得的实例再次相当于采用对角线。
Once upon a time I got confused about this exact issue.

【讨论】：

【解决方案5】：

（将此作为单独的答案发布，因为它与我的另一个答案几乎没有重叠。）

我认为这是一个单子的真正原因是它与Maybe (Pair a) 和Pair a = P a a 同构。它们都是 monad，都是可遍历的，所以它们的组合也应该形成一个 monad。 Oh, I just found out not always.

单子m-over-n与n可遍历的条件是：

-- Using TypeApplications notation to make the layers easier to track.
sequenceA @n @m . pure @n = fmap @m (pure @n)
sequenceA @n @m . fmap @n (join @m)
    = join @m . fmap @m (sequenceA @n @m) . sequenceA @n @m
sequenceA @n @m . join @n
    = fmap @m (join @n) . sequenceA @n @m . fmap @n (sequenceA @n @m)

（也有sequenceA @n @m . fmap @n (pure @m) = pure @m，但总是这样。）

在我们的例子中，我们有 m ~ Maybe 和 n ~ Pair。 Pair 的相关方法定义为：

fmap f (P x y) = P (f x) (f y)
pure x = P x x
P f g <*> P x y = P (f x) (g y)
join (P (P a00 a01) (P a10 a11)) = P a00 a11 -- Let's pretend join is a method.
sequenceA (P x y) = P <$> x <*> y

让我们检查第三个属性：

sequenceA @n @m . join @n
    = fmap @m (join @n) . sequenceA @n @m . fmap @n (sequenceA @n @m)

-- LHS
sequenceA . join $ P (P a00 a01) (P a10 a11)
sequenceA $ P a00 a11
P <$> a00 <*> a11 -- Maybe (Pair a)

-- RHS
fmap join . sequenceA . fmap sequenceA $ P (P a00 a01) (P a10 a11)
fmap join . sequenceA $ P (P <$> a00 <*> a01) (P <$> a10 <*> a11)
fmap join $ P <$> (P <$> a00 <*> a01) <*> (P <$> a10 <*> a11)
fmap join $ (\x y z w -> P (P x y) (P z w)) <$> a00 <*> a01 <*> a10 <*> a11
(\x _ _ w -> P x w) <$> a00 <*> a01 <*> a10 <*> a11 -- Maybe (Pair a)

这些显然不一样：虽然任何a 值都将仅从a00 和a11 中提取，但a01 和a10 的影响在左侧被忽略，但不是在右侧（换句话说，如果a01 或a10 是Nothing，则RHS 将为Nothing，但LHS 不一定如此）。 LHS 正好对应chi's answer 中消失的Empty，RHS 对应my other answer 中描述的内对角线修剪。

P.S.：我忘记表明我们在这里讨论的可能实例与问题中讨论的实例相同：

join' ::  m (n (m (n a))) -> m (n a)
join' = fmap @m (join @n) . join @m . fmap @m (sequenceA @n @m)

有了m ~ Maybe 和n ~ Pair，我们有：

join' :: Maybe (Pair (Maybe (Pair a))) -> Maybe (Pair a)
join' = fmap @Maybe (join @Pair) . join @Maybe . fmap @Maybe (sequenceA @Pair @Maybe)

join @Maybe . fmap @Maybe (sequenceA @Pair @Maybe) 表示join' 将导致Nothing，除非任何地方都没有Nothings：

join' = \case
    Just (P (Just (P a00 a01)) (Just (P a10 a11))) -> _
    _ -> Nothing

解决非Nothing 的情况很简单：

fmap join . join . fmap sequenceA $ Just (P (Just (P a00 a01)) (Just (P a10 a11)))
fmap join . join $ Just (Just (P (P a00 a01) (P a10 a11)))
fmap join $ Just (P (P a00 a01) (P a10 a11))
Just (P a00 a11)

所以……

join' = \case
    Just (P (Just (P a00 _)) (Just (P _ a11))) -> Just (P a00 a11)
    _ -> Nothing

...本质上等同于：

join = \case
    Pair (Pair a00 _) (Pair _ a11) -> Pair (a00 a11)
    _ -> Empty

【讨论】：