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

[Timon Gehr]

On 04/10/2013 04:45 AM, oleg at okmij.org wrote:
>
> ...
>
> 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
>

I am not sure that the two statements are equivalent. Above you say that 
the context distinguishes x == y from y == x and below you say that it 
distinguishes them in one possible run.

> The function unsafeInterleaveST ought to bear the same stigma as does
> unsafePerformIO. After all, both masquerade side-effecting
> computations as pure.

Potentially side-effecting computations. There are non-side-effecting 
uses of unsafePerformIO and unsafeInterleaveST, but verifying this is 
outside the reach of the type checker. If they have observable 
side-effects, I'd say the type system has been broken and it does not 
make sense to have a defined language semantics for those cases.

> 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.)
>

In essence, lazy IO provides unsafe constructs that are not named 
accordingly. (But IO is problematic in any case, partly because it 
depends on an ideal program being run on a real machine which is based 
on a less general model of computation.)

> 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
>


I think this context cannot be used to reliably distinguish x == y and y 
== x. Rather, the outcomes would be arbitrary/implementation 
defined/undefined in both cases.