Actually, the only correct monad instance of Pair
is as follows.
instance Monad Pair where
m >>= f = joinPair (f <$> m)
joinPair :: Pair (Pair a) -> Pair a
joinPair (Pair (Pair x _) (Pair _ y)) = Pair x y
The reason this is the correct monad instance is because Pair
is a representable functor.
instance Representable Pair where
type Rep Pair = Bool
index (Pair x _) False = x
index (Pair _ y) True = y
tabulate f = Pair (f False) (f True)
Turns out, for every representable functor (>>=)
is equivalent to the following bindRep
function.
bindRep :: Representable f => f a -> (a -> f b) -> f b
bindRep m f = tabulate (a -> index (f (index m a)) a)
If we specialize the bindRep
function to Pair
we get the following.
bindRep :: Pair a -> (a -> Pair b) -> Pair b
bindRep (Pair x y) f = tabulate (a -> index (f (index (Pair x y) a)) a)
= Pair (index (f x) False) (index (f y) True)
-- |_________________| |________________|
-- | |
-- (1st elem of f x) (2nd elem of f y)
The following blog post by Adelbert Chang explains it better. Reasoning with representable functors.
Here's another way to prove uniqueness. Consider the left and right identity monad instance laws.
return a >>= k = k a -- left identity law
m >>= return = m -- right identity law
Now, for the Pair
data type return x = Pair x x
. Hence, we can specialize these laws.
Pair a a >>= k = k a -- left identity law
m >>= x -> Pair x x = m -- right identity law
So, what should the definition of >>=
be in order to satisfy these two laws?
Pair x y >>= f = Pair (oneOf [x1, x2, y1, y2]) (oneOf [x1, x2, y1, y2])
where Pair x1 y1 = f x
Pair x2 y2 = f y
The oneOf
function returns one of the elements of the list non-deterministically.
Now, if our >>=
function is to satisfy the left identity law then when x = y
then x1 = x2
and y1 = y2
and the result must be Pair (oneOf [x1, x2]) (oneOf [y1, y2])
.
Similarly, if our >>=
function is to satisfy the right identity law then x1 = y1 = x
and x2 = y2 = y
and the result must be Pair (oneOf [x1, y1]) (oneOf [x2, y2])
.
Hence, if you want to satisfy both laws then the only valid result is Pair x1 y2
.