Re: [Haskell-beginners] Monad for Pair

Thanks for this - I’ll work through it. Mike

On 18 Nov 2015, at 08:28, Marcin Mrotek wrote:

...

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 _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners