[Haskell-cafe] Proof that Haskell is RT

[David MacIver]

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.
But you're still in the IO monad at this point so I suppose it
technically "doesn't count" because it's only observable as the result
of IO.

It's pretty suspect behaviour, but not actually a failure of
referential transparency.