18 Oct
2001
18 Oct
'01
1:20 a.m.
I want to learn how to go about proving things like (p >>= j) >= k == p >>= (\x->(j x >>= k)) where 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? proof-assistant software?