bug in language definition (strictness)

[Peter Gammie]

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