runST does not prevent resources from escaping

[prophet]

runST does not prevent resources from escaping

[tomjaguarpaw]

Summary: runST does not prevent resources from escaping, but it does prevent escaped resources from being used.

[simon]

Thanks for sharing this. It is important to keep in mind that (forall s. resource s -> x) -> x is not sufficient to prevent resource leakage.

[Kleidukos]

Thanks for the explanation!
I’m trying to reproduce locally your “Bonus: We don’t even need existentials” section but GHC (9.12.2) tells me [GHC-07525]: A newtype constructor must not have existential type variables. Do you have reproducible code you could share?

[Leary]

Tmp.hs:29:5-64: error: [GHC-07525]
    • A newtype constructor must not have existential type variables
      MkNotSoSafePtr :: forall a {k}.
                        (forall r. (forall (s :: k). SafePtr s a -> r) -> r)
                        -> NotSoSafePtr a
    • In the definition of data constructor ‘MkNotSoSafePtr’
      In the newtype declaration for ‘NotSoSafePtr’
   |
29 |   = MkNotSoSafePtr (forall r. (forall s. SafePtr s a -> r) -> r)
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

The existential type variable here is k; you can fix the issue by bringing it into scope yourself or killing the polykindedness of SafePtr that introduces it in the first place.

[Kleidukos]

I’m not well-versed in polykindness or kind variables, how would I do what you suggested?

[Leary]

newtype SafePtr (s :: Type) a = MkSafePtr (Ptr a)

or

newtype NotSoSafePtr a
  = MkNotSoSafePtr (forall r. (forall (s :: Type). SafePtr s a -> r) -> r)

or

newtype NotSoSafePtr a
  = MkNotSoSafePtr (forall r. (forall k (s :: k). SafePtr s a -> r) -> r)

or

newtype NotSoSafePtr k a
  = MkNotSoSafePtr (forall r. (forall (s :: k). SafePtr s a -> r) -> r)

[jackdk]

Does this problem go away if you index the monad with s as well? runST :: (forall s . ST s a) -> a uses an s parameter on the ST monad, and while you can sneak a reference out by using an existential wrapper, you can’t do anything evil with it because the s on the STRef will differ from the one in a future runST call.

Similarly, would this avoid the use-after-free in your “safe” pointer functions?

newtype IOS s a = IOS (IO a)
  deriving stock (Functor)
  deriving newtype (Applicative, Monad, MonadIO, ...)

pokeSafe :: Storable a => SafePtr s a -> a -> IOS s ()
pokeSafe (MkSafePtr pointer) x = IOS $ poke pointer x

allocaSafe :: Storable a => (forall s. SafePtr s a -> IOS s b) -> IO b
allocaSafe f = do
  pointer <- malloc
  -- This is the change
  IOS act <- f (MkSafePtr pointer)
  result <- act
  -- End change
  free pointer
  pure result

Also, the malloc and free calls might want to be bracket-ed.

[Leary]

Only if you remember to type role IOS nominal representational, hide the constructor, and resist the urge to give it MonadUnliftIO!

[tomjaguarpaw]

@jackdk

Does this problem go away if you index the monad with s as well?

Yes, congratulations, you have just invented Bluefin! (well, modulo :&, which is needed for having resources with different lifetimes).

@Leary’s caveats are essential, and @Leary first pointed out to me here the necessity of keeping the type index on the monad too:

Bluefin prevents handles leaking

To truly prevent handles from leaking, the type level tag must have no eliminators. In ST, this is the case because ST itself shares the tag. Similarly, in bluefin, the handle’s tag must relate to the tag of Eff with :>. These all eliminate tags: hPutStrLn :: Handle s -> String -> IO () cleanup :: SCod s m a -> SCode s' m a Foo e1 -> Bar e2 -> Eff r The simplest way to see the issue is to consider: z :: IO (String -> IO ()) z = runSCod do hdl <- withFile "bla" WriteMode pure (hPutStrL…

• type role IOS nominal representational: the need for this is unfortunate. Type roles default to the least safe possibility!
• MonadUnliftIO: even weaker functions can break the scoping too: MonadUnliftIO instance allows escape · Issue #29 · tomjaguarpaw/bluefin · GitHub. I don’t have anything optimistic to say about this except that if you use them you to have to be careful.

[prophet]

Oh, I did exactly what Leary mentioned in my testing but forgot to mention it in the post. Thanks for the correction! I’ll update it.
(That said, this is quite an unfortunate error message even for GHC standards. It’s very subtle that there are any existentials involved at all and it’s really all a result of PolyKinds generalization being a bit overzealous. This would have compiled fine in Haskell2010 + RankNTypes)

[prophet]

It does, but (just like with ST in the post), the monad with the s parameter is not just an additional detail here, it is the actual mechanism that makes this safe!
If you had a SafePtr ConcreteS1 a, then you also couldn’t use it in an IOS ConcreteS2 monad (without involving any RankNTypes at all).
All the higher rank continuation does is invent a fresh type constant that is different for every invocation of allocaSafe.

[chrisdone]

There’s a related comment on Oleg’s regions page:

https://okmij.org/ftp/Haskell/regions.html

Monadic Regions can manage resources other than memory, as explained by Brandon Moore: ``I’m assuming you understand how the type on runST and the STRef operations ensure that, even though you can smuggle out an STRef in the result from runST, you will never be able to use it again

I’ve been reading this area as a way to learn Liquid Haskell, by expressing resource tracking in refinement types. So I coincidentally was coming back to the literature on it.

[tomjaguarpaw]

Thanks for linking that. At some point I want to go over the history to see how these things evolved, and why they stopped evolving, because 30 years ago Haskell researchers were very close to inventing Bluefin, and I’m not sure why they didn’t. For example, take Lightweight Monadic Regions. It discusses the operation

importSHandle :: SHandle (SIO r) -> SHandle (SIO (r,s))

This is basically (a version specialized to SHandle of) what Bluefin calls

mapHandle :: Handle h => h e -> h (e :& es)

(Bluefin’s version of “pairing regions” (,) is called :&.)

Bluefin uses an incoherent instance in a way that is essential for ergonomics (see Plucking constraints in Bluefin). Maybe incoherent instances didn’t exist then, so the thread of work was dropped? The Haskell landscape would have looked very different if we had had a Bluefin equivalent 30 years ago!

[sclv]

Yep! I was going to refer to the “lightweight monadic regions” paper linked there which I think handles all this stuff just dandy: https://homes.luddy.indiana.edu/ccshan/capability/region-io.pdf

The problem in this post is the poke function just cares that there is “an” s but not which one. Forcing the usage to check that the s corresponds to the region you are in can be done by changing the type of such functions to ensure they match the s of your monadic region.

[Kleidukos]

@tomjaguarpaw

The Haskell landscape would have looked very different if we had had a Bluefin equivalent 30 years ago!

Considering the amount of people thanked in the Bluefin README, that’s a lot to ask from a lot of time-travellers.

[turion]

I might be completely missing the point here and misunderstanding the implications, but I find the title and the claim misleading.

First, runST as in the base function, was not shown to have a problem here, right? The claim here is that an adaptation of the technique doesn’t work as expected.

Second, isn’t the real fault the type signature pokeSafe :: Storable a => SafePtr s a -> a -> IO ()? (And peekSafe for that matter?) After all, the point of the s variable is to prevent operations on the pointer outside its scope, but this restriction is completely sidestepped here. I believe you’d really need something like:

newtype SafePtrM s a = SafePtrM (IO a)

pokeSafe :: Storable a => SafePtr s a -> a -> SafePtrM s ()
pokeSafe (MkSafePtr pointer) x = SafePtrM $ poke pointer x

runSafePtrM :: (forall s . SafePtrM s a) -> IO a

[turion]

Oh, this is the same idea as the IOS construction earlier. Apologies for the noise.