[Haskell-cafe] equational reasoning

Roman Cheplyaka roma at ro-che.info
Thu Feb 19 16:06:15 EST 2009

* 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

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

More information about the Haskell-Cafe mailing list