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

Timon Gehr timon.gehr at gmx.ch
Thu Apr 11 21:17:21 CEST 2013

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.

More information about the Haskell-Cafe mailing list