Here's part of a pencil-and-paper proof of laws for a state monad. Before doing so, I've got a question of my own about the *other* laws: Is there a place where somebody has explicitly written the laws that "non-proper morphisms" of commonly used monads? Back to the original question... Beware. What I'm about to say doesn't quite work in Haskell, for two reasons. First, you can't make my definition into an instance of the class Monad without inserting type constructors into inconvenient places. Second, due to the way undefined works in Haskell, the state monad doesn't obey all the laws. Assume we don't have non-termination, and assume we don't care about overloading (>>=) and return (so we don't need to shoe-horn our monad into the monad type class). Preliminaries. From the Prelude we have: curry :: ((a,b) -> c) -> a -> b -> c uncurry :: (a -> b -> c) -> (a,b) -> c id :: a -> a We define the state monad to be a synonym for a function returning a pair: M a = s -> (a,s) Define morphisms return = curry id -- where id is specialized to type (a,s) -> (a,s) m >>= k = (uncurry k) . m get = \s -> (s,s) put s = \_ -> ((),s) Now check the laws. Of the basic 3, I'll only do associativity. The other 2 are easier. Take the two sides of the conjectured law and unfold the definition of >>= (and return), then use properties of uncurry (and curry) to massage them into the same form. If you can do so, the law holds. (I'm going to avoid unfolding the definition of (un)curry so I can stay at a higher level of abstraction, though the following might be shorter if I did unfold them.) LHS == (p >>= q) >>= r == uncurry r . (p >>= q) == uncurry r . (uncurry q . p) RHS = == p >>= (\x -> q x >>= r) == uncurry (\x -> q x >>= r) . p == uncurry (\x -> uncurry r . q x) . p == uncurry (\x s -> (uncurry r . q x) s) . p == uncurry (\x s -> uncurry r (q x s)) . p == (\xs -> uncurry r (q (fst xs) (snd xs))) . p == (\xs -> uncurry r (uncurry q xs)) . p == (\xs -> (uncurry r . uncurry q) xs) . p == (uncurry r . uncurry q) . p Now, one thing that's equally interesting (and perhaps not spoken of often enough) is the laws that the "non-proper morphisms" obey. In the case of state: put a >> get == put a >> return a where each side reduces to \_ -> (a,a) get >> get == get where each side reduces to \s -> ((),s) BTW, in a proof assistant like Coq, Isabelle or Agda these identities can be verified much more easily (though a badly done "proof script" may be unreadable.) On Fri, Apr 11, 2008 at 02:35:28PM -0300, Rafael C. de Almeida wrote:
Hello,
I was studying Monads and I was trying to think about new Monads I could define. So, a question poped into my mind: how is proof regarding the 3 Monad laws handled? I know that, aside from testing all the possible values (and there can be a lot of them), there's no general way to prove it. Nonetheless, I think that it would be insightful to see how people write those proofs for their monads -- specially for new user monads. Is there some article or some notes on proving that Monads are implemented correctly?
[]'s Rafael
-- Tom Harke Portland State University