TLDR;
I’ve published a release candidate for a linearly-typed reference-counting library today. I would very much appreciate it if anyone interested could comment on the design/API and possibly reason about the soundness bugs that I believe are lurking. You’re welcome to try it and see what you can do with it, but I would not yet recommend it for any sort of production use just yet .
Hey all, a few months back I wrote a library for reference-counting using linear types.
This library came about when I was working a lot on my game engine, not too long after I decided to rewrite the whole thing using linear types and got stuck on needing to access linear Vulkan resources in more than one place, or store and share them in certain structures.
It was originally inspired by the simple type system with reference counted described in the beginning of “Advanced Topics in Types and Programming Languages” (aka TAPL2) which I was reading at the time, however, it has since diverged considerably (yet, the principle idea remains similar).
Now, I’m not 100% confident of the soundness of the library. I would really appreciate some interested eyes to consider the API and consider whether a resource can be unsafely duplicated using the library…!
That said, I must add that, anecdotally, it has been working flawlessly in the heart of the engine.
(I wrote a bit more about the engine’s relationship with this library in the README’s first paragraphs, if you’re interested.)
I’ve decided to push the release candidate for external consideration given that it has been working well with the engine, because I have been looking at it recently again, and because some of you may find it interesting or useful (or find the unsoundness-seeking-challenge fun ).
I was briefly confused, because I thought you wouldn’t need linear types at all if you use (automatic) reference counting. After reading the documentation it became clear that you’re using linear types to make sure manual reference counting is done properly. It looks quite impressive!
Though I still wonder how difficult it would be to write a GHC plugin to do automatic reference counting.
Exactly! In fact, before linearity, the Core of the engine used ad-hoc reference counting to know when to free things, but it had become incredibly unwieldy since I had to remember to increment references when things were implicitly aliased (which required very thinking very hard about anything to do with resources) and decrement them when they were no longer needed at a given place. Mind you, this was not just disturbing in theory; I chased down many awful bugs caused by bad resource management and forgetting to increment resources that were shared).
As for automatic reference counting using some GHC plugin, hmm… you would need to be able to say a certain thing is managed with reference counts, provide a finalizer, and then more critically be able to discern with the plugin when something is being aliased and when an alias is dropped (and that sounds much harder).
I think manual reference counting using linear types does make for a good compromise where only certain user-space resources must be freed linearly yet aliased across the program.
That said, without linear types, I wouldn’t want to do manual reference counting for a complex application again – it is way too error prone unless you have figure out some structure that enforces increments and decrements are done at the right place (although at some point down the line I feel you’ll need explicit share and forget, so it is just about how deep you hide it vs the flexibility you have while hiding it completely).
Huh, haven’t thought about this approach to application design. If I’m reading the package correctly, the idea is that instead of explicitly managing dependencies in code you’re offloading it to runtime counters, then the last element that throws the resource out deletes it. I don’t feel like the management shift itself is explicitly required, but I’ll keep this in mind as a possibility when I get to my next prototyping iteration.
I did however find myself looking for a basic RAII solution in Haskell (ensure that a resource gets recycled no more than once if an exception occurs during a batch update), and this is quite similar spiritually, so I wonder what the overlap is.
Also now that I’m thinking about the code more, how does this work with dictionaries? Is it simply impossible to use them that way because every aliased item is considered linear (and is thus “recreated” anew every time it’s used)?
Hopefully I’ll see you at Zurihac @romes, reminder to add an instance for GHC.Generics.Generically when there is a generic implementation, like Aliasable.
If I’m reading the package correctly, the idea is that instead of explicitly managing dependencies in code you’re offloading it to runtime counters, then the last element that throws the resource out deletes it.
I’ll keep this in mind as a possibility when I get to my next prototyping iteration.
Be careful when deciding to use linearity everywhere, as it is quite a heavy hammer in common applications. Though if you do need to track resources carefully, and also have multiple aliases to the same resource, then this may be a good way to do it
I did however find myself looking for a basic RAII solution in Haskell (ensure that a resource gets recycled no more than once if an exception occurs during a batch update), and this is quite similar spiritually, so I wonder what the overlap is.
My intuition is that there is some overlap too, but I’d have to see side by side an expected RAII solution and this to compare usefully. If I’m not mistaken, RAII lifetimes are typically associated with scopes or automatic memory management (e.g., reference counting!) – and those lifetimes are all implicit kind of. Here there is much more explicitness (kind of required by linearity), as you decide all points of sharing and forgetting.
Also now that I’m thinking about the code more, how does this work with dictionaries? Is it simply impossible to use them that way because every aliased item is considered linear (and is thus “recreated” anew every time it’s used)?
When performing IO, are you using the linear IO from linear-prelude? Do you find it easy to use and to interface with regular IO? How do you deal with exceptions?
Speaking of exceptions, I see that newAlias receives an already-created resource before “entering the linear world”. What if that resource needs to be allocated beforehand with something like bracket? How would that interact with linearity and reference counting?
@danidiaz Yes, I’ve been using plain linear IO from linear-base.
Interfacing with regular IO has not been a problem because I haven’t looked at the “edges” of linearity recently. In essence, where I do have to interface with regular IO (the “edge”) I think I simply use a lot of Unsafe, however, everywhere else I’m using functions that wrap the regular IO with a linearly typed API.
In my particular case, I have two main libraries at the moment: ghengin-core and ghengin-vulkan.
ghengin-core is essentially UNSAFE FREE :), and uses the linearly-typed rendering API exposed by ghengin-vulkan.
ghengin-vulkan has Unsafe.toLinear calls in basically every function, to provide a linear api while interacting with regular IO under the hood.
So the answer in short is: I’ve gotten used to needing unsafe linearity at the borders to interact with existing libraries, however, the core of the program lives unsafe-free and regular-io-interaction-free since it talks to that linearly-typed API on top of regular IO for the program domain.
I’ve got a good example even:
See createVulkanDevice and destroyVulkanDevice in Ghengin.Vulkan.Renderer.Device, note the implementations instantly call Unsafe.toLinear.
See runRenderer in Ghengin.Vulkan.Renderer, note how it calls a lot of functions (including createVulkanDevice) that do all kinds of regular IO under the hood, but which are all linearly typed as exposed by the modules they are in. Despite this being a module still within ghengin-vulkan, because it is much farther from the regular IO edge than other modules in the same package, there is barely any unsafety in it. I think the only occurrence is caused by programmer laziness at the time.
(I think runRenderer above is quite a neat function showing how linear types can be pretty smooth when everything else cooperates, i.e. all functions you depend on are already linearly typed)
On exceptions
To be very truthful, I have not thought about exceptions with linear types in practice (ie in my engine) much (given its hobbyiest nature). In turn, I haven’t considered them in reference-counting either.
I haven’t tried RIO yet either, since it seemed to be lacking in terms of interfacing with the rest of linear-base, but I also haven’t fully looked into it.
I think I need some motivating goal to think more carefully about exceptions in the package – like the engine eventually growing the need to care about exceptions, or if someone out there were really interested in using this for something more serious but needed assurance wrt exceptions.
I’m not yet even sure the library is sound modulo exceptions at all . I would be more motivated to pursue polishing the package wrt to exceptions etc after fixing the more prominent issues first, and having something usable out there without risk violating linearity through it first.
Thanks for pinging me (as a general rule, I don’t read the Discourse very assiduously, but I’ll see if I’m pinged).
It’s a nice library. I’m curious how you use it. All your Aliasable types appear to be garbage-collected types, and you don’t seem to be taking particular measures to keep them off the GC. So I imagine that you have more interesting cases in mind (these Vulkan resources that you mention in your post). Do you have a tiny example of how you intend the library to be used?
Some thoughts:
In the Shareable m (Alias μ a) instances, the fact that there’s an m and a μ is suspicious
There doesn’t seem to be an instance of Aliasable (Alias m a), am I missing something? This looks important.
On the other hand, I’m not entirely sure why Aliasable is needed to begin with. You seem to be increasing the count to each of the inner fields when you increment a counter. But I don’t think you need to do that, do you?
The moral Haskell equivalent of RAII is bracket, often provided as a with-style wrapper. It’s not technically RAII in the strict C++ sense, because Haskell doesn’t have stack-allocated variables with a deterministic scope-bound lifecycle that we could (ab)use to tie to the lifecycle of the resources they represent, but morally, they serve the same purpose. We just have to use an explicit wrapper function (bracket) to mark the “scope” ourselves.
Basic pattern with raw bracket:
bracket
-- Acquire the managed resource; this happens before the "body"
(acquireResource resourceConfig)
-- Release the managed resource; this will happen either after successful
-- completion of the body, or when the body is aborted with an exception.
-- The release action takes the resource returned from `acquireResource`
-- as an argument.
releaseResource
-- The body itself, receiving the acquired resource as an argument.
$ \resource -> do { things with resource }
The equivalent C++ RAII code would look something like this:
{
// Acquire the managed resource; the constructor of the `Resource` class
// handles the actual allocation, and the destructor deallocates it
Resource resource(resourceConfig);
// Body goes here. If at any point an exception is thrown, `resource`
// goes out of scope, and its destructor runs. Otherwise, we reach the
// end of the `{}` block, and the same thing happens.
doThingsWith(resource);
} // Brackets matter: this is where `resource` goes out of scope.
A with-style wrapped, then, might look something like this in action:
posts <- withDatabaseConnection dbConfiguration $ \conn -> do
query "SELECT title, date_posted, author_name FROM posts ORDER BY date_posted DESC LIMIT 100"
renderPosts posts
Here, our resource-type-specific with wrapper (withDatabaseConnection, in this case) hides the allocation and deallocation functions (much like the constructor and destructor in the C++ case), and instead only takes the parameters (if any) to pass to the allocation function (much like in the C++ case, the constructor is called with the parameters we pass when initializing the RAII’d variable).
Anyway; the overlap with reference counting is that brackets cover a subset of the use cases for reference counting. The big limitation of a bracket is that everything that uses the resource must happen within the bracket’s body; we cannot “suspend the bracket”, we cannot separate acquisition from release, and we cannot move ownership around like we can with garbage-collected references (like regular Haskell values). This same problem also exists in C++ RAII - if we want to separate allocation from deallocation, such that they no longer happen within the same scope, we cannot use RAII, instead we need to resort to other tools, such as “smart pointers” (some of which effectively implement reference counting, while others only allow a single owner at any time, and they are designed to transfer ownership in some way or other).
One solution for this is in Haskell to just hook into the GC. We can do this using foreign pointers and finalizers: a finalizer is just a regular IO action that will run just before the GC releases the value, and because the GC is (hopefully) sound, this will happen some time after the last reference has been dropped. For most practical uses, this is fine - unless we explicitly force the finalizer, it will not run while there are active references to the value, but it will (probably) run eventually. The problem with that is that GC isn’t guaranteed to pick up any garbage within any particular time frame; depending on the GC configuration and the allocation characteristics of our program, it might not happen until the program shuts down. This is bad in cases where the resource we want to manage is scarce and needs to be released ASAP when we’re done with, or when deallocation needs to be deterministic.
That’s where reference counting comes in.
Each resource is tagged with a reference count, and that reference count travels with the reference - when we share it, the recipient must acquire it (incrementing the shared refcount), and when we’re done with it, we must release it (decrementing the shared refcount, and deallocating the resource if the refcount reaches zero).
This is very similar to a bracket, but now we can separate the acquire from the release, concurrent use of the shared resource is safe as long as all users do their acquisitions and releases correctly, and the resource will be deallocated the moment the last reference is released. For example, we can now do something like this:
workerThread :: CRef Connection -> IO ()
workerThread connRef = do
-- 'withCRef' uses a bracket to make sure that our local usage of the
-- reference is always scoped properly, even in the case of an exception.
withCRef connRef
doSomeBackgroundWork
frontendThread :: CRef Connection -> IO ()
frontendThread connRef = do
withCRef connRef $ \_ ->
runHttpServer (myApp connRef)
main = do
connRef <- newCRef (connectDatabaseShared dbConfig) disconnectDatabase
workerThread <- runWorker connRef
frontendThread <- runFrontend connRef
releaseCRef connRef
waitAll [ workerThread, frontendThread ]
The crux is in that “as long as all user do their acquisitions and releases correctly” though, because we cannot always use a bracket to pair up our acquisitions and releases automatically and in an exception-safe way, so we have to be diligent about this ourselves. This isn’t trivial, and messing up will lead to leaking (potentially scarce) resources, or premature deallocation.
For example, if we fail to acquire the connection reference in the frontend thread in the above example, everything will work fine, except if the worker thread finishes before the frontend thread does - once that happens, the refcount can reach zero, the connection gets closed, but the frontend thread still holds a reference, and it will try to use the database through it. Likewise, if we forget the release in main, the database connection will not be closed at all, because we still have one reference (from main itself) left. It gets even worse when we mix these two mistakes, with some users using without acquiring, and others using without releasing - depending on how the order of operations pans out in practice, this might just work seemingly fine by sheer coincidence, but then fail on someone else’s computer, or on the next run, or in CI, or on the production system, or in certain usage scenarios, or…
And IIUC, this is what this library addresses: it uses linear types to statically ensure that acquisitions and releases of refcounted variables are always paired up.
Oh, and another issue with reference counting is that it doesn’t natively handle cycles. If you have two reference-counted variables that reference each other, then each will prevent the other’s counter from reaching zero, so they will never be deallocated. Languages that use refcounting as their GC mechanism need an answer to this. Python has a cycle detector to automatically detect and break such cycles; other languages put the burden on the programmer, giving them a “weak reference” mechanism that they can use to manually insert cycle breakers.
Fortunately, this is not something we have to worry about in Haskell a lot, because the kind of things that we would want to use refcounting for are relatively few, and they don’t normally form cycles.
An unfortunate property of the normal style of bracket is that there’s nothing to stop the resource leaking from its scope, for example
import Control.Exception
import System.IO (openFile, hClose, hPutStr, Handle, IOMode (WriteMode))
withFile :: (Handle -> IO a) -> IO a
withFile k =
bracket
(openFile "/tmp/myFile" WriteMode)
hClose
k
example :: IO ()
example = do
h <- withFile pure
hPutStr h "Hello"
-- ghci> example
-- *** Exception: /tmp/myFile: hPutStr: illegal operation (handle is closed)
Effect systems can fix that! For example, here’s a solution in Bluefin.
Imports and basic definitions
{-# LANGUAGE GHC2021 #-}
import Bluefin
import Bluefin.Compound (useImplIn)
import Bluefin.Eff (bracket, Eff, (:>), (:&))
import Bluefin.IO (effIO, IOE)
import System.IO
(openFile, hClose, hPutStr, Handle, IOMode (WriteMode))
newtype SafeHandle e = MkSafeHandle (Handle)
withFileSafe ::
e1 :> es =>
IOE e1 ->
(forall e. SafeHandle e -> Eff (e :& es) r) ->
Eff es r
withFileSafe ioe k =
bracket
(effIO ioe (openFile "/tmp/myFile" WriteMode))
(effIO ioe . hClose)
(useImplIn (k . MkSafeHandle))
hPutStrSafe ::
(e1 :> es, e2 :> es) =>
IOE e1 ->
SafeHandle e2 ->
String ->
Eff es ()
hPutStrSafe ioe (MkSafeHandle h) = effIO ioe . hPutStr h
-- Doesn't compile:
--
-- • Couldn't match type ‘e20’ with ‘e1’
-- Expected: SafeHandle e1 -> Eff (e1 :& es) (SafeHandle e20)
-- Actual: SafeHandle e1 -> Eff (e1 :& es) (SafeHandle e1)
-- • because type variable ‘e1’ would escape its scope
example :: e :> es => IOE e -> Eff es ()
example ioe = do
h <- withFileSafe ioe pure
hPutStrSafe ioe h "Hello"
-- Works fine
example2 :: e :> es => IOE e -> Eff es ()
example2 ioe =
withFileSafe ioe (\h -> hPutStrSafe ioe h "Hello")
Thanks for commenting @aspiwack. I gave this some thought and realised that Aliasable is actually unnecessary. Historically, it came about in order to derive generic instances for Shareable, but really it was a round about way of doing so, and overbearing.
Just today, I deleted all traces of Aliasable. Now, Shareable can be derived generically, and that’s all that was needed in the end.
I’ll have to get back to you on the examples, but if you happen to be by ZuriHac maybe I can show you in person.
On your remaining thoughts:
Shareable m a means we can share as in m. The mu in Alias mu a is the monad in which the resource can be freed. That is, we can share it in any MonadIO m, but only free it in mu.
Turns out you were right, after I gave it some more thought. There is no point to Aliasable, it was just used to allow generic instances of Shareable but in a contrived way. Removed!
Is the MonadIO constraint on the various functions really necessary by the way? You’re using Counter in a way which I think can be considered pure from the outside. So I think you could get away with using unsafePerformIO here.
.
and got stuck on needing to access linear Vulkan resources in more than one place, or store and share them in certain structures.