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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe