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'')
join
for the composition of two monads in general. But this does not lead to any concrete examples. – Brent Yorgey