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