具体例子表明 monads 在组合下不是封闭的(有证据)?

情况 (E) 由 (1) 和 (2) monad 定律决定:-- 将 (1) 应用到 (B (Just (P y1 y2)))加入 (返回' (B (Just (P y1 y2))))= -- 使用我们对返回的定义'加入 (B (Just (P (B (Just (P y1 y2))) (B (Just (P y1 y2))))))= - 从(1)这应该等于B (只是 (P y1 y2))为了在情况 (E) 中返回 B (Just (P y1 y2))，这意味着我们必须从 x1 中选择 y1code> 或 x3,和 y2 来自 x2 或 x4.-- 将 (2) 应用到 (B (Just (P y1 y2)))join (fmap return' (B (Just (P y1 y2))))= -- fmap 的定义加入 (B (Just (P (return y1) (return y2))))= -- 返回定义加入 (B (Just (P (B (Just (P y1 y1))) (B (Just (P y2 y2))))))= - 从(2)这应该等于B (只是 (P y1 y2))同样，这表示我们必须从 x1 或 x2 中选择 y1，并从其中任何一个中选择 y2x3 或 x4.两者结合，我们确定 (E) 的右侧必须是 B (Just (P x1 x4)).到目前为止一切都很好，但是当您尝试填写 (C) 和 (D) 的右侧时，问题就出现了.每个都有 5 个可能的右手边，但没有一个组合有效.我对此还没有很好的论据，但我确实有一个程序可以详尽地测试所有组合:{-# LANGUAGE ImpredicativeTypes, ScopedTypeVariables #-}导入 Control.Monad(守卫)数据对 a = P a a推导 (Eq, Show)实例函子对在哪里fmap f (P x y) = P (f x) (f y)实例 Monad Pair where返回 x = P x xP a b >>= f = P x y其中 P x _ = f aP _ y = f bnewtype Bad a = B (也许 (Pair a))推导 (Eq, Show)实例函子坏在哪里fmap f (B x) = B $ fmap (fmap f) x-- 唯一可行的定义.单位 :: a ->坏了单位 x = B (Just (P x x))-- 此类型连接的可能定义数.如果这等于零，则没有 monad 适合您！加入 :: 整数加入 = 总和 $ 做-- 尝试所有可能的方法来处理下面连接定义中的情况 3 和 4.让方式 = [ \_ _ ->B 什么都没有, a b ->B(只是(P a)), a b ->B (只是 (P a b)), a b ->B (只是 (P b a)), a b ->B (Just (P b b)) ] :: [forall a.->->坏了]c3 :: forall a.->->坏 <- 方式c4 :: forall a.->->坏 <- 方式让加入:: forall a.坏 (Bad a) ->坏了join (B Nothing) = B Nothing -- 别无选择join (B (Just (P (B Nothing) (B Nothing)))) = B Nothing -- 再次，别无选择join (B (Just (P (B (Just (P x1 x2))) (B Nothing))) = c3 x1 x2join (B (Just (P (B Nothing) (B (Just (P x3 x4))))) = c4 x3 x4join (B (Just (P (B (Just (P x1 x2))) (B (Just (P x3 x4)))))) = B (Just (P x1 x4)) -- 源自monad定律-- 我们已经从这两个人身上学到了一切，但我还是决定留下他们.守卫 $ all (x -> join (unit x) == x) bad1守卫 $ all (x -> join (fmap unit x) == x) bad1——这才是最重要的守卫 $ all (x -> join (join x) == join (fmap join x)) bad3返回 1main = putStrLn $ show joins ++ 组合工作."-- 用于生成包含不同 Int 的所有不同形式的 Bad 值的函数.bad1 :: [坏整数]bad1 = map fst (bad1' 1)bad3 :: [坏 (坏 (坏 (坏)))]bad3 = 地图 fst (bad3' 1)bad1' :: 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) : 做(x, n') [(Bad (Bad (Bad Int)), Int)]bad3' n = (B Nothing, n) : 做(x, n') It is well-known that applicative functors are closed under composition but monads are not. However, I have been having trouble finding a concrete counterexample showing that monads do not always compose.This answer gives [String -> a] as an example of a non-monad. After playing around with it for a bit, I believe it intuitively, but that answer just says "join cannot be implemented" without really giving any justification. I would like something more formal. Of course there are lots of functions with type [String -> [String -> a]] -> [String -> a]; one must show that any such function necessarily does not satisfy the monad laws.Any example (with accompanying proof) will do; I am not necessarily looking for a proof of the above example in particular. 解决方案 Consider this monad which is isomorphic to the (Bool ->) monad:data Pair a = P a ainstance 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 band compose it with the Maybe monad:newtype Bad a = B (Maybe (Pair a))I claim that Bad cannot be a monad.Partial proof:There's only one way to define fmap that satisfies fmap id = id:instance Functor Bad where fmap f (B x) = B $ fmap (fmap f) xRecall the monad laws:(1) join (return x) = x(2) join (fmap return x) = x(3) join (join x) = join (fmap join x)For the definition of return x, we have two choices: B Nothing or B (Just (P x x)). It's clear that in order to have any hope of returning x from (1) and (2), we can't throw away x, so we have to pick the second option.return' :: a -> Bad areturn' x = B (Just (P x x))That leaves join. Since there are only a few possible inputs, we can make a case for each: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)))))) = ???Since the output has type Bad a, the only options are B Nothing or B (Just (P y1 y2)) where y1, y2 have to be chosen from x1 ... x4.In cases (A) and (B), we have no values of type a, so we're forced to return B Nothing in both cases.Case (E) is determined by the (1) and (2) monad laws:-- 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 equalB (Just (P y1 y2))In order to return B (Just (P y1 y2)) in case (E), this means we must pick y1 from either x1 or x3,and y2 from either x2 or x4.-- apply (2) to (B (Just (P y1 y2)))join (fmap return' (B (Just (P y1 y2))))= -- def of fmapjoin (B (Just (P (return y1) (return y2))))= -- def of returnjoin (B (Just (P (B (Just (P y1 y1))) (B (Just (P y2 y2))))))= -- from (2) this should equalB (Just (P y1 y2))Likewise, this says that we must pick y1 from either x1 or x2, and y2 from either x3 or x4. Combining the two,we determine that the right hand side of (E) must be B (Just (P x1 x4)).So far it's all good, but the problem comes when you try to fill in the right hand sides for (C) and (D).There are 5 possible right hand sides for each, and none of the combinations work. I don't have a nice argument for this yet, but I do have a program that exhaustively tests all the combinations:{-# 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 bnewtype 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 aunit x = B (Just (P x x))-- Number of possible definitions of join for this type. If this equals zero, no monad for you!joins :: Integerjoins = 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 1main = 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'') 这篇关于具体例子表明 monads 在组合下不是封闭的(有证据)?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！ 上岸，阿里云！