具体示例显示monad在组合下没有关闭（带证据）？
Posted
tags:
篇首语：本文由小常识网(cha138.com)小编为大家整理，主要介绍了具体示例显示monad在组合下没有关闭（带证据）？相关的知识，希望对你有一定的参考价值。
众所周知，应用函子在组合下是封闭的，但是monad不是。但是，我一直难以找到一个具体的反例，表明monad并不总是构成。
This answer将[String -> a]作为非monad的一个例子。在玩了一下之后，我直觉地相信它，但是这个答案只是说“加入无法实现”而没有给出任何理由。我想要更正式的东西。当然有很多类型为[String -> [String -> a]] -> [String -> a]的函数;必须表明任何这样的功能必然不符合monad法则。
任何例子（附带证据）都可以;我不一定特别想要证明上述例子。
考虑这个与(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))。很明显，为了从（1）和（2）返回x有任何希望，我们不能扔掉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))
为了在案例（E）中返回B (Just (P y1 y2))，这意味着我们必须从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'')
对于小型混凝土反例，请考虑终端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的定义必须失败。
构建被排斥的中间人
(->) r是每个r的monad，Either e是每个e的monad。让我们来定义它们的组成（(->) r里面，Either e外面）：
import Control.Monad
newtype Comp r e a = Comp uncomp :: Either e (r -> a)
我声称，如果Comp r e是每个r和e的monad，那么我们可以实现the law of exluded middle。这在intuitionistic logic中是不可能的，call/cc是函数式语言的类型系统的基础（具有排除中间的定律相当于具有Comp算子）。
让我们假设join :: Comp r e (Comp r e a) -> Comp r e a
是一个monad。然后我们有
swap :: (r -> Either e a) -> Either e (r -> a)
swap = uncomp . join . Comp . return . liftM (Comp . liftM return)
所以我们可以定义
swap（这只是布里特特提到的组合monads的data False -- an empty datatype corresponding to logical false
type Neg a = (a -> False) -- corresponds to logical negation
函数，第4.3节，只添加了newtype的（de）构造函数。请注意，我们不关心它具有什么属性，唯一重要的是它是可定义的总。）
现在让我们来吧
r = b并专门交换e = b，a = False，excludedMiddle :: Either b (Neg b)
excludedMiddle = swap Left
：
(->) r结论：尽管Either r和Comp r r是monad，但它们的成分ReaderT不可能。
注意：这也反映在如何定义创建我们第一个Monad
带CheckBoxes的WPF ComboBox显示有关已检查项目的信息？