Hello, instances of classes are required to fulfill certain laws. These laws are usually given in the form t = t' where t and t' are terms. My question is what the exact meaning of the = is. Does it mean that evaluation of the terms must lead to equal results regarding (==)? But if this is the case, what about terms of types which aren't instances of Eq? Furthermore, wouldn't equivalence be undefined if at least one of the two terms is _|_. Or does the = mean that the results of both terms must have exactly the same structure. But if this is true, what would it mean that two functions have the same structure? Does the = even include that all free variables occuring in t and/or t' must be evaluated the same way? In the following example, for instance, f x and g x wouldn't be equivalent according to the last definition although they would yield the same result for every x: f :: () -> () f _ = undefined g :: () -> () g () = undefined When evaluating f x, nothing of x would be evaluated which wouldn't be the case when evaluating g x. So x is not evaluated the same way in f x and g x but both terms always yield the same result (always _|_). Consider replacing each of the two occurences of undefined above by (). The difference in the evaluation of x would now result in different results of f x and g x if x = undefined. f x would be () and g x would be _|_. Where difference in free variable evaluation causes difference in term results there requirement of result equivalence of course includes requirement of "free variable evaluation equivalence". In these cases the second and the third definition approach from the beginning of this mail would be equivalent. Now let's consider the Monad/MonadPlus law m >>= \x -> mzero = mzero and the monadic instances of []. Here we have the case that evaluation behaviour of m is not the same for both terms. (The second term doesn't even contain m and therefore does no evaluation of m at all which is of course not true for the first term.) And here the different evaluation behaviour of m results in both terms not having the same result for every m. For example undefined >>= \x -> mzero is not mzero but _|_. You may also take a term like [1 ..] >>= \x -> mzero which maybe looks harmless but also has _|_ as result. Does this mean that [] doesn't satisfy the Monad/MonadPlus laws? I'm interested in your answers regarding all these questions. Wolfgang