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
