Concrete example showing that monads are not closed under composition (with proof)?
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'')
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.
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:
- "First" or "Second" is printed after we read
input
from the console, meaning that the sequence of actions was reversed and that the actions fromfoo
escaped into puref
. Or
swap
(hencejoin
) throws away theIO
action and neither "First" nor "Second" is ever printed. But this means thatjoin
violates the lawjoin . return = id
because if
join
throws theIO
action away, thenfoo ≠ (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.