[Haskell-cafe] equational reasoning

[Roman Cheplyaka]

* Tillmann Rendel <rendel at cs.au.dk> [2009-02-19 22:43:24+0100]
> Roman Cheplyaka schrieb:
>> 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.
>
> Let's consider
>
>   omega = omega
>   const omega 42

I guess you meant "const 42 omega".

> which is evaluated to 42 in Haskell, but is nonterminating in an strict  
> language. I would expect every kind of semantics to account for this  
> difference.

It's slightly different. I understand that error ".." and omega have the
same denotation, but the difference is that omega does not have normal
form and error ".." is in normal form.

So non-termination of "const 42 omega" in a strict language is not
surprising (we know that strict evaluation does not always find normal
form, even if it exists), but "const 42 (error ...) = error ..." means that
different evaluation orders give us different normal forms, which is
denied by Church-Rosser.

> Second, who says Church-Rosser holds for Haskell?

Now I see that exceptions magic can break it. Is this what you mean?

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