Disowning an STRef

#21

Bodigrim’s text-builder-linear: Builder for Text and ByteString based on linear types may be of inspiration.

But I am afraid I cannot find a API that provides what OP wants. My intuition is that, the moment you take the value out of the scope of a lineary-typed function, the value is no longer guaranteed to be “unique” and hence all hell can break loose. From text-builder-linear I derive that intuition.

There might be other way to achieve the same result OP wants, but I am not sure you could do that without lifting everything in a linearly-typed function. You may argue at that point it loses the point of doing so. I am not sure, maybe linear function may still offer more.

Anyone knows more about type theory and uniqueness type may want to chime in instead.

2 Likes
#22

This is a standard problem with Haskell’s linear types. The solution is to use a CPS variant, for example

runSTLinear :: (forall s. ST s (STRef s a)) -> (STRef s a %1 -> r) -> r
2 Likes
#23

From a recent discussion with @aspiwack, I think there ought to be some Ur's in that type signature:

runSTLinear :: (forall s. ST s (STRef s a)) ->
               (STRef s a %1 -> Ur r) ->
               Ur r

to prevent:

rampantSTRef :: STRef s' a
rampantSTRef = runSTLinear (...) id

But considering that the OP was about:

  -- ...yes: I gave it the proper name
unsafeDisownSTRef :: STRef s a -> ST s (STRef s' a)

for which the CPS variant would seem to be:

unsafeWithDisownedSTRef :: STRef s a ->
                           (STRef s' a -> ST s a) ->
                           ST s a

then the appropriate “lineated” variant would then be:

withDisownedSTRef :: STRef s a ->
                     (STRef s' a %1 -> ST s (Ur a)) ->
                     ST s (Ur a)

…to thwart the (mis)use of id.

However any (properly) "lineated" variant would appear to exclude the second example in the OP:

toplevelGraph :: GraphNode Pure
toplevelGraph = runST $ constructGraph >>= disown

along with defining top-level IORefs, thereby defeating the purpose of disowning encapsulated state to begin with. But…I am definitely not an expert on this, and all of the above could be wrong: @aspiwack can tell us just how wrong I am :-D

2 Likes
#24

I think the problems identified here can be overcome, using linear types. (Some have suggested this above; this post was written but not sent before those comments appeared. Great minds think alike!)

I see three problems identified above:

  • dangerous polymorphism
  • copying of references via inlining
  • the possibility of mutation in structures believed pure

Disclaimer: I’m not actually proposing to change runST. Just having some fun imagining new possibilities.

Imagine we had

runST :: (forall s. StateToken s %1-> ST s (StateToken s, Ur a)) -> a

where

data Ur a where
  MkUr :: a -> Ur a   -- "unrestricted"
data StateToken s -- abstract

The idea is that StateToken s is guaranteed not to escape the runST, because it’s required in the result and yet is in scope linearly. Now let’s revisit disownSTRef:

disownSTRef :: STRef s a -> StateToken s' %1-> ST s (Ur (STRef s' a), StateToken s')

I think this would stop us from making the dangerously polymorphic newSTRefPure, because the returned ref would have to be fixed to the token type of an enclosing runST.

So we have solved our first problem. Our second problem’s key example is this:

Ur globalRef = runST $ \t -> do
  ref <- newSTRef Nothing
  (ur_disowned, _) <- disownSTRef ref realWorldToken
  return (t, ur_disowned)

If this gets inlined, we’re in trouble. So we must add a rule to the optimizer never to duplicate a realWorldToken. Put another way, there is an arbitrary but fixed number of realWorldTokens available, and the optimizer is not empowered to mint more. GHC already has to analyze an expression in the process of deciding whether to inline it, and this just adds a new check to that algorithm.

So that’s the second problem solved. For the third, I realized that my STRefish is problematic. I know that a type cannot depend on a specific choice of the state type variable s because of parametricity. But a type might indeed depend on the distinction between Ref and Pure, meaning my very generic disown is dangerous. So it needs a few tweaks:

data Pure   -- no constructors

type family STRefish s a where
  STRefish Pure a = a
  -- no other equations

My disown above also forgot to worry about the possibility that a reference would be used after it is disowned. If we don’t want to gate every use of an STRef behind a StateToken, we’ll just have to disown as we leave the ST monad. So we make runST yet more glorious:

runST ::
  (forall s.
    (forall a. STRefish s a ~ STRef s a) =>
    StateToken s %1->
    ST s (StateToken s, Ur (a s)) ->
  a Pure

(Of course, if you want to return something not indexed by a state token, you can use the Const functor.)

It would be nice if there were a way of convincing GHC that the abstract s is not Pure, in which case we would just add another equation to STRefish and then could avoid the quantified constraint in the new runST type. I don’t think this is possible, but I imagine the quantified constraint would work – even if it’s pretty unwieldy.

Incidentally, my recent Linearly qualified types paper would make the syntax here much more palatable.

I offer no proof that any of these ideas are correct, but I do think I’ve closed some loopholes here. Looking forward to you all finding more of them. :slight_smile:

4 Likes
#25

“Linearly Qualified Types” would be such a great addition! My observation has been that, otherwise the linear-code I have is dotted with the “bureaucracy” of dups and consumes!

Semi-related fwiw: I just watched https://www.youtube.com/watch?v=0uA-tKR6Ah4 and learned that in Haskell we don’t have a %0 -> b support, not sure if it would anything to this conversation at all.

#26

I’m still not sure if I understand the question. but GraphNode (Ref a) allows cyclic graph (which is kind of the point using STRef, but GraphNode (Pure a) can not. So how could disown convert a impure graph to a pure one ?