[Haskell-cafe] Proof that Haskell is RT

[Jonathan Cast]

On Wed, 2008-11-12 at 18:47 -0500, Dan Doel wrote:
> On Wednesday 12 November 2008 6:18:38 pm David MacIver wrote:
> > To put it a different way, in the absence of unsafeInterleaveIO the IO
> > monad has the property that if f and g are observably equal up to
> > termination then x >>= f and x >>= g are equivalent in the IO monad
> > (actually this may not be true due to exception handling. Our three
> > main weapons...). In the presence of unsafeInterleaveIO this property
> > is lost even though referential transparency is retained.
> 
> I'm not sure what exactly you mean by this, but, for instance:
> 
>     randomIO >>= (print :: Int -> IO ())
> 
> obviously isn't going to give the same results as:
> 
>     randomIO >>= (print :: Int -> IO ())
> 
> every time. Your weirdTuple is semantically similar, in that it selects 
> between returning (1,1) and (2,1), but instead of being random, it 
> operationally selects depending on how you subsequently evaluate the value.

I think the point is that randomIO is non-deterministic (technically,
pseudo-random) but causal --- the result is completely determined by
events that precede its completion.  unsafeInterleaveIO, by contrast, is
arguably (sometimes) deterministic --- but is, regardless, definitely
not causal.

jcc