[Haskell-cafe] equational reasoning

[Jonathan Cast]

On Thu, 2009-02-19 at 23:06 +0200, Roman Cheplyaka wrote:
> * Wouter Swierstra <wss at cs.nott.ac.uk> [2009-02-19 11:58:38+0100]
> > There are several problems with this approach.
> >
> > For example, I can show:
> >
> > const 0 (head []) = 0
> >
> > But if I pretend that I don't know that Haskell is lazy:
> >
> > const 0 (head []) = const 0 (error ....) = error ...
> 
> Where does the last equality come from?

Pretending Haskell is strict.  It would be an axiom of Strict Haskell,
were someone to write such a thing, that

  forall a b (x :: String) (f :: a -> b). f (error x) = error x :: b

With the side condition that f is a lambda.

Then, we would know that, if f is a lambda of arity > 1 (or a constant
defined to be such a lambda), that (f a), where a is a value (such as
0), is equal to some lambda; so by congruence and the equation above, we
get (f a (error x) = error x) for all values a.

Which doesn't obviate the point that any proof-checker for *Haskell*
worth its salt would reject any alleged proof of (const 0 (error x) =
error x).

jcc