Disowning an STRef

#1

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.

Could this possibly work and be safe?

4 Likes
Global IORefs + Circular dep = surprising behavior?
Mutable Value Semantics Trend vs Immutability
#2

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.

#3

disownSTRef implies

pureNewSTRef = \a -> runST (disownSTRef =<< newSTRef a) :: a -> STRef s' a

which can’t possibly be right, can it? It would mean you could do

   let r = pureNewSTRef True
       m = runST (do { modifySTRef r not; readSTRef r })
    in runST (readSTRef r)

and the result would depend on whether m has been evaluated or not.

#4

From a quick search for "unsafePerformST" in Hoogle:

…have fun!

#5

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

#6

It definitely type checks. I ran it in ghci!

#7

Huh! Can you share a full file or something?

#8 
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)
1 Like
#9

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 #-}
#10

Yea, pretty much. I didn’t consider that the r binding would have an implicit forall

#11

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
5 Likes
#12

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…

#13

This reminds me I ought to read https://www.jonmsterling.com/papers/sterling-gratzer-birkedal-2022.pdf. Ideally, we no longer need to guess at what exactly the ST monad is doing, and now have the answers, right?

#14

I’m thinking “no”:

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

#15

Heh heh, is that a deliberate typo? ‘observable problem’.

#16

Just “observable”. I blame the phone keyboard.

#17

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.

#18

Could a linearly-typed transferDanglingSTRef help? Some sort of “move” semantics (between different type of monads) for STRef?

1 Like
#19

Interesting idea! Perhaps that could work.

#20

…only if there is a total ordering for all the various users of said “dangler”, otherwise nondeterminism awaits: