Neil Mitchell wrote:
Haskell is known for its power at equational reasoning - being able to treat a program like a set of theorems. For example:
break g = span (not . g)
Which means we can replace:
f = span (not . g)
with:
f = break g
by doing the opposite of inlining, and we still have a valid program.
However, if we use the rule that "anywhere we encounter span (not . g) we can replace it with break g" then we can redefine break as:
break g = break g
Clearly this went wrong! Is the folding back rule true in general, only in specific cases, or only modulo termination?
Well, from the equational point of view, the equation break p = break p is trivially valid, so nothing is wrong with equational reasoning. Of course, the definitions break p := span (not . p) and break p := break p are clearly different, since the latter implies break p = _|_ . It seems that "de-inlining" can make things less defined. But I think that this phenomenon is an artifact of working with named functions, similar to name capture. I guess it's not present for anonymous lambda terms. Regards, apfelmus