[Haskell-cafe] equational reasoning

[Roman Cheplyaka]

* 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?

> Which would allow me to substitute each occurrence of 0 with "error" -  
> which probably isn't a good idea. So to do proper equational reasoning in 
> a lazy language you need to be extremely careful with evaluation order. 

Evaluation order matters for operational semantics, not for axiomatic.
And even in operational semantics Church–Rosser theorem should prevent
getting different results (e.g. 0 and error) for different evaluation
orders.

Please correct me if I'm wrong.

-- 
Roman I. Cheplyaka :: http://ro-che.info/
"Don't let school get in the way of your education." - Mark Twain