[Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe
duncan.coutts at googlemail.com
Thu Apr 18 15:17:43 CEST 2013
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. That
said, it might not be such a useful semantics because we often want the
lazy behaviour of a lazy future.
More information about the Haskell-Cafe