On 06/08/2009 13:49, Thomas Davie wrote:

On 6 Aug 2009, at 14:37, Nils Anders Danielsson wrote:

...

On 2009-08-06 11:08, Malcolm Wallace wrote:

...

yet, because of the definition of $!, this applies the constructor to its arguments right-to-left instead of the intuitive left-to-right.

I do not think that there is a bug: x `seq` y `seq` e has the same denotation as y `seq` x `seq` e.

Not if one considers the "kind" of bottom one receives:

undefined `seq` error "it exploded" `seq` e will print "Prelude.undefined" while error "it exploded" `seq` undefined `seq` e will print "Error: it exploded"

There's only one kind of bottom in Haskell 98. And even with the imprecise exceptions extension, both expressions still have the same denotation - they denote the same set of exceptions, one of which is non-deterministically picked when the program is run. Cheers, Simon

On 06/08/2009 14:20, Peter Gammie wrote:

On 06/08/2009, at 10:59 PM, Simon Marlow wrote:

...

On 06/08/2009 13:49, Thomas Davie wrote:

...

On 6 Aug 2009, at 14:37, Nils Anders Danielsson wrote:

...

On 2009-08-06 11:08, Malcolm Wallace wrote:

...

yet, because of the definition of $!, this applies the constructor to its arguments right-to-left instead of the intuitive left-to-right.

I do not think that there is a bug: x `seq` y `seq` e has the same denotation as y `seq` x `seq` e.

Not if one considers the "kind" of bottom one receives:

undefined `seq` error "it exploded" `seq` e will print "Prelude.undefined" while error "it exploded" `seq` undefined `seq` e will print "Error: it exploded"

There's only one kind of bottom in Haskell 98. And even with the imprecise exceptions extension, both expressions still have the same denotation - they denote the same set of exceptions, one of which is non-deterministically picked when the program is run.

If the FFI Addendum is considered part of Haskell 98, then we have unsafePerformIO, and so an appeal to denotational equivalence is not sufficient. When grafting a pure interface onto a notionally-pure library (specifically a BDD library), I often used seq to get these effects buried in "pure" values under control.

That sounds like a very dangerous use of seq and unsafePerformIO to me! The presence of unsafePerformIO doesn't change the meaning of the rest of Haskell. You can use it to write programs that don't behave according to the denotational semantics if you want, but if you do that it's considered an unsafe use of unsafePerformIO. What semantics would you like Haskell to have, in which (x `seq` y `seq` e) and (y `seq` x `seq` e) are not equal?

I also think the principle of least surprise is clearly violated here.

