bug in language definition (strictness)

[Simon Marlow]

On 06/08/2009 17:42, 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".
>>
>> 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 fact remains that seq *is* defined denotationally, and any 
implementation that respects its semantics is legal.  If you want to 
change that, you need to make a Haskell Prime proposal.

I think it might be difficult to do that.  The Haskell report has no 
framework for talking about operational semantics at all.  The pure 
subset of Haskell is timeless, there's no specified evaluation order. 
Before we think about changing that, let's remember why it's that way: 
one reason is that evaluation order doesn't affect the denotational 
semantics, so it's unnecessary.  Another reason is that it lets Haskell 
admit many different implementations, including things like automatic 
speculative parallelism.  If you start nailing down evaluation orders, 
you rule out interesting implementations.  (this is why I've complained 
about lazy I/O in the past - it starts to creep in this direction).

There's nothing stopping you from making a compiler in which seq has the 
behaviour you want.  Indeed, Control.Parallel.pseq is the kind of seq 
you want (I think - we haven't put any thought into precisely specifying 
what it means).  pseq is a valid implementation of seq, it's just not 
the one we normally want to use, because it restricts the compiler's 
ability to optimise.  And pseq isn't something we want to mandate in the 
language, because it only makes sense in certain kinds of 
implementations.  I'm completely happy with asking users to use pseq 
when they really want an evaluation order guarantee.

> 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?

Cheers,
	Simon