[Haskell-cafe] Re: Equational Reasoning goes wrong

apfelmus apfelmus at quantentunnel.de
Sun Jul 22 11:57:27 EDT 2007

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)


  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.


More information about the Haskell-Cafe mailing list