strict bits of datatypes
Lennart Augustsson
lennart at augustsson.net
Fri Mar 16 21:08:57 EDT 2007
Given the translation of strict constructors I can't anything but _|_
as the answer.
On Mar 16, 2007, at 15:50 , Ian Lynagh wrote:
>
> 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
>
> _______________________________________________
> Haskell-prime mailing list
> Haskell-prime at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-prime
More information about the Haskell-prime
mailing list