[Haskell-cafe] Monad proof

[harke at cs.pdx.edu]

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