具体示例显示monad在组合下没有关闭(带证据)？

Question

众所周知,应用函子在组合下是封闭的,但是monad不是.但是,我一直难以找到一个具体的反例,表明monad并不总是构成.

这个答案给出[String -> a]了一个非monad的例子.在玩了一下之后,我直觉地相信它,但是这个答案只是说"加入无法实现"而没有给出任何理由.我想要更正式的东西.当然有很多类型的函数[String -> [String -> a]] -> [String -> a]; 必须表明任何这样的功能必然不符合monad法则.

任何例子(附带证据)都可以; 我不一定特别想要证明上述例子.

Answer 1

考虑一下与monad同构的(Bool ->)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

并用Maybemonad组成:

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'')

Answer 2

对于小型混凝土反例,请考虑终端monad.

data Thud x = Thud

该return和>>=只是去Thud,和法律保持平凡.

现在让我们来看看Bool的作家monad(比方说,xor-monoid结构).

data Flip x = Flip Bool x

instance Monad Flip where
   return x = Flip False x
   Flip False x  >>= f = f x
   Flip True x   >>= f = Flip (not b) y where Flip b y = f x

呃,我们需要作文

newtype (:.:) f g x = C (f (g x))

现在尝试定义......

instance Monad (Flip :.: Thud) where  -- that's effectively the constant `Bool` functor
  return x = C (Flip ??? Thud)
  ...

参数化告诉我们???不能以任何有用的方式依赖x,因此它必须是常量.结果,join . return也必然是一个恒定的功能,因此是法律

join . return = id

必须失败的任何定义join和return我们选择.

Answer 3

构建被排斥的中间人

(->) r是每一个单子r,并Either e为每一个单子e.让我们来定义它们的构成((->) r内部,Either e外部):

import Control.Monad
newtype Comp r e a = Comp { uncomp :: Either e (r -> a) }

我声称,如果Comp r e每个人都是monad r,e那么我们就可以实现被排除在中间的法则.这在功能语言的类型系统的基础上的直觉逻辑中是不可能的(具有被排除的中间定律相当于具有call/cc运算符).

我们假设Comp是monad.然后我们有

join :: Comp r e (Comp r e a) -> Comp r e a

所以我们可以定义

swap :: (r -> Either e a) -> Either e (r -> a)
swap = uncomp . join . Comp . return . liftM (Comp . liftM return)

(这只是布里特特提到的组合monads的swap功能,第4.3节,只添加了newtype的(de)构造函数.注意我们不关心它具有什么属性,唯一重要的是它是可定义的和总数.)

现在让我们来吧

data False -- an empty datatype corresponding to logical false
type Neg a = (a -> False) -- corresponds to logical negation

并专门调换r = b,e = b,a = False:

excludedMiddle :: Either b (Neg b)
excludedMiddle = swap Left

结论:即使(->) r和Either r有单子,它们的组成Comp r r是不可能的.

注:这也是体现在如何ReaderT和EitherT定义.无论 ReaderT r (Either e)和EitherT e (Reader r)同形r -> Either e a!没有办法如何为双重定义monad Either e (r -> a).

逃避IO行动

有许多相同的例子涉及IO并导致以IO某种方式逃脱.例如:

newtype Comp r a = Comp { uncomp :: IO (r -> a) }

swap :: (r -> IO a) -> IO (r -> a)
swap = uncomp . join . Comp . return . liftM (Comp . liftM return)

现在让我们拥有

main :: IO ()
main = do
   let foo True  = print "First" >> return 1
       foo False = print "Second" >> return 2
   f <- swap foo
   input <- readLn
   print (f input)

运行此程序时会发生什么？有两种可能性:

1. 在我们input从控制台读取之后打印"第一个"或"第二个" ,这意味着操作的顺序被颠倒了,并且操作从foo逃逸到纯粹f.

2. 或者swap(因此join)抛弃了IO动作,既没有打印"第一"也没有"第二".但这意味着join违反了法律

   join . return = id
   

   因为如果join把IO动作扔掉,那么

   foo ? (join . return) foo
   

其他类似的IO+ monad组合导致构建

swapEither :: IO (Either e a) -> Either e (IO a)
swapWriter :: (Monoid e) => IO (Writer e a) -> Writer e (IO a)
swapState  :: IO (State e a) -> State e (IO a)
...

他们的join实施必须允许e逃避,IO或者他们必须抛弃它并用其他东西替换,违反法律.