proving the monad laws

[Iavor Diatchki]

hi,

just a comment that the you can get more modular (and hence simpler) 
proofs by using monad transformers.
than you can break down your proof in a number of steps:
1. prove that the identity monad is a monad
2. prove that the exception transformer: ErrorT x m a = m (Either x a)
gives a monad,if 'm' is a monad.
3. prove that the state transformer:  StateT s m a = s -> m (a,s)
gives a monad,provided that 'm' is a monad
then you are done, as TI = StateT Subst (StateT Int (ErrorT String Id)).
this involves more proofs, but they are "simpler" and can be reused for 
other monads as well.

hope this helps
iavor




Steffen Mazanek wrote:
> Hello,
> 
> consider the following monad (which is a slight adaptation of the
> one used in "Typing Haskell in Haskell") as given:
> 
> data Error a = Error String | Ok a
> data TI a = TI (Subst -> Int -> Error (Subst, Int, a))
> instance Monad TI where
>  return x   = TI (\s n -> Ok (s,n,x))
>  TI f >>= g = TI (\s n -> case f s n of
>                            Ok (s',m,x) -> let TI gx = g x in
>                                           gx s' m
>                            Error s->Error s)
>  fail s = TI (\_ _->Error s)
> 
> Now I would like to verify the monad laws. It is really easy to
> show that return is both a left- and a right-unit. But I got stuck
> with associativity:
> 
> m@(TI mf) >>= (\a->f a >>= h) =
>  = TI (\s n -> case mf s n of
>       Ok (s',m,x) -> let TI gx = (\a->f a >>= h) x in
>                            gx s' m
>       Error s->Error s)  =  ...
>  = ((TI mf) >>= f) >>= h
> 
> Is there someone outside who is willing to tell what fills the gap?
> A hint may be sufficient already. Or is there a tool, which finds
> such derivations?
> I have read the tutorial "All about Monads", but there only is mentioned,
> that there is an obligation for the programmer to prove these laws. It
> would be helpful as well, to provide an example!
> I was wondering, if it is possible to simplify: "let TI gx = f x >>=h in 
> ...".
> But the "a" may occur in "h"?
> 
> Thank you.
> Steffen
> 
> _______________________________________________
> Haskell mailing list
> Haskell@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell
> 


-- 
==================================================
| Iavor S. Diatchki, Ph.D. student               |
| Department of Computer Science and Engineering |
| School of OGI at OHSU                          |
| http://www.cse.ogi.edu/~diatchki               |
==================================================