bug in language definition (strictness)

[John Meacham]

On Mon, Aug 17, 2009 at 01:02:29PM +0100, Simon Marlow wrote:
> On 07/08/2009 12:17, Ravi Nanavati wrote:
>> I wonder if this discussion has veered too far into legalistic
>> reasoning (of various sorts). From where I'm standing the
>> state-of-play is this:
>>
>> 1. Compiler writers (and some users) want a "liberal" version of seq
>> (that's slippery about evaluation order) for optimizations and better
>> correspondence with the denotational semantics.
>> 2. Other users want a version of seq that guarantees evaluation order
>> for use cases where that matters.
>>
>> Is there any deep reason why we don't just figure out what the best
>> way to give people both versions of seq is and do that?
>
> Compilers can provide seq with an ordering guarantee if they want, just  
> as GHC does with Control.Parallel.pseq.  I don't think it would be good  
> to mandate this in the standard, for the reassons I've already described  
> in this thread, in summary:
>
>  - it constrains evaluation order in a way that Haskell
>    doesn't currently do, and which might prevent interesting
>    implementations (e.g. automatic parallelisation)
>
>  - it's not clear how to specify what "seq with an ordering guarantee"
>    actually means.  If someone were to come up with a precise
>    definition, that would be a much better basis for discussion.

What is interesting is that pseq, or seq with an ordering guarentee,
actually would introduce a lazyness, instead of strictness. in order to
see this, we can observe what will have with the strictness analyzer.
imagine the function

f :: Int -> Int -> Int
f x y = y `seq` x

Now, the strictness analysis will see that f is strict in both its
arguments, y because of seq, and x because it is what returned. we can
say it derives the following annotated type (where ! means strict)

f :: !Int -> !Int -> Int

now, anything that calls f is free to evaluate its arguments before
passing them to f, more importantly, it enables things like the
worker-wrapper transform and unboxing. however if we have

f x y = y `pseq` x

now, what is the strictness for f?
Although f is still 'strict' in both arguments in that it evaluates
both, in order to guarentee the ordering that its second argument is
evaluated before its first, it must be lazy in its first argument. or:

f :: Int -> !Int -> Int

otherwise the calling function may evaluate the first argument before
the second, since the strictness information doesn't include ordering
information.  So, adding a 'pseq' actually gets rid of strictness.

things get worse with something like

j :: Bool -> Int -> Int -> Int
j b x y = if b then f x y else f y x


even though j is obviously strict in all its arguments in that it
evaluates them all, the compiler cannot derive that fact since it
doesn't know the _order_ in which they are strict.


This suggests a natural implementation (and specification) for pseq,

pseq :: a -> b -> b
pseq x y = x `seq` lazy y

where lazy :: a -> a is a compiler provided function equivalent to 'id'
except that it is considered lazy in its argument by the strictness
analyzer.


So, I think an order preserving 'seq' is possible, but it has the ironic
quality of introducing lazyness, rather than strictness.

And if anything were proposed as a cross-compiler convention, I think
'lazy' would be a more useful and less confusing function to introduce
as a portable primitive.


        John



-- 
John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/