I do have some sympathy with that. The fact that we're having this discussion is evidence that something is wrong - and indeed it took quite a while before we noticed that seq doesn't actually enforce a sequential evaluation order. And seq was originally introduced to fix space leaks, but sometimes it can't be used for this because it doesn't provide enough operational guarantees (I haven't seen such cases myself, but Malcolm W tells me it really happens). I'm against the change originally proposed in this thread, because on its own it doesn't make any difference. But by all means let's think about ways to restore the lack of surprise, but which hopefully don't curtail the compiler's ability to optimise, or run programs in parallel. Cheers, Simon

On Thu, Aug 06, 2009 at 03:33:40PM +0100, Malcolm Wallace wrote:

...

What semantics would you like Haskell to have, in which (x `seq` y `seq` e) and (y `seq` x `seq` e) are not equal?

I can easily imagine that (x `seq` y `seq` e) might have *two* semantic denotations: bottom (Exception: stack overflow), and e. And I would like to be able to choose which one I get (please). This is the declared purpose of seq, namely "to improve performance by avoiding unneeded laziness".

There is no stack overflow in the denotational semantics. Either you would get an answer with a bigger stack (and that's the denotation), or you wouldn't (in which case the value is bottom). As Simon said, the denotational semantics of seq is very limited for specifying performance.

On 6 Aug 2009, at 17:34, Mathias Stearn wrote:

On Thu, Aug 6, 2009 at 11:00 AM, Ross Paterson wrote:

...

There is no stack overflow in the denotational semantics.

There is currently no denotational semantics simulator with an infinite stack. Until there is, Haskell programs will have to be executed on lowly physical computers with all the limitations that is implied. Can we please make things work well on them?

When writing a document that defines the denotation of values, no. Perhaps when considering operational semantics, but that's an entirely different matter. Bob

...

...

What semantics would you like Haskell to have, in which (x `seq` y `seq` e) and (y `seq` x `seq` e) are not equal?

I can easily imagine that (x `seq` y `seq` e) might have *two* semantic denotations: bottom (Exception: stack overflow), and e. And I would like to be able to choose which one I get (please). This is the declared purpose of seq, namely "to improve performance by avoiding unneeded laziness".

I'm afraid I don't really comprehend what you're getting at. What do you mean by an expression having two semantic denotations, and how would you like to choose which one you get? And I'm baffled by the mention of stack overflow, where does that come in?

Whether it is a stack overflow, or some other kind of resource-related exception like out-of-memory, or too-many-open-file-handles, does not really matter. As you were saying, semantically they are all just bottom. My real point is that seq looks for all the world like it is intended to affect the operational behaviour of a program, yet some people insist that it is a purely denotational device, and that operational questions are not relevant. The Report hints that using seq can "improve performance" (although the opposite is also true), and changes in performance are certainly an operational notion. Yet I think it would be valid to say that seq can turn a non-terminating (exceptioning) program into a terminating one. Regards, Malcolm

...

Yet I think it would be valid to say that seq can turn a non-terminating (exceptioning) program into a terminating one.

Do you have an example of that?

Sure. foldl (+) 0 [1..10000000] :: Integer *** Exception: stack overflow foldl' (+) 0 [1..10000000] :: Integer 50000005000000 The only difference between foldl and foldl' is strictness (the use of seq). By "non-terminating (exceptioning)" I of course really meant "terminating with bottom" as opposed to "terminating with a defined value", but since non-termination and exceptions are semantically both bottom, you won't mind that slip. :-) Regards, Malcolm

Dan Weston wrote:

...

foldl (+) 0 [1..10000000] :: Integer *** Exception: stack overflow foldl' (+) 0 [1..10000000] :: Integer 50000005000000

I thought both of these were perfectly well defined in denotational semantics (and equal to 50000005000000). The first is merely a failure of one person's computer to implement the (perfectly well-defined) denotational semantics of the program.

Quite. It's slightly confusing that a stack overflow manifests in the same way as an exception that indicates _|_, such as error or divide by zero. It's exactly the same as if you'd pressed Control-C during the first evaluation. That doesn't cause the expression to have value _|_, but it does raise an exception. The type of the exception is some help: StackOverflow is a constructor in the AsyncException datatype, indicating that it was an asynchronous exception. Evaluating the expression again might yield a result. Cheers, Simon

On 07/08/2009, at 12:00 AM, Simon Marlow wrote:

On 06/08/2009 14:20, Peter Gammie wrote:

...

On 06/08/2009, at 10:59 PM, Simon Marlow wrote:

...

On 06/08/2009 13:49, Thomas Davie wrote:

...

On 6 Aug 2009, at 14:37, Nils Anders Danielsson wrote:

...

On 2009-08-06 11:08, Malcolm Wallace wrote:

...

yet, because of the definition of $!, this applies the constructor to its arguments right-to-left instead of the intuitive left-to- right.

I do not think that there is a bug: x `seq` y `seq` e has the same denotation as y `seq` x `seq` e.

Not if one considers the "kind" of bottom one receives:

undefined `seq` error "it exploded" `seq` e will print "Prelude.undefined" while error "it exploded" `seq` undefined `seq` e will print "Error: it exploded"

There's only one kind of bottom in Haskell 98. And even with the imprecise exceptions extension, both expressions still have the same denotation - they denote the same set of exceptions, one of which is non-deterministically picked when the program is run.

If the FFI Addendum is considered part of Haskell 98, then we have unsafePerformIO, and so an appeal to denotational equivalence is not sufficient. When grafting a pure interface onto a notionally-pure library (specifically a BDD library), I often used seq to get these effects buried in "pure" values under control.

That sounds like a very dangerous use of seq and unsafePerformIO to me!

How so? Take this code: newtype BDD = BDD (ForeignPtr Int) exists :: Group BDD -> BDD -> BDD exists group bdd = bdd `seq` unsafePerformIO $ withGroup group $ \ gid -> do bdd_assoc bdd_manager gid withBDD bdd ({#call unsafe bdd_exists#} bdd_manager) >>= addBDDfinalizer Without the seq, a recursive use of a quantifier will screw up the effect of bdd_assoc. How is this unsafe? IMHO I'm using seq in the standard way, to shuffle the data dependencies to get better (correct) operational behaviour. I grant that it is dodgy in a concurrent setting, but the library itself is not thread safe.

What semantics would you like Haskell to have, in which (x `seq` y `seq` e) and (y `seq` x `seq` e) are not equal?

As Malcolm observes, an operational one. seq is difficult to motivate without such considerations anyway. I'm sure you could imagine an example where space use differs between the two. My point was that in the presence of unsafePerformIO, even if the denotational values are the same for the two seq variants, the end- user observable effects are not. I meant this as an example of violating least-surprise in a context a bit larger than pure Haskell semantics. BTW I have no opinion on the change Malcolm proposes, but would like to see the issue resolved. cheers peter

On 07/08/2009, at 6:04 PM, Simon Marlow wrote:

If, as I understand it, you are relying on the fact that seq's first argument is evaluted before its second, then you really want pseq rather than seq.

This is the sense in which I mean it's a dangerous use of seq and unsafePerformIO - because the compiler is within its rights to evaluate the second argument to seq "first".

In GHC we provide a way to do what you want (pseq), I'm just not convinced it should be the required behaviour of seq.

OK, thanks for pointing that out. I would have thought that what I was doing (or trying to do) was a reasonable use of the FFI and unsafePerformIO - from the library user's POV the interface really is pure, at least in a sequential setting. So should there be a mechanism for guaranteeing left-to-right evaluation ala pseq in Haskell Prime? cheers peter

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? Thanks, - Ravi On Fri, Aug 7, 2009 at 6:30 AM, Malcolm Wallace wrote:

...

If, as I understand it, you are relying on the fact that seq's first argument is evaluted before its second, then you really want pseq rather than seq.

In GHC we provide a way to do what you want (pseq), I'm just not convinced it should be the required behaviour of seq.

Whilst looking for something else, I have discovered that the official list of changes from Haskell 1.2 to Haskell 1.3 has this explicit statement:

"The seq function evaluates its first argument before returning the second one."        http://haskell.org/definition/from12to13.html

In addition, the 1.3 and 1.4 Reports, in describing how seq should be understood for any particular type, states:

"The _case_ is used to force evaluation of the first argument to `seq` before returning the second argument."

The Haskell'98 committee decided to remove the Eval class (that had seq as one of its methods), see http://www.cs.chalmers.se/~rjmh/Haskell/Messages/Decision.cgi?id=204

I assume that it was simply inattention whilst editing the Report text, that caused the removal of the official requirement that seq evaluate its first argument before its second, because I can find no discussion by the committee that suggested such an important change.

If you can point me to the committee discussion that led to changing this requirement, I would be grateful.

Regards,    Malcolm

_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime

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/

On Fri, Aug 07, 2009 at 08:56:39AM +1000, Peter Gammie wrote:

How so? Take this code:

newtype BDD = BDD (ForeignPtr Int)

exists :: Group BDD -> BDD -> BDD exists group bdd = bdd `seq` unsafePerformIO $ withGroup group $ \ gid -> do bdd_assoc bdd_manager gid withBDD bdd ({#call unsafe bdd_exists#} bdd_manager) >>= addBDDfinalizer

Just a question, why not do

How so? Take this code:

newtype BDD = BDD (ForeignPtr Int)

exists :: Group BDD -> BDD -> BDD exists group bdd = unsafePerformIO $ bdd <- evaluate bdd withGroup group $ \ gid -> do bdd_assoc bdd_manager gid withBDD bdd ({#call unsafe bdd_exists#} bdd_manager) >>= addBDDfinalizer

It seems that evaluate is exactly the thing to order evaluations in the IO monad. John -- John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/