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