Had an idle thought this morning: Would it be safe to have a new primitive
disownSTRef :: STRef s a -> ST s (STRef s' a)
? Note that s' is completely unconstrained. In particular, it could be RealWorld, which would mean that you could now create an IORef at toplevel without unsafePerformIO, which would be nice.
The idea is that any STRef s a must have been created within the invocation of runST that we’re now in, and so disowning the ref can’t interfere with other state in the outside world.
Even more powerfully, we can imagine something like this:
data Purity
= Ref Type
| Pure
type family STRefish s a where
STRefish (Ref s) a = STRef s a
STRefish Pure a = a
disown :: t (Ref s) -> ST s (t s')
-- primitive which I think is safe and can be a no-op at runtime
data GraphNode s = Node { payload :: Int, neighbors :: STRefish s [GraphNode s] }
toplevelGraph :: GraphNode Pure
toplevelGraph = runST $ do
graph <- constructGraph
disown graph
And now we have a completely pure data structure constructed using mutability, but emancipated from any monad.
You mean you can construct a top level value of type
pureIORed :: IORef Bool
Doesn’t that already disprove purity? If I inline that top-level value (or otherwise duplicate it’s evaluation) I get two different IORefs, which certainly is observable.
@tomjaguarpaw I don’t think that will type check, because you’re using r in two different ST s scopes (different s). You’ve got one s introduced by runST in m, and a different one in runST (readSTRef r).
import Control.Monad.ST
import Data.STRef
disownSTRef :: STRef s a -> ST s (STRef s' a)
disownSTRef = undefined
pureNewSTRef :: a -> STRef s' a
pureNewSTRef = \a -> runST (disownSTRef =<< newSTRef a)
example :: Bool
example =
let r = pureNewSTRef True
m = runST (do { modifySTRef r not; readSTRef r })
in runST (readSTRef r)
Perhaps what you’re thinking of is the following. This works:
example :: Bool
example =
let r :: forall s. STRef s Bool
r = pureNewSTRef True
m = runST (do { modifySTRef r not; readSTRef r })
in runST (readSTRef r)
This doesn’t work
example2 :: forall s. Bool
example2 =
let r :: STRef s Bool
r = pureNewSTRef True
m = runST (do { modifySTRef r not; readSTRef r })
in runST (readSTRef r)
Needed extensions:
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
Even worse, this makes it possible to implement unsafeCoerce, since there is no ST wrapper to prevent generalization of polymorphic references anymore
module Danger where
import Data.STRef
import Control.Monad.ST
import Unsafe.Coerce
disownSTRef :: STRef s a -> ST s (STRef s' a)
disownSTRef ref = pure (unsafeCoerce ref)
newSTRefPure :: a -> STRef s a
newSTRefPure x = runST $ do
ref <- newSTRef x
disownSTRef ref
unsafeCoerce' :: a -> b
unsafeCoerce' x = runST $ do
-- The type of ref is generalized since
-- Haskell lacks a value restriction.
-- Normally the ST monad would prevent generalization
let ref :: STRef s (Maybe a)
ref = newSTRefPure Nothing
writeSTRef ref (Just x)
result <- readSTRef ref
case result of
Nothing -> error "unreachable"
Just x -> x
Since we all agree that an ability to create polymorphic references in pure code is unsafe since it makes implementing unsafeCoerce possible (as @prophet showed and also is stated in the unsafePerformIO docs), I’d call the new op unsafeDisownSTRef. However then we add another unsafe operation that can be implemented in terms of other unsafe operations, not sure if this adds more value…
from a quick glance of that paper, the investigation of state and mutation occurs within the context of an appropriate monad.
what’s being contemplated here would put the state outside of the control of any monad, which is why it’s possible to define unsafeCoerce - the disowned STRef would be “free” to use in any context.
I noticed one R. Harper (of SML fame) is acknowledged in that paper - it was from the earlier work on supporting references in (S)ML that we now know the risks of polymorphic references, and why SML has its value restriction for mutable references…
So far we’ve got things which are sound but not complete (existing ST), and unsound (this, if the refutation is true). Trying to close in on that perfect “sound and complete” is where it helps to understand the semantics. e.g. Which Monad matters; the higher rank stuff stuff of runST is a very syntactic encapsulation trick — it implements a conservative approximation of what is really going on with a sledgehammer.