Re: [Haskell-cafe] beginner's problem about lists

11 Oct 2006

      On Oct 11, 2006, at 10:14 AM, Malcolm Wallace wrote:
...
Matthias Fischmann  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

Re: [Haskell-cafe] beginner's problem about lists

Robert Dockins