strict bits of datatypes

[Nils Anders Danielsson]

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
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