Confused about seq and forms.

[Janis Voigtlaender]

Jay Cox wrote:

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

seq reduces its first argument to weak head normal form, as in:

f = seq (const undefined) "good"
g = seq undefined "bad"

Main> f
"good"
(93 reductions, 148 cells)
Main> g
"
Program error: {undefined}
(12 reductions, 56 cells)


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

Here the argument is in WHNF but not in HNF. Supplied with a second
argument, seq would return this:

h = seq (\x ->(\y->reverse y) [1..]) "good"

Main> h
"good"
(89 reductions, 124 cells)


> 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

That is exactly the point. And it is a bit weird, because it would seem
that for a function it would make no difference, whether it is _|_ or
(\x->_|_), because all you can do operationally with a function (if seq
is not present) is to apply it to some argument and both _|_ and
(\x->_|_) would give back _|_ in this case. But since seq is present in
Haskell 98 (and for good reason: efficiency), this intuition breaks
down: _|_ ARE (\x->_|_) different.
As the Haskell report states, this weakens Haskell's parametricity
properties, making for example shortcut deforestation (foldr c n (build
g) = g c n) wrong in the presence of seq:

build:: (forall b . (a -> b -> b) -> b -> b) -> [a]
build g = g (:) []

u :: [Int]
u = foldr undefined [] (build seq)

v :: [Int]
v = seq undefined []

Main> u
[]
(20 reductions, 35 cells)
Main> v

Program error: {undefined}
(10 reductions, 51 cells)


Hope the above helped to understand seq better.

Janis.

--
Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt@tcs.inf.tu-dresden.de