strict bits of datatypes

Nils Anders Danielsson nad at
Tue Mar 20 14:59:14 EDT 2007

On Tue, 20 Mar 2007, "Bernie Pope" <bjpop at> 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 mailing list