[Haskell-beginners] Monad for Pair

[Mike Houghton]

Thanks for this - I’ll work through it.

Mike

> On 18 Nov 2015, at 08:28, Marcin Mrotek <marcin.jan.mrotek at gmail.com> 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners