84
votes

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.

5
The closest I can find is the appendix of web.cecs.pdx.edu/~mpj/pubs/RR-1004.pdf, which shows that under a lot of simplifying assumptions, it is impossible to write join for the composition of two monads in general. But this does not lead to any concrete examples.Brent Yorgey
You may get better answers to this question on cs.stackexchange.com, the new Computer Science Stack Exchange site.Patrick87
Perhaps I'm not understanding, but I think the question could be more precisely defined. When you say "composing" two monads, do you mean simply composing the type constructors? And when the result "is not a monad", does this mean that a monad instance of that type construcor cannot be written? And, if a monad instance for the composed type constructor can be written, does it have to bear any relation to the instances of the two factor monads, or can it be totally unrelated?Owen
Yes, I mean composing the type constructors; "not a monad" means a valid (lawful) monad instance cannot be written; and I don't care whether the instance for the composition has any relation to the instances of the factors.Brent Yorgey

5 Answers

42
votes

Consider this monad which is isomorphic to the (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

and 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) x

Recall 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 a
return' 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 equal
B (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 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))

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

For a small concrete counterexample, consider the terminal monad.

data Thud x = Thud

The return and >>= just go Thud, and the laws hold trivially.

Now let's also have the writer monad for Bool (with, let's say, the xor-monoid structure).

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

Er, um, we'll need composition

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

Now try to define...

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

Parametricity tells us that ??? can't depend in any useful way on x, so it must be a constant. As a result, join . return is necessarily a constant function also, hence the law

join . return = id

must fail for whatever definitions of join and return we choose.

35
votes

Constructing excluded middle

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

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

I claim that if Comp r e were a monad for every r and e then we could realize the law of exluded middle. This is not possible in intuitionistic logic which underlies typesystems of functional languages (having the law of excluded middle is equivalent to having the call/cc operator).

Let's assume Comp is a monad. Then we have

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

and so we can define

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

(This is just the swap function from paper Composing monads that Brent mentions, Sect. 4.3, only with newtype's (de)constructors added. Note that we don't care what properties it has, the only important thing is that it is definable and total.)

Now let's 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 though (->) r and Either r are monads, their composition Comp r r cannot be.

Note: That this is also reflected in how ReaderT and EitherT are defined. Both ReaderT r (Either e) and EitherT e (Reader r) are isomorphic to r -> Either e a! There is no way how to define monad for the dual Either e (r -> a).


Escaping IO actions

There are many examples in the same vein that involve IO and which lead to escaping IO somehow. For example:

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)

Now let's have

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 run? There are two possibilities:

  1. "First" or "Second" is printed after we read input from the console, meaning that the sequence of actions was reversed and that the actions from foo escaped into pure f.
  2. Or swap (hence join) throws away the IO action and neither "First" nor "Second" is ever printed. But this means that join violates the law

    join . return = id
    

    because if join throws the IO action away, then

    foo ≠ (join . return) foo
    

Other similar IO + monad combinations lead to constructing

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

Either their join implementations must allow e to escape from IO or they must throw it away and replace with something else, violating the law.

4
votes

Your link references this data type, so let's try picking some specific implementation: data A3 a = A3 (A1 (A2 a))

I will arbitrarily pick A1 = IO, A2 = []. We'll also make it a newtype and give it a particularly pointed name, for fun:

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

Let's come up with some arbitrary action in that type, and run it in two different-but-equal ways:

λ> let v n = 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 breaks the associativity law: ∀x y z. (x >=> y) >=> z == x >=> (y >=> z).

It turns out, ListT m is only a monad if m is a commutative monad. This prevents a large category of monads from composing with [], which breaks the universal rule of "composing two arbitrary monads yields a monad".

See also: https://stackoverflow.com/a/12617918/1769569

-1
votes

Monads do not compose. Not in a generic way - there is no general way of composing monads. See https://www.slideshare.net/pjschwarz/monads-do-not-compose