Re: [Haskell-cafe] equational reasoning

On Thu, 2009-02-19 at 23:06 +0200, Roman Cheplyaka wrote:

* Wouter Swierstra [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