strict bits of datatypes

[Ian Lynagh]

Hi all,

A while ago there was a discussion on haskell-cafe about the semantics
of strict bits in datatypes that never reached a conclusion; I've
checked with Malcolm and there is still disagreement about the right
answer. The original thread is around here:
http://www.haskell.org/pipermail/haskell-cafe/2006-October/018804.html
but I will try to give all the relevant information in this message.

The question is, given:

    data Fin a = FinCons a !(Fin a) | FinNil

    w = let q = FinCons 3 q
        in case q of
               FinCons i _ -> i

is w 3 or _|_?

---------- The _|_ argument ----------

(Supporters include me, ghc and hugs)

    q = FinCons 3 q
=== (by Haskell 98 report 4.2.1/Strictness Flags/Translation
    q = (FinCons $ 3) $! q
=== (by definition of $, $!)
    q = q `seq` FinCons 3 q
=== (solution is least fixed point of the equation)
    q = _|_

Thus

w = case _|_ of
        FinCons i _ -> i

so w = _|_.


---------- The 3 argument ----------

(Supporters include Malcolm Wallace, nhc98 and yhc)

Here I will just quote what Malcolm said in his original message:

    The definition of seq is
        seq _|_ b = _|_
        seq  a  b = b, if a/= _|_

    In the circular expression
        let q = FinCons 3 q in q
    it is clear that the second component of the FinCons constructor is not
    _|_ (it has at least a FinCons constructor), and therefore it does not
    matter what its full unfolding is.

and in his recent e-mail to me:

    Yes, I still think this is a reasonable interpretation of the Report.  I
    would phrase it as "After evaluating the constructor expression to WHNF,
    any strict fields contained in it are also be guaranteed to be in WHNF."

This also makes q a fixpoint of q = q `seq` FinCons 3 q, but not the
least fixed point.

----------

So I think it would be good if we can all agree on what the meaning
should be, and then to clarify the wording in the report so that future
readers understand it correctly too.


Thanks
Ian