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. Now that I look at it, par has the same property, of statically being lazy in the second parameter that it returns (and thus is really strict). Again, this is not documented. Summary: why is it that way round, and can we think of a way to explain it better. Duncan
duncan.coutts:
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.
Could you state "static" strictness as a StrictCheck property? I'm not quite sure what this distinction means, actually. -- Don
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 .. I'm not quite sure what this distinction means, actually.
If I recall the issue correctly: - 'seq' is strict in both parameters (in the second, by being like 'flip const', and in the first, by its special nature). - given that both parameters are thus needed, there is nothing to force the 'a' to be evalutated *before* the 'b'; many programs using 'seq' tend to rely on this property (which the implementation is free to ignore). - 'pseq' is still strict in both parameters, but was meant to offer better evaluation-order guarantees than 'seq' does. - a strict variant of 'case', somewhat like 'case a of !a -> b', might express the intent more closely but then one would want to abstract over it for composition, running back into 'seq'. Hope this isn't too far off;-) Claus ps. it is unfortunate that the docs try to explain evaluation order in terms of how the compiler reacts to manipulating its knowledge about strictness. Strictness of both 'seq' and 'pseq' is as one would expect, and how the intended evaluation order guarantee is achieved is strictly and subtly an implementation matter (not permitting any transformations would also work, for instance).
On Thu, 2008-11-20 at 15:33 -0800, Don Stewart wrote:
duncan.coutts:
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.
Could you state "static" strictness as a StrictCheck property? I'm not quite sure what this distinction means, actually.
No, because StrictCheck can only check actual strictness properties. I mean actually passing in _|_ and getting _|_ out, at runtime. For pseq there is its actual strictness (it's strict in both args) but then the strictness that we tell the optimiser is different. We claim that it is lazy in it's second argument. That means that the optimiser is not able to do certain transformations that it might otherwise do. Basically it cannot propagate the strictness information upwards to earlier expressions or callers. -- "pseq" is defined a bit weirdly (see below) -- -- The reason for the strange "lazy" call is that it -- fools the compiler into thinking that pseq and par are non-strict in -- their second argument (even if it inlines pseq at the call site). -- If it thinks pseq is strict in "y", then it often evaluates -- "y" before "x", which is totally wrong. {-# INLINE pseq #-} pseq :: a -> b -> b pseq x y = x `seq` lazy y {-# INLINE par #-} par :: a -> b -> b par x y = case (par# x) of { _ -> lazy y } The lazy x function is a primitive that is the same as id, except that it lies to the optimiser and claims that it is not strict. Duncan
On Thu, 2008-11-20 at 15:33 -0800, Don Stewart wrote:
duncan.coutts:
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.
Could you state "static" strictness as a StrictCheck property? I'm not quite sure what this distinction means, actually.
Note that you could make the actual and declared strictness match each other more closely by defining pseq to have the type: pseq :: a -> b -> (# b #) Now it's clear that it returns the second argument unevaluated. Of course that'd be a lot less convenient to use. Duncan
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
On Fri, 2008-11-21 at 10:53 +0000, Simon Marlow wrote:
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?
Hmm, though the difference is really in what transformations you want the compiler not to do. I would not say the operational behaviour is actually different. Used in isolation there's really no way to distinguish them, even using trace and other tricks to observe the evaluation order. I guess we can try to simplify it to something like "evaluation happens here" (pseq) vs "evaluation happens here or before" (seq). Duncan
Duncan Coutts wrote:
On Fri, 2008-11-21 at 10:53 +0000, Simon Marlow wrote:
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?
Hmm, though the difference is really in what transformations you want the compiler not to do. I would not say the operational behaviour is actually different. Used in isolation there's really no way to distinguish them, even using trace and other tricks to observe the evaluation order.
Yes, to be more precise, the difference is in what *guarantees* you get about operational behaviour. You might be able to observe a difference with trace, or you might not, depending on what the compiler did. Using trace you will always observe pseq's first argument evaluated before its second, that's not true of seq.
I guess we can try to simplify it to something like "evaluation happens here" (pseq) vs "evaluation happens here or before" (seq).
Ok, but we need to be careful: it would be wrong to talk about ordering at all with respect to seq, since it tells you nothing about ordering. The implementation might be using a non-lazy evaluation strategy, for example. Cheers, Simon
Duncan Coutts
I guess we can try to simplify it to something like "evaluation happens here" (pseq) vs "evaluation happens here or before" (seq).
No, that is not correct, or at least it is highly misleading. The key difference between them is that: (x `pseq` y) = if y is not yet in WHNF, the compiler guarantees that x will be evaluated to WHNF before y. (x `seq` y) = if y is not yet in WHNF, the compiler can choose whether to evaluate y to WHNF before x, or x before y. In other words, pseq guarantees sequencing (given a side condition), whilst seq does not guarantee sequencing. Regards, Malcolm
participants (5)
-
Claus Reinke -
Don Stewart -
Duncan Coutts -
Malcolm Wallace -
Simon Marlow