[Haskell-cafe] Re: Equational Reasoning goes wrong

[Jon Fairbairn]

"Neil Mitchell" <ndmitchell at gmail.com> 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                                 Jon.Fairbairn at cl.cam.ac.uk