[Haskell-cafe] Proof that Haskell is RT

[Lennart Augustsson]

But how can you tell something being causal or not?
Assuming that all IO operations return random result, of course. :)

>From a practical point of view unsafeInterleaveIO can give suspect results.
But theoretically you can't fault it until you have given a semantics
for the IO monad operations so you have something to compare it
against.

  -- Lennart

On Thu, Nov 13, 2008 at 12:05 AM, Jonathan Cast
<jonathanccast at fastmail.fm> wrote:
> 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
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>