[Haskell-cafe] Equational Reasoning goes wrong

Neil Mitchell ndmitchell at gmail.com
Sun Jul 22 10:53:51 EDT 2007


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)


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?



More information about the Haskell-Cafe mailing list