# [Haskell-cafe] Re: Proofs and commercial code -- was Haskell Weekly News: Issue 85 - September 13, 2008

apfelmus apfelmus at quantentunnel.de
Mon Sep 15 05:32:41 EDT 2008

```Daryoush Mehrtash wrote:
> Does it make sense to use proof to validate that a given monad
> implementation obeys its laws?

Absolutely, and this is usually done by hand.

Take for instance the state monad.

newtype State s a = State { runState :: s -> (a,s) }

instance Monad (State s) where
return x        = State \$ \s -> (x,s)
(State m) >>= f = State \$ \s -> let (x,s') = m s in runState (f x) s'

The first monad law is

return a >>= f = f a

And here is proof:

return a >>= f
= { definition of return }
State (\s -> (a,s)) >>= f
= { definition of >>= }
State \$ \s -> let (x,s') = (\s -> (a,s)) s in runState (f x) s'
= { apply lambda abstraction }
State \$ \s -> let (x,s') = (a,s) in runState (f x) s'
= { pattern binding }
State \$ \s -> runState (f a) s
= { eta reduction }
State \$ runState (f a)
= { State . runState = id }
f a

Exercise: Prove the other monad laws, i.e.

m >>= return = m
(m >>= g) >>= h = m >>= (\x -> g x >>= h)

Regards,
apfelmus

```