[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
More information about the Haskell-Cafe
mailing list