Bluefin prevents handles leaking

#1

The latest article in my series about Bluefin. This one is about how Bluefin uses the type system to achieve ST-like resource safety guarantees.

13 Likes
#2

This is nice but it also means that you can’t store a handle in a data structure without also parameterizing that structure over its lifetime.
Do you have something like an uncheckedCoerceHandle :: Handle e1 -> Handle e2 for cases where it’s difficult to statically ensure lifetimes like this?

It’s not like this breaks memory safety or anything so I would rather not have to use unsafeCoerce

2 Likes
#3

Thanks! And, that’s correct.

Here I’m not so sure, because, although I hear “lifetime” used by the Rust community, I don’t know what it means. I call the parametrization “effect tagging”. I’m not sure if it’s the same as “lifetime”.

In any case, you can put two handles in a structure and parametrize a structure with a single type variable without requiring that those two handles have the same lifetime in the sense of being created and destroyed together. For example, I can do this:

data StateAndHandle e = MkStateAndHandle {
    sahState :: State Int e,
    sahHandle :: Handle e
    }

and create these two fields at separate locations (with evalState and withFile respectively). See Bluefin.Compound for more details.

mapHandle is the part of the external facing API that allows you to do things like Handle e1 -> Handle e2. In# from the internals can get you the unsafe bit. But you really shouldn’t have to do this! If you really find a case where you think it would be better to do so then please open an issue so I can understand the circumstances better.

#4

It’s really nice to see this trick to be used in an effect system, I think it’s way underused.
Maybe something that you might not immediately realize, but this also works outside of bluefin. E.g. if you have IO, you can write a newtype ScopedHandle s = UnsafeScopedHandle {getHandle :: Handle} and a function withScopedHandle :: FilePath -> (forall s. ScopedHandle s -> IO r) -> IO r and you will not be able to escape the handle out of the continuation.
Take this in contrast to the usual ways of preventing something like this, like:

  • just using a continuation: make pure the continuation, here you have your handle
  • make the continuation return IO () instead of IO r: make an IORef, write the handle to the IORef, here you have your handle
2 Likes
#5

As a bonus, here’s a Monad that doesn’t let you escape resources out of the do block, similar to how it is done with runST:

{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE BlockArguments #-}
module ScopedCont where

import System.IO qualified
import Control.Monad.Codensity
import UnliftIO (MonadIO, IOMode (WriteMode), liftIO)
import Data.Kind
import Control.Monad.Trans (MonadTrans, lift)

newtype SCod s (m :: k -> Type) a = MkSCod {unSCod :: forall b. (a -> m b) -> m b}
  deriving (Functor, Applicative, Monad) via (Codensity m)
  deriving MonadTrans via Codensity

instance MonadIO m => MonadIO (SCod s m) where 
  liftIO = lift . liftIO


runSCod :: (Applicative m) => (forall s. SCod s m r) -> m r
runSCod k = unSCod k pure

newtype Handle s = MkHandle {unsafeGetHandle :: System.IO.Handle}

withFile :: FilePath -> System.IO.IOMode -> SCod s IO (Handle s)
withFile fp md = MkSCod (\k -> System.IO.withFile fp md (k . MkHandle))

hPutStrLn :: Handle s -> String -> SCod s IO ()
hPutStrLn (MkHandle hdl) = liftIO $ System.IO.hPutStrLn hdl

x :: IO ()
x = runSCod do 
  hdl <- withFile "bla" WriteMode
  liftIO $ hPutStrLn hdl "test"

y :: IO (Handle s)
y = runSCod do 
  withFile "bla" WriteMode
1 Like
#6

I guess you mean that y doesn’t compile?

#7

yes, exactly, y doesn’t compile.

#8

This is really fascinating! I wonder why you need SCod or the s tag at all, though. Given your observation in Bluefin prevents handles leaking - #4 by MangoIV isn’t it sufficient just to use IO?

1 Like
#9

maybe you can write a function cleanup :: SCod s m a -> SCode s' m a that calls the continuation and then give you a new scope.

1 Like
#10

In this case not, notice the function signature of withFile which seems to “return” a Handle which is what we want to prevent and guard against by scoping over only the do block.

We’re basically building “nested” continuations which are finally called by runSCont and then the resources allocated in the block are freed. At least that’s the aim. :stuck_out_tongue:

2 Likes
#11

Oh I see. If you have a withFile that returns a Handle s then you do need an effect tag to make that safe. If you have a withFile that passes the (universally quantified) Handle s to a continuation, then you don’t need the tag.

Doing away with the tag is a such an ergonomic improvement that I’m inclined to make a version of Bluefin without one. That would mean that

(e1 :> es, e2 :> es) => Foo e1 -> Bar e2 -> Eff es r

Could become

Foo e1 -> Bar e2 -> Eff r

Amazing! The only downside would be that there would be no safe version of runPureEff :: (forall es. Eff es r) -> r. However, the API could still be designed so that any top-level definition

f :: Eff r

is morally pure. Amazing! This could be a gentle on-ramp to Bluefin.

4 Likes
#12

you have to be a bit careful though. In case of Scod, the “lifetime” of the handle is basically over the entirety of the block. So if you do more work, then the Handle might be allocated for way longer than needed. You somehow need to make this obvious. I think making the CPS interface the standard one is better in that regard. The programmer will want to prevent increased nesting at all cost and hence limit the “lifetime” of the resource.

1 Like
#13

Yeah, if I were doing this I would just use the CPS interface.

1 Like
#14

Somebody with a large brain needs to please tell me how cleanup :: SCod s m a -> SCod s' m a relates to delimited continuations. I can’t quite put my finger on it. It looks like this is exactly reset from Control.Monad.Codensity

1 Like
#15

I have made a full example with an example run on how this will look in terms of lifetimes:
https://bin.mangoiv.com/note?id=fd2dc39a-61ae-4e2e-acd4-665d409e8bb6
Fixed version which cannot escape handle via hputStrLn:
https://bin.mangoiv.com/note?id=b06dd7a8-b8d4-4ba4-ab92-64db0fc8e36d

1 Like
#16

scoped is somewhat like a ResourceT region, except it doesn’t let you use effects created in outer regions, I think.

#17

I am not very confident about ResourceT because I never saw its appeal but I think you can even get the “immediate release” semantics in a safe way if you make the resource in the continuation linear and then have a release function that “eats” the resource and have all other functions that operate on it return it.

I am not entirely sure if that works for do notation though. Maybe I should try out.

Something cool that another person showed me is that you can add random cleanup functions to Codensity (and hence for SCod) by asking for the continuation to complete and then executing that function, like this: registerHandler cleanup = Codensity \k -> k () `finally` cleanup

#18

Yeah, you can use linear types for that. I have a Bluefin branch where I experimented with “linear coroutines”, where when you send an a, you either get a b back (and the ability to continue), or you get notified that the other side terminated with an r (and no ability to continue). It works out OK. You can not use normal do notation, but you can use QualifiedDo with Control.Functor.Linear.

I’m not planning to introduce this to Bluefin any time soon, but when people start asking for more fine-grained control over consuming results from coroutines I probably will.

1 Like
#19

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 (hPutStrLn hdl)

Another way to look at it is that a handle is isomorphic to the interface operating on it, so partially applying the functions in that interface gives you a different representation for the handle. If this representation isn’t tagged, nothing stops its escape.

6 Likes
#20

You are right! So the IO version is actually not entirely safe! I think cleanup is fine though, since it is supposed to call the continuation and is fully intentionally eliminating the tag.