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