strict bits of datatypes
Nils Anders Danielsson
nad at cs.chalmers.se
Tue Mar 20 14:59:14 EDT 2007
On Tue, 20 Mar 2007, "Bernie Pope" <bjpop at csse.unimelb.edu.au> 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
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.)
More information about the Haskell-prime