是`数据PoE a =空| 对aa`一个monad？

Question

这个问题来自于一个应用而非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

实际的原因,我相信这是一个单子是,它是同构于Maybe (Pair a)同Pair a = P a a.它们都是monad,都是可穿越的,所以它们的构图也应该形成monad.哦,我发现并不总是.

哪个反例可以归咎于monad法？(以及如何系统地找到它？)

---

编辑:我没想到这个问题会引起人们的兴趣.如果我接受最好的例子或"系统地"部分的最佳答案,我现在必须下定决心.

同时,我想想象一下如何join更简单地工作Pair a = P a a:

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

它始终采用外部路径,屈服P 1 4,通常称为矩阵表示中的对角线.对于monad associativy,我需要三维,树形可视化效果更好.取自chi的答案,这是加入失败的例子,以及我如何理解它.

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

现在,您join . fmap join首先折叠较低级别,然后join . join从根目录进行折叠.

Answer 1

显然,它不是一个单子.其中一个monad" 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法律更容易测试,比如,相关性>>=.

Answer 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

Answer 3

既然你对如何系统地做到这一点很感兴趣,这就是我如何找到一个快速检查的反例:

{-# 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

并测试monad法则:

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)映射到a Pair,所以我们不能按照两个monad中的任何一个的规律PoE组成.

Answer 4

这种潜在的Monad实例可以简洁地描述为"采取对角线".如果我们使用join演示文稿,则更容易理解为什么.这是你提到join的Pair类型:

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

然而,取对角线只能保证给join定长(或无限)列表合法.这是因为相关性法则:

join . join = join . fmap join

如果列表列表中的第n个列表没有第n个元素,则将导致对角线被修剪:它将在其第n个元素之前结束.join . join首先取内部对角线(列表列表),同时join . fmap join取内部对角线.有可能对于不在外对角线中的不够长的最里面的列表进行修剪join . fmap join,但是它不可能影响join . join.(用图片而不是单词更容易显示.)

你PoE是一个类似列表的类型,没有固定长度(长度为零或两个).事实证明,采取对角线不会给我们一个monad,因为上面讨论的潜在问题实际上阻碍了(如chi的回答所示).

补充说明:

• 这正是ZipList不是monad 的原因:zippy行为相当于采取对角线.

• 无限列表与自然函数同构,固定长度列表与自然函数同构到适当的值是同构的.这意味着您可以从Monad实例中为函数获取实例 - 而您获得的实例再次等于采用对角线.

• 曾几何时,我对这个确切的问题感到困惑.