[Haskell-cafe] equational reasoning
roma at ro-che.info
Fri Feb 20 02:47:54 EST 2009
* 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
> 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
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
More information about the Haskell-Cafe