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

[apfelmus]

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