[Haskell-cafe] Proof that Haskell is RT

[David MacIver]

On Wed, Nov 12, 2008 at 11:05 PM, Jonathan Cast
<jonathanccast at fastmail.fm> wrote:
> On Wed, 2008-11-12 at 23:02 +0000, David MacIver wrote:
>> On Wed, Nov 12, 2008 at 10:46 PM, Don Stewart <dons at galois.com> wrote:
>> > david.maciver:
>> >> On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson
>> >> <lennart at augustsson.net> wrote:
>> >> > Actually, unsafeInterleaveIO is perfectly fine from a RT point of view.
>> >>
>> >> Really? It seems easy to create things with it which when passed to
>> >> ostensibly pure functions yield different results depending on their
>> >> evaluation order:
>> >>
>> >> module Main where
>> >>
>> >> import System.IO.Unsafe
>> >> import Data.IORef
>> >>
>> >> main = do w1 <- weirdTuple
>> >>           print w1
>> >>           w2 <- weirdTuple
>> >>           print $ swap w2
>> >>
>> >> swap (x, y) = (y, x)
>> >>
>> >> weirdTuple :: IO (Int, Int)
>> >> weirdTuple = do it <- newIORef 1
>> >>                 x <- unsafeInterleaveIO $ readIORef it
>> >>                 y <- unsafeInterleaveIO $ do writeIORef it 2 >> return 1
>> >>                 return (x, y)
>> >>
>> >> david at mel:~$ ./Unsafe
>> >> (1,1)
>> >> (1,2)
>> >>
>> >> So show isn't acting in a referentially transparent way: If the second
>> >> part of the tuple were evaluated before the first part it would give a
>> >> different answer (as swapping demonstrates).
>> >
>> > Mmmm? No. Where's the pure function that's now producing different
>> > results?  I only see IO actions at play, which are operating on the
>> > state of the world.
>>
>> I suppose so. The point is that you have a pure function (show) and
>> the results of evaluating it totally depend on its evaluation order.
>
> Sure.  But only because the argument to it depends on its evaluation
> order, as well.

That's not really better. :-)

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.

Anyway, I'll shut up now.