On 04/10/2013 04:45 AM, o...@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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
