pseq strictness properties

[Simon Marlow]

Duncan Coutts wrote:
> I don't think I'm just speaking for myself when I say that pseq is
> confusing and the docs similarly.
> 
> Given the type
> 
> a -> b -> b
> 
> we would assume that it is lazy in it's first arg and strict in the
> second. (Even in the presence of seq we know that it really really must
> be strict in it's second arg since it returns it or _|_ in which case
> it's still strict).
> 
> Of course we know of the seq primitive with this type that is strict in
> both. However we also now have pseq that has the _opposite_ "static"
> strictness to the original expected strictness.
> 
> Statically, pseq claims that it's strict in the first but lazy in the
> parameter that it _returns_. At runtime of course it is strict in both
> parameters.
> 
> Given the need for pseq I would have expected pseq to statically be lazy
> in it's first argument (and actually be strict at runtime). I expected
> it'd statically be strict in the second arg.
> 
> So I'm wondering if there is a good explanation for pseq having the
> opposite strictness properties to that which I expected. At first, even
> after reading the docs I assumed that it was just a typo and that it
> really meant it was lazy in the first arg (statically). I was just
> recording a patch to "fix" the documentation when I checked the
> underlying code and found to my surprise that the original docs are
> correct.
> 
> I also think the docs need to be clarified to make this distinction
> between the actual strictness behaviour and what the compiler thinks it
> is during strictness analysis. Since they are different I think it's an
> important distinction to make.

Phil Trinder and others have been working on formalising the difference 
between pseq and seq, they might be able to tell you more.  But here's how 
I think of it:

Denotationally, pseq and seq are the interchangeable.  That's important, it 
tells you what the strictness of pseq is: it's the same as seq.

The difference between the two is entirely at the operational level, where 
we can talk about the order of evaluation.  'pseq x y' causes both x and y 
to be evaluated, and in the absence of any other demands on x and y, x will 
be evaluated earlier than y.

This isn't quite the same as saying "pseq x y" evaluates x and then y, 
although in many cases that is what happens.  The compiler is still free to 
move the evaluation of x earlier.  It might also be the case that y is 
already evaluated, so it's not true to say that x is always evaluated before y.

In order to make pseq work like this, we have to prevent GHC from 
performing certain transformations at compile-time.  That is because 
otherwise, GHC is allowed to make any transformations that respect the 
denotation of the program, but with pseq we want a guarantee at the 
operational level.  We want to prevent GHC from re-ordering evaluation such 
that y (or any "part of y" if y is a larger expression) is evaluated before 
x, but GHC can only do that if it knows that y is strictly demanded by 
pseq.  So by removing this information, using the lazy annotation, we 
prevent GHC from performing the offending transformations.

The docs probably shouldn't say anything about what the compiler sees, it 
should stick to what the programmer sees.  Duncan - do you want to try 
rewording it?

Cheers,
	Simon