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
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. 
2 Likes
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
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
Yeah, if I were doing this I would just use the CPS interface.
1 Like
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
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
scoped is somewhat like a ResourceT region, except it doesn’t let you use effects created in outer regions, I think.
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
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
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 aFoo 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
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.
Any time you “eliminate” a tag with intention, you should actually be cancelling that elimination with an introduction.
so what we need to change is to actually make hputStrLn return an SCod, that way it stays tagged, however in that case we cannot use it in an inner scope.
yea, the actual type of scoped is:
scoped :: Monad m => (forall s. SCod s m r) -> SCod s' m r
scoped act = lift (runSCod act)
Very nice, and the same objection applies to my “Bluefin with fewer tags” idea. You could just do
withFile (pure . hPutStrLn)
to violate encapsulation. Oh well. In a way it’s encouraging that Bluefin is no more complicated than necessary.
I think strictly “no eliminators with effects”, right?
1 Like
Hmm. I want to say “yes”, but care needs to be taken. Though an effectless function can’t act upon anything, it may still observe something about your scoped quantities that threatens your invariants if the observation isn’t also scoped.
Suppose, for example, you had:
newtype ID s = ID Integer
deriving (Eq, Ord)
identify :: Handle s a -> ID s
You or your users could rely on uniqueness of IDs, giving Handle Eq, Ord, TestCoercion, etc.
Depending on implementation, however, IDs might only be unique on a per-scope basis. In which case removing the s tag from ID would be very dangerous, purity of identify notwithstanding.
1 Like
This method seems similar to, or even equivalent to, Monadic Regions by Oleg Kiselyov and Chung-chieh Shan. I believe it was a general method for emulating a region (lifetime) type system in Haskell.
1 Like
I’m not very familiar with this monadic regions approach, but it’s indeed strange that, although monadic regions were discovered quite early, they haven’t received much attention.
Additionally, I believe that using Effectful’s Provider could similarly prevent resource leaks, but Bluefin’s method might be more convenient since it allows handles to be passed around as values.
2 Likes