A concrete example showing that monads are not closed in composition (with proof)?

Question

It is well known that applicative functors are closed in composition, but monads are not. However, I could not find a concrete counterexample showing that monads do not always compose.

This answer gives [String -> a] as an example of a nonmonode. Having played a little with him, I find this intuitive, but this answer simply says: “The connection cannot be implemented,” without any excuse. I would like something more formal. Of course, there are many functions of type [String -> [String -> a]] -> [String -> a] ; it must be shown that any such function does not necessarily satisfy the laws of the monad.

Any example (with accompanying evidence) will do; I am not necessarily looking for evidence of the above example in particular.

Answer 1

Consider this monad isomorphic to the monad (Bool ->) :

 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 

and compose it with Maybe monad:

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

I argue that Bad cannot be a monad.

---

Partial evidence:

There is only one way to determine fmap that satisfies fmap id = id :

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

Recall the laws of the monad:

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

To determine return x we have two options: B Nothing or B (Just (P xx)) . It is clear that in order to hope for the return of x from (1) and (2), we cannot throw away x , so we need to choose the second option.

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

This leaves a 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 is of type Bad a , the only parameters are B Nothing or B (Just (P y1 y2)) , where y1 , y2 must be selected from x1 ... x4 .

In cases (A) and (B), we have no values ​​of type a , so we are forced to return B Nothing in both cases.

Case (E) is determined by the laws of (1) and (2) of the 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)) 

To return B (Just (P y1 y2)) in case (E), this means that we must select y1 from x1 or x3 , and y2 from x2 or 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)) 

Similarly, this suggests that we must choose y1 from x1 or x2 and y2 from x3 or x4 . Combining the two, we determine that the right-hand side of (E) should be B (Just (P x1 x4)) .

So far so good, but the problem arises when you try to fill in the right sides for (C) and (D).

There are 5 possible right sides for each of them, and none of the combinations work. I have no good arguments so far, but I have a program that exhaustively tests all combinations:

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

Answer 2

For a small specific counterexample, consider the terminal monad.

 data Thud x = Thud 

return and >>= just go Thud , and the laws are executed trivially.

Now let there also be a writer monad for Bool (with, say, the structure of xor monoids).

 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 

Er, um, we need a composition

 newtype (:.:) fgx = C (f (gx)) 

Now try to determine ...

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

Parametricity tells us that ??? cannot be in any useful way on x , so it must be a constant. As a result of join . return join . return necessarily a constant function, so the law

 join . return = id 

should fail for any join and return definitions.

Answer 3

Build Excluded Average

(->) r is a monad for each r , and Either e is a monad for each e . Let define their composition ( (->) r inside, Either e outside):

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

I argue that if Comp re were a monad for every r and e , then we could implement the law of excluded mean . This is not possible in the intuitionistic logic that underlies the systems of types of functional languages ​​(having the law of excluded mean is equivalent to calling / cc ).

Suppose Comp is a monad. Then we have

 join :: Comp re (Comp rea) -> Comp rea 

and so we can define

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

(This is just a paper swap function. The component monads that Brent mentions, section 4.3, with the newtype (de) constructors added. Note that we don't care what properties it has, that it is definable and total.)

Now let set

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

and specialize swap for r = b , e = b , a = False :

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

Conclusion: Even if (->) r and Either r are monads, their composition Comp rr cannot be.

Note. This is also reflected in ReaderT and EitherT . Both ReaderT r (Either e) and EitherT e (Reader r) isomorphic to r -> Either ea ! There is no way to define a monad for double Either e (r -> a) .

---

Performing IO Actions

In the same vein, there are many examples that include IO and which lead to the screening of IO some way. For example:

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

Now let

 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) 

What will happen when this program is launched? Two possibilities are possible:

• "First" or "Second" is printed after we read input from the console, which means that the sequence of actions has been canceled and that the actions from foo broke into pure f .

• Or swap (hence join ) discards the IO action, and neither "First" nor "Second" are ever printed. But that means join breaks the law

   join . return = id 

  because if join discards the IO action, then

   foo ≠ (join . return) foo 

Other similar combinations of IO + monad lead to the construction

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

Either their join implementations should allow e to exit the IO , or they should throw it away and replace it with something else, breaking the law.

Answer 4

Your link refers to this data type, so try choosing a specific implementation: data A3 a = A3 (A1 (A2 a))

I will arbitrarily take A1 = IO, A2 = [] . We will also make this newtype and give it a particularly sharp name for pleasure:

newtype ListT IO a = ListT (IO [a])

Take some arbitrary action in this type and run it in two different ways:

 λ> 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] 

As you can see, this violates the law of associativity: ∀xy z. (x >=> y) >=> z == x >=> (y >=> z) ∀xy z. (x >=> y) >=> z == x >=> (y >=> z) .

It turns out that ListT m is only a monad if m is a commutative monad. This prevents a large group of monads from composing [] , which violates the universal rule of "composing two arbitrary monads, giving a monad."

See also: https://stackoverflow.com>