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:
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.
I agree.
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.
Yes our result should hold for any scheduling.
That
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.
Best wishes,
David
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
