runST does not prevent resources from escaping

[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.