proving the monad laws

[oleg@pobox.com]

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
	(st f) . (st g)
and do:
	- inlining of the 'st' operation
	- de-sugaring into core Haskell
	- more inlining and beta [perhaps to a certain depth]
	- rearranging expression based on associative laws,
	e.g., converting f . (g . h) into (f . g) . h
	converting
	   case (case x of P -> A) of P' -> A'
	into
	   case x of P -> case A of P' -> A'

Then do the same for (st ((st f) . g)) and compare the results. If the
results are identical, great. Otherwise, the user has to look at the
results and decide if they are the same based on his intuition.

GHC already does inlining, de-sugaring, and some betas. I think there
is a flag that makes GHC dump the result of these operations for
normalization with respect associative laws. BTW, GHC accepts
user-defined rules: so we can express associativity rules for known
operations and direct GHC to normalize terms with respect to these
laws. I don't know how to express side conditions though (e.g., the
normalization of 'case' above is valid only if the variables bound by
pattern P do not occur in P', A'). It would be great if there was a
RULES-pragma operation to alpha-rename bound variables in a term. In
that case, we can safely normalize more expressions.