[Haskell-cafe] beginner's problem about lists

[Robert Dockins]

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