Robert Dockins robdockins at fastmail.fm
Wed Oct 11 11:04:49 EDT 2006

```On Oct 11, 2006, at 10:14 AM, Malcolm Wallace wrote:

> Matthias Fischmann <fis at wiwi.hu-berlin.de> wrote:
>
>>> No, your Fin type can also hold infinite values.
>>
>> let q = FinCons 3 q in case q of FinCons i _ -> i  ==>  _|_
>>
>> does that contradict, or did i just not understand what you are
>> saying?
>
> That may be the result in ghc, but nhc98 gives the answer 3.
>
> It is not entirely clear which implementation is correct.  The
> Language
> Report has little enough to say about strict components of data
> structures - a single paragraph in 4.2.1.  It defines them in terms of
> the strict application operator (\$!), thus ultimately in terms of seq,
> and as far as I can see, nhc98 is perfectly compliant here.
>
> 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.

Let's do some algebra.

data FinList a = FinCons a !(FinList a)

let q = FinCons 3 q in q
==>
let q = ((\x1 x2 -> (FinCons \$ x1)) \$! x2) 3 q in q   (translation
from 4.2.1)
==>
let q = (FinCons \$ 3) \$! q in q                     (beta)
==>
let q = (\$!) ((\$) FinCons 3) q in q                 (syntax)
==>
let q = (\$!) ((\f x -> f x) FinCons 3) q in q       (unfold (\$))
==>
let q = (\$!) (FinCons 3) q in q                     (beta)
==>
let q = (\f x -> seq x (f x)) (FinCons 3) q in q    (unfold (\$!))
==>
let q = seq q (FinCons 3 q) in q                    (beta)

We have (from section 6.2):
seq _|_ y = _|_
seq x y = y    iff x /= _|_

Now, here we have an interesting dilemma.  Suppose q is _|_, then:

let q = seq q (FinCons 3 q) in q
==>
let q = _|_ in q                                    (specification of
seq)
==>
_|_                                                 (unfold let)

Instead suppose q /= _|_, then:

let q = seq q (FinCons 3 q) in q
==>
let q = FinCons 3 q in q                            (specification of
seq)
==>
let q = FinCons 3 q in FinCons 3 q        (unfold let)
==>
FinCons 3 (let q = FinCons 3 q in q)           (float let)

It seems that both answers are valid, in that they conform to the
specification.  Is 'seq' under-specified?  Using a straightforward
operational interpretation, you will probably get the first answer, _|
_, and this is what I have always assumed.  The second requires a
sort of strange "leap of faith" to arrive at that answer (ie, assume
'q' is non-bottom), and is less satisfying to me.  What do others think?

> Regards,
>     Malcolm

Rob Dockins

Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
-- TMBG

```