Hello,
thank you for the idea of using variables directly to see what happens.
This is really a simplification for the proof.
At first I thought that there should be a simpler solution and I tried to
modify your approach, so that it applies to = as well, but now I am
convinced :-) I have
Hello!
Would it be possible to write a piece of Haskell code which checks
the monadic laws automatically by simulating evaluation in this way?
To some extent, yes. The proof in the previous message was based on
normalization, with respect to associative laws and some betas. So we
can take
Steffen Mazanek posed a problem: given the monad:
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
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
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 -
