On Thu, 2009-03-05 at 13:08 +0000, Simon Marlow wrote:
Lennart Augustsson wrote:
I don't see any breaking of referential transparence in your code. Every time you do an IO operation the result is basically non-deterministic since you are talking to the outside world. You're assuming the IO has some kind of semantics that Haskell makes no promises about.
I'm not saying that this isn't a problem, because it is. But it doesn't break referential transparency, it just makes the semantics of IO even more complicated.
(I don't have a formal proof that unsafeInterleaveIO cannot break RT, but I've not seen an example where it does yet.)
So the argument is something like: we can think of the result of a call to unsafeInterleaveIO as having been chosen at the time we called unsafeInterleaveIO, rather than when its result is actually evaluated. This is on dodgy ground, IMO: either you admit that the IO monad contains an Oracle, or you admit it can time-travel. I don't believe in either of those things :-)
That's the charm of denotational semantics --- you're outside the laws of physics. jcc