（具有certificate）显示monad没有closures的具体例子？
众所周知，应用函子在构图下是封闭的，但monad不是。 然而，我一直无法find一个具体的反例，表明monad并不总是构成。
这个答案给出了[String -> a]作为非monad的例子。 在玩了一下之后，我直觉地相信，但是这个答案只是说“连接不能实现”而没有给出任何理由。 我想要更正式的东西。 当然还有很多types为[String -> [String -> a]] -> [String -> a]的函数。 必须表明任何这样的function必然不符合单子法。
任何示例（附带certificate）都可以; 我不一定特别寻找上述例子的certificate。
考虑这个与(Bool ->) monad同构的monad：
data Pair a = P aa instance Functor Pair where fmap f (P xy) = P (fx) (fy) instance Monad Pair where return x = P xx P ab >>= f = P xy where P x _ = fa P _ y = fb
并用Maybe monad撰写：
newtype Bad a = B (Maybe (Pair a))
我声称Bad不能是单子。
部分certificate：
定义满足fmap id = id fmap只有一种方法：
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的定义，我们有两个select： B Nothing或B (Just (P xx)) 。 很显然，为了有从（1）和（2）中返回x任何希望，我们不能丢弃x ，所以我们必须select第二个选项。
return' :: a -> Bad a return' x = B (Just (P xx))
那离开join 。 由于只有less数可能的投入，我们可以为每个情况提供一个案例：
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)))))) = ???
由于输出的typesBad a ，唯一的选项是B Nothing或B (Just (P y1 y2)) ，其中y1 ， y2必须从x1 ... x4select。
在（A）和（B）的情况下，我们没有atypesa值，所以在这两种情况下我们都被迫返回B Nothing 。
情况（E）由（1）和（2）单子定律确定：
-- 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)) ，这意味着我们必须从x1或者x3selecty1 ，并且从x2或者x4 y2 。
-- 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))
同样，这就表示我们必须从x1或x2selecty1 ，并从x3或x4 y2 。 结合这两者，我们确定（E）的右边必须是B (Just (P x1 x4)) 。
到目前为止，这一切都很好，但是当你尝试填写（C）和（D）的右侧时，问题就来了。
有5个可能的右侧为每个，没有任何组合工作。 我还没有一个很好的论据，但我有一个程序，详尽地testing所有的组合：
{-# LANGUAGE ImpredicativeTypes, ScopedTypeVariables #-} import Control.Monad (guard) data Pair a = P aa deriving (Eq, Show) instance Functor Pair where fmap f (P xy) = P (fx) (fy) instance Monad Pair where return x = P xx P ab >>= f = P xy where P x _ = fa P _ y = fb 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 xx)) -- 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 , \ab -> B (Just (P aa)) , \ab -> B (Just (P ab)) , \ab -> B (Just (P ba)) , \ab -> B (Just (P bb)) ] :: [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 xy)), 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 xy)), n'')
对于一个小的具体的反例，考虑terminalmonad。
data Thud x = Thud
return和>>=只是去Thud ，法律微不足道。
现在，让我们让Bool的作者monad吧（比方说，异或结构）。
data Flip x = Flip Bool x instance Monad Flip where return x = Flip False x Flip False x >>= f = fx Flip True x >>= f = Flip (not b) y where Flip by = fx
呃，我们需要组合
newtype (:.:) fgx = C (f (gx))
现在尝试定义…
instance Monad (Flip :.: Thud) where -- that's effectively the constant `Bool` functor return x = C (Flip ??? Thud) ...
参数性告诉我们 不能以任何有用的方式依赖于x ，所以它必须是一个常数。 因此， join . return join . return也是一个不变的function，因此是法律
join . return = id
必须失败，无论我们select的join和return定义。
构build排除的中间
(->) r是每个r一个monad， Either e是每个e一个monad。 让我们定义它们的组成（ (->) r里面，或Either e外）：
import Control.Monad newtype Comp rea = Comp { uncomp :: Either e (r -> a) }
我声称， 如果Comp re是每个r和e的monad，那么我们就可以实现中间排除的规律 。 这在function语言的types系统的基础之上的直觉主义逻辑中是不可能的（具有被排除中的定律相当于具有调用/ cc算子）。
假设Comp是一个monad。 那我们有
join :: Comp re (Comp rea) -> Comp rea
所以我们可以定义
swap :: (r -> Either ea) -> Either e (r -> a) swap = uncomp . join . Comp . return . liftM (Comp . liftM return)
（这只是纸张的swapfunction，就是Brent提到的单元组，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 rr不可能是。
注意：这也反映在ReaderT和EitherT是如何定义的。 ReaderT r (Either e)和EitherT e (Reader r)都同构于r -> Either ea ！ 没有办法如何定义monad的双Either e (r -> a) 。
转义IO操作
涉及到IO的同样的例子有很多，并且导致IO以某种方式逃脱。 例如：
newtype Comp ra = 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)
这个程序运行时会发生什么？ 有两种可能性：
- 当我们从控制台读取
input后，打印出“First”或“Second”，这意味着一系列的动作被颠倒过来 ，而foo的动作逃到了纯粹的f。 -
或
swap（因此join）抛出IO操作，既不是“第一”也不是“第二”打印。 但这意味着join违反法律join . return = id因为如果
join抛出IO动作的话foo ≠ (join . return) foo
其他类似的IO + monad组合导致构build
swapEither :: IO (Either ea) -> Either e (IO a) swapWriter :: (Monoid e) => IO (Writer ea) -> Writer e (IO a) swapState :: IO (State ea) -> State e (IO a) ...
他们的join实现必须允许e从IO逃脱，否则他们必须抛弃它，并用其他方法取代，违反法律。
你的链接引用这个数据types，所以让我们尝试select一些具体的实现： data A3 a = A3 (A1 (A2 a))
我会随意挑选A1 = IO, A2 = [] 。 我们也会把它变成新的types，并给它一个特别指出的名字，为了好玩：
newtype ListT IO a = ListT (IO [a])
让我们来想一下这种types的任意行为，并以两种不同的方式运行它：
λ> let vn = ListT $ do {putStr (show n); return [0, 1]} λ> runListT $ ((v >=> v) >=> v) 0 0010101[0,1,0,1,0,1,0,1] λ> runListT $ (v >=> (v >=> v)) 0 0001101[0,1,0,1,0,1,0,1]
正如你所看到的，这打破了关联性定律： ∀xy z. (x >=> y) >=> z == x >=> (y >=> z) ∀xy z. (x >=> y) >=> z == x >=> (y >=> z) 。
事实certificate，如果m是一个交换单子， ListT m只是一个单子。 这可以防止一大类monad与[]合成，这打破了“构成两个任意单子产生单子”的普遍规则。
另请参阅： https ： //stackoverflow.com/a/12617918/1769569
