On Tue, 20 Mar 2007, "Bernie Pope" <[EMAIL PROTECTED]> wrote:
> Malcolm wrote: >> x = x `seq` foo > We can translate the definition of x into: > > x = fix (\y -> seq y foo) > > Isn't it the case that, denotationally, _|_ and foo are valid > interpretations of the rhs? > > If we want to choose between them then we need something extra, such as an > operational semantics, or a rule saying that we prefer the least solution. We already have such a rule. According to the H98 report the let expression let x = x `seq` foo in ... can be translated into let x = fix (\~y -> y `seq` foo) in ... where "fix is the least fixpoint operator". Now, since seq ⊥ x = ⊥ we get that ⊥ is the least fixpoint of (\~y -> y `seq` foo), so the above _is_ equivalent to let x = ⊥ in ... (If x is also, by some other reading of the report, equivalent to some non-bottom expression, then the report should be fixed.) -- /NAD _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
