On 04/10/2013 04:45 AM, oleg@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.