haskell - 具体的例子表明单子(monad)在组合下不是封闭的(有证明)？

Question

众所周知，应用仿函数在组合下是封闭的，但 monad 不是。然而，我一直很难找到一个具体的反例来表明单子(monad)并不总是组合的。

This answer给出 [String -> a] 作为非 monad 的示例。经过一番尝试后，我凭直觉相信它，但这个答案只是说“连接无法实现”，而没有真正给出任何理由。我想要更正式的东西。当然，有很多类型为 [String -> [String -> a]] -> [String -> a] 的函数；必须证明任何这样的函数必然不满足单子(monad)定律。

任何例子(附带证明)都可以；我不一定要特别寻找上述示例的证明。

Answer 1

考虑这个与 (Bool ->) 同构的 monad单子(monad):

data Pair a = P a a

instance Functor Pair where
  fmap f (P x y) = P (f x) (f y)

instance Monad Pair where
  return x = P x x
  P a b >>= f = P x y
    where P x _ = f a
          P _ y = f b

并用 Maybe 组成它单子(monad):

newtype Bad a = B (Maybe (Pair a))

我声称Bad不能是单子(monad)。

<小时/>

部分证明:

只有一种方法可以定义 fmap满足fmap id = id :

instance Functor Bad where
    fmap f (B x) = B $ fmap (fmap f) x

回想一下单子(monad)定律:

(1) join (return x) = x 
(2) join (fmap return x) = x
(3) join (join x) = join (fmap join x)

对于return x的定义，我们有两个选择:B Nothing或B (Just (P x x)) 。很明显，为了有任何返回的希望x从(1)和(2)，我们不能扔掉x ，所以我们必须选择第二个选项。

return' :: a -> Bad a
return' x = B (Just (P x x))

剩下 join 。由于只有几个可能的输入，我们可以为每个输入提供一个案例:

join :: Bad (Bad a) -> Bad a
(A) join (B Nothing) = ???
(B) join (B (Just (P (B Nothing)          (B Nothing))))          = ???
(C) join (B (Just (P (B (Just (P x1 x2))) (B Nothing))))          = ???
(D) join (B (Just (P (B Nothing)          (B (Just (P x1 x2)))))) = ???
(E) join (B (Just (P (B (Just (P x1 x2))) (B (Just (P x3 x4)))))) = ???

由于输出的类型为 Bad a ，唯一的选项是 B Nothing或B (Just (P y1 y2))哪里y1 , y2必须从x1 ... x4中选择.

在情况 (A) 和 (B) 中，我们没有 a 类型的值，所以我们被迫返回B Nothing在这两种情况下。

情况 (E) 由 (1) 和 (2) 单子(monad)定律确定:

-- apply (1) to (B (Just (P y1 y2)))
join (return' (B (Just (P y1 y2))))
= -- using our definition of return'
join (B (Just (P (B (Just (P y1 y2))) (B (Just (P y1 y2))))))
= -- from (1) this should equal
B (Just (P y1 y2))

为了返回B (Just (P y1 y2))在情况 (E) 中，这意味着我们必须选择 y1来自 x1或x3 ,和y2来自 x2或x4 .

-- apply (2) to (B (Just (P y1 y2)))
join (fmap return' (B (Just (P y1 y2))))
= -- def of fmap
join (B (Just (P (return y1) (return y2))))
= -- def of return
join (B (Just (P (B (Just (P y1 y1))) (B (Just (P y2 y2))))))
= -- from (2) this should equal
B (Just (P y1 y2))

同样，这表示我们必须选择 y1来自 x1或x2 ，和y2来自 x3或x4 。结合两者，我们确定 (E) 的右侧必须是 B (Just (P x1 x4)) .

到目前为止，一切都很好，但是当您尝试填写 (C) 和 (D) 的右侧时，问题就出现了。

每个都有 5 个可能的右侧，但没有一个组合有效。我对此还没有一个很好的论据，但我确实有一个程序可以详尽地测试所有组合:

{-# LANGUAGE ImpredicativeTypes, ScopedTypeVariables #-}

import Control.Monad (guard)

data Pair a = P a a
  deriving (Eq, Show)

instance Functor Pair where
  fmap f (P x y) = P (f x) (f y)

instance Monad Pair where
  return x = P x x
  P a b >>= f = P x y
    where P x _ = f a
          P _ y = f b

newtype Bad a = B (Maybe (Pair a))
  deriving (Eq, Show)

instance Functor Bad where
  fmap f (B x) = B $ fmap (fmap f) x

-- The only definition that could possibly work.
unit :: a -> Bad a
unit x = B (Just (P x x))

-- Number of possible definitions of join for this type. If this equals zero, no monad for you!
joins :: Integer
joins = sum $ do
  -- Try all possible ways of handling cases 3 and 4 in the definition of join below.
  let ways = [ \_ _ -> B Nothing
             , \a b -> B (Just (P a a))
             , \a b -> B (Just (P a b))
             , \a b -> B (Just (P b a))
             , \a b -> B (Just (P b b)) ] :: [forall a. a -> a -> Bad a]
  c3 :: forall a. a -> a -> Bad a <- ways
  c4 :: forall a. a -> a -> Bad a <- ways

  let join :: forall a. Bad (Bad a) -> Bad a
      join (B Nothing) = B Nothing -- no choice
      join (B (Just (P (B Nothing) (B Nothing)))) = B Nothing -- again, no choice
      join (B (Just (P (B (Just (P x1 x2))) (B Nothing)))) = c3 x1 x2
      join (B (Just (P (B Nothing) (B (Just (P x3 x4)))))) = c4 x3 x4
      join (B (Just (P (B (Just (P x1 x2))) (B (Just (P x3 x4)))))) = B (Just (P x1 x4)) -- derived from monad laws

  -- We've already learnt all we can from these two, but I decided to leave them in anyway.
  guard $ all (\x -> join (unit x) == x) bad1
  guard $ all (\x -> join (fmap unit x) == x) bad1

  -- This is the one that matters
  guard $ all (\x -> join (join x) == join (fmap join x)) bad3

  return 1 

main = putStrLn $ show joins ++ " combinations work."

-- Functions for making all the different forms of Bad values containing distinct Ints.

bad1 :: [Bad Int]
bad1 = map fst (bad1' 1)

bad3 :: [Bad (Bad (Bad Int))]
bad3 = map fst (bad3' 1)

bad1' :: Int -> [(Bad Int, Int)]
bad1' n = [(B Nothing, n), (B (Just (P n (n+1))), n+2)]

bad2' :: Int -> [(Bad (Bad Int), Int)]
bad2' n = (B Nothing, n) : do
  (x, n')  <- bad1' n
  (y, n'') <- bad1' n'
  return (B (Just (P x y)), n'')

bad3' :: Int -> [(Bad (Bad (Bad Int)), Int)]
bad3' n = (B Nothing, n) : do
  (x, n')  <- bad2' n
  (y, n'') <- bad2' n'
  return (B (Just (P x y)), n'')