Haskell is known for its power at equational reasoning - being able to treat a program like a set of theorems.
when you're trying to do equational reasoning, you better make sure that you're reasoning with equations. as others have pointed out some of the more interesting relations between programs are inequations, where one side is defined in all cases in which the other is, and both sides are equal whenever both are defined. the interesting bit here is that the equation you're trying to use is also part of the program in which you're going to use it (unlike flat sets of theorems), and if you apply the equation to parts of itself, you might change it. by sawing off the branch of logic you're working from, you might then find yourself suspended in mid air. at the point of definition for an equation 'lhs = rhs', we have an inequation: lhs is not yet defined, rhs presumably is, and then we declare them to be equivalent, so that lhs is defined whenever rhs is, and both have equal values whenever both are defined. in other words, as long as/whereever our new definition holds, we can use it as an equation, whereas we only have an inequation if we start fiddling with the definition itself. if we replace lhs with rhs in the definition (making the left hand side "more defined"), we get something valid (semantically, though not necessarily syntactically) but useless - a tautology that only "defines" what already was. if we replace rhs with lhs in the definition (making the right hand side "less defined"), we get another valid but useless equation - a tautology that does not add any information to help make a useful new definition. [this is the variant that loops, making no progress towards producing information] if our definition is recursive, and we replace an occurrence of lhs in rhs with an instance of rhs, we have not changed the information content of the definition. a very useful group of transformations in non-strict languages (when you want to make your code less strict, eg in cyclic programming) are the eta-expansions: f --> \x.(f x) -- f is a function p --> (fst p,snd p) -- p is a pair l --> (head l:tail l) -- l is a list .. all of which add information by "borrowing from the future" - if f,p,l turn out to be defined, the above are equations, otherwise they are inequations, the rhs being more defined than the lhs (because the future payback never happens). in particular: Prelude> let x = x Prelude> :t x x :: t Prelude> let r = (\y->x y,(fst x,snd x),(head x:tail x)) Prelude> :t r r :: (t -> t1, (a, b), [a1]) Prelude> let f (a,(_,_),(_:_)) = a `seq` () Prelude> :t f f :: (t, (t1, t2), [t3]) -> () Prelude> f r () while Prelude> f (x,x,x) Interrupted. well, at least that is my naive way of looking at these things;-) claus