[Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of "referential transparency"]

[oleg at okmij.org]

One may read this message as proving True === False without resorting
to IO. In other words, referential transparency, or the substitution
of equals for equals, may fail even in expressions of type Bool.

This message is intended as an indirect stab at lazy IO. 
Unfortunately, Lazy IO and even the raw unsafeInterleaveIO, on which
it is based, are sometimes recommended, without warnings that usually
accompany unsafePerformIO.
http://www.haskell.org/pipermail/haskell-cafe/2013-March/107027.html

UnsafePerformIO is known to be unsafe, breaking equational reasoning;
unsafeInterleaveIO gets a free pass because any computation with it
has to be embedded in the IO context in order to be evaluated -- and
we can expect anything from IO. But unsafeInterleaveIO has essentially
the same code as unsafeInterleaveST: compare unsafeInterleaveST from
GHC/ST.lhs with unsafeDupableInterleaveIO from GHC/IO.hs keeping in
mind that IO and ST have the same representation, as described in
GHC/IO.hs. And unsafeInterleaveST is really unsafe -- not just mildly
or somewhat or vaguely unsafe. In breaks equational reasoning, in pure
contexts.

Here is the evidence. I hope most people believe that the equality on
Booleans is symmetric. I mean the function

        (==) :: Bool -> Bool -> Bool
        True  == True  = True
        False == False = True
        _     == _     = False

or its Prelude implementation.
The equality x == y to y == x holds even if either x or y (or both)
are undefined. 

And yet there exists a context that distinguishes x == y from y ==x. 
That is, there exists 
        bad_ctx :: ((Bool,Bool) -> Bool) -> Bool
such that

        *R> bad_ctx $ \(x,y) -> x == y
        True
        *R> bad_ctx $ \(x,y) -> y == x
        False

The function unsafeInterleaveST ought to bear the same stigma as does
unsafePerformIO. After all, both masquerade side-effecting
computations as pure. Hopefully even lazy IO will get
recommended less, and with more caveats. (Lazy IO may be
superficially convenient -- so are the absence of typing discipline and
the presence of unrestricted mutation, as many people in 
Python/Ruby/Scheme etc worlds would like to argue.)

The complete code:

module R where

import Control.Monad.ST.Lazy (runST)
import Control.Monad.ST.Lazy.Unsafe (unsafeInterleaveST)
import Data.STRef.Lazy

bad_ctx :: ((Bool,Bool) -> Bool) -> Bool
bad_ctx body = body $ runST (do
   r <- newSTRef False
   x <- unsafeInterleaveST (writeSTRef r True >> return True)
   y <- readSTRef r
   return (x,y))


t1 = bad_ctx $ \(x,y) -> x == y
t2 = bad_ctx $ \(x,y) -> y == x