[Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe

[David Sabel]

Am 18.04.2013 15:17, schrieb Duncan Coutts:
> On Mon, 2013-04-15 at 20:44 +0200, David Sabel wrote:
>
>> A very interesting discussion,  I may add my 2 cents:
>>      making unsafeInterleaveIO nondeterministic indeed seems to make it safe,
>>      more or less this was proved in our paper:
>>
>> http://www.ki.informatik.uni-frankfurt.de/papers/sabel/chf-conservative-lics.pdf
>> slides:
>> http://www.ki.informatik.uni-frankfurt.de/persons/sabel/chf-conservative.pdf
>>
>> there we proposed an extension to Concurrent Haskell which adds a primitive
>>
>> future :: IO a -> IO a
>>
>> Roughly speaking future is like unsafeInterleaveIO, but creates a new
>> concurrent thread
>> to compute the result of the IO-action interleaved without any fixed order.
> That's very interesting to hear. It has always been my intuition that
> the right way to understand unsafeInterleaveIO is using a concurrency
> semantics (with a demonic scheduler). And whenever this
> "unsafeInterleaveIO is unsound" issue comes up, that's the argument I
> make to whoever will listen! ;-)
>
> That intuition goes some way to explain why unsafeInterleaveIO is fine
> but unsafeInterleaveST is right out: ST is supposed to be deterministic,
> but IO can be non-deterministic.
I agree.
>
>> We have shown that adding this primitive to the functional core language
>> is 'safe' in the sense
>> that all program equations of the pure language still hold in the
>> extended language
>> (which we call a conservative extension in the above paper)
>>
>> The used equality is contextual equivalence
>> (with may- and a variant of must-convergence in the concurrent case).
> Ok.
>
>> We also showed that adding unsafeInterleaveIO (called lazy futures in
>> the paper..)
>> - which delays until its result is demanded - breaks this conservativity,
>> since the order of evaluation can be observed.
> My conjecture is that with a concurrent semantics with a demonic
> scheduler then unsafeInterleaveIO is still fine, essentially because the
> semantics would not distinguish it from your 'future' primitive.
Yes our result should  hold for any scheduling.

> That
> said, it might not be such a useful semantics because we often want the
> lazy behaviour of a lazy future.
Yes I agree with that, too.

Best wishes,
  David