Confused about seq and forms.

[Jay Cox]

Somewhere (either Algorithms: AFA, some paper, or the haskell report) I
read that seq evaluates its first argument to head normal form.  I
remember posting on this message forum or haskell-cafe that it evaluates
the first argument to weak head normal form.  At the time, I thought
I was right, THEN I read whatever I read (I just cannot find the
reference! sorry!)  I also know that sometimes shoot off my mouth,
(or in this case, my fingers!).  I want to get my facts right.
I still am trying to write a document about strictness and haskell
evaluation for those of us without research degrees ;-)

Anyway.  my only other source is foldoc.

head normal form

        (HNF) A lambda expression is in head normal form if its top
        level is either a variable, a data value, a built-in function
        applied to too few arguments or a lambda abstraction whose
        body is not reducible.  I.e. the top level is neither a redex
        nor a lambda abstraction with a reducible body.

        An expression in HNF may contain redexes in argument postions
        whereas a normal form may not.  See also Weak head normal
        form.

I shall not post WHNF def as it is rather large.  search google for foldoc
if you want it.  But the key thing is this example:

        The term was coined by {Simon Peyton Jones} to make explicit
        the difference between {head normal form} (HNF) and what
        {graph reduction} systems produce in practice.  A lambda
        abstraction with a reducible body, e.g.

                \ x . ((\ y . y+x) 2)

        is in WHNF but not HNF.

so it looks if seq reduced to head normal form, above would be
reduced to (\x . 2+y)

seq (\x ->(\y->reverse y) [1..])
this would seem to reduce indefinately to get to head normal form.

The haskell report says can be used to tell the difference between
_|_ and (\x->_|_).  I'm not sure how, unless the following is what
is meant to be demonstrated.

Prelude> seq (error "foo") False
*** Exception: foo
Prelude> seq (\x -> error "foo") False
False

So, I guess, my first real question is,

Which of HNF or WHNF does seq reduce its first argument to?  It still
appears to be WHNF but maybe I'm confused about HNF.



Any referal to a paper describing the differences between HNF and WHNF
(yes, that includes yours Simon PJ!) would be appreciated.  Actually,
I really, really want that reference to at least read that bit about WHNF.
However, I'd love any correction or verefication of my thinking process.

Thanks,

Jay Cox