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 [EMAIL PROTECTED] 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 | ==================================================
_______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
