
22 Jul
2007
22 Jul
'07
10:53 a.m.
Hi 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? Thanks Neil