[Haskell-beginners] Monad for Pair

[Marcin Mrotek]

> You might want to try writing out a test instance in full and re-checking the second law.

Ok, while the part upto Applicative is correct and unambiguous:

data Pair a = Pair a a

instance Functor Pair where
  fmap f (Pair a b) = Pair (f a) (f b)

instance Applicative Pair where
  pure a = Pair a a
  Pair fa fb <*> Pair a b = Pair (fa a) (fb b)

there are at least two implementations of Monad (assuming return=pure,
also GHC 7.10 allows omitting return and implements it exactly like
that):

-- implementation (a)
instance Monad Pair where
  Pair a _ >>= k = k a

-- implementation (b)
instance Monad Pair where
  Pair _ b >>= k = k b

... neither of which can satisfy the laws. There are more:

-- implementation (c)
instance Monad Pair where
  Pair a b >>= k = Pair a' b'
    where
      Pair a' _ = k a
      Pair _ b' = k b

-- implementation (d)
instance Monad Pair where
  Pair a b >>= k = Pair a' b'
    where
      Pair _ b' = k a
      Pair a' _ = k b

and, well:

instance Monad Pair where
  Pair a b >>= _ = Pair a b

Did I miss anything? Now, trying to get the second law to work:

a) m >>= return = m
Pair a b >>= (\a -> Pair a a) = Pair a b
Pair a a = Pair a b
contradiction.

b) m >>= return = m
Pair a b >>= (\a -> Pair a a) = Pair a b
Pair b b = Pair a b
contradiction.

c) m >>= return = m
Pair a b >>= (\a -> Pair a a) = Pair a b
Pair a b = Pair a b
no contradiction this time, I'll write the other laws after I'm done
with the second for the other instances.

d) m >>= return = m
Pair a b >>= (\a -> Pair a a) = Pair a b
Pair b a = Pair a b
contradiction.

e) m >>= return = m
trivially correct.

Testing the first law for (c) and (e) that passed the second law:

c) return a >>= k = k a
Pair a a >>= k a = k a
---
Pair a' b' = k a
  where
    Pair a' _ = k a
    Pair _ b' = k a
---
no contradiction again.

e) return a >>= k = k a
return a = k a
contradiction.

Okay, then testing the third law for (c):

m >>= (\x -> k x >>= h)  =  (m >>= k) >>= h

Pair a b >>=  (\x -> k x >>= h) = (Pair a b >>= k) >>= h (*)

Let's again unpack the application of >>= in some pseud-haskell:

Pair a1 _ = (\x -> k x >>= h) a = k a >>= h (**)
Pair _ b1 = (\x -> k x >>= h) b = k b >> =h

Pair a2 _ = k a (***)
Pair _ b2 = k b

plugging it into (*):

Pair a1 b1 = Pair a2 b2 >>= h

Unpacking >>= again:

Pair a3 _ = h a2 (****)
Pair _ b3 = h b2

Pair a1 b1 = Pair a3 b3

Now, testing if a1 = a3, lets bring in (**), (***), and (****):

Pair a1 _ = k a >>= h
Pair a2 _ = k a
Pair a3 _ = h a2

Form the first and the second equations (also using the one for b2
earlier, but it's going to be dropped anyway sooner or later) we get:

Pair a1 _ = Pair a2 b2 >>= h

Unpacking >>= :

Pair a4 _ = h a2
Pair _ b4 = h b2

But from the third equation we know that (Pair a3 _ = h a2) so:

Pair a1 _ = Pair a3 _

This does seem to work, I have no idea why. I'm pretty sure there I've
made a mistake somewhere. Perhaps I shouldn't do equational reasoning
after just getting up, or just use Agda :-/

Best regards,
Marcin Mrotek