Wed, 17 Oct 2001 10:20:17 -0700
I want to learn how to go about proving things like
(p >>= j) >= k == p >>= (\x->(j x >>= k))
p >>= k = \s0 -> let (s1, a) = p s0
in k a s1
eg, verifying that the 3 monad laws hold for a specific monad.
also, verifying the more numerous laws every arrow should obey.
I could teach myself to do it clumsily, but I want to learn from others.
would learning category theory help me do this? pointers to documents?