Bluefin prevents handles leaking

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