On Oct 11, 2006, at 10:14 AM, Malcolm Wallace wrote:
Matthias Fischmann <[EMAIL PROTECTED]> 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
