[Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe
sabel at ki.informatik.uni-frankfurt.de
Thu Apr 18 20:32:38 CEST 2013
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:
>> 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.
>> 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).
>> 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.
> 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.
More information about the Haskell-Cafe