"Neil Mitchell" <[EMAIL PROTECTED]> writes: > 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 [EMAIL PROTECTED] _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
