"Neil Mitchell"
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?
To add another viewpoint on what goes wrong: I think you're being seduced by syntax. When you say that you can replace "span (not . g)" with "break g", you require that the break you defined above be in scope. You wouldn't consider
bother = \break -> break . span (not . g)
to be a suitable candidate for replacement without doing an alpha conversion first. Now because the definitions in a haskell programme are all mutually recursive, there's really a big Y (fix) round the whole lot. Simplifying it a bit, you could say that unsugaring the definition
break g = span (not . g)
gives you
break g := fix (\break -> span (not . g))
(where ":=" denotes non-recursive definition). Now it's clear that you can't apply your equation in there, because the break you want to use isn't in scope. -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk