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

[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.

> 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. That
said, it might not be such a useful semantics because we often want the
lazy behaviour of a lazy future.

Duncan