Reference Counting with Linear Types

Good to see some more uses of linear types! Very few languages can use linear types, and their potential is huge IMO.

OP shows the benefits of a linear RC that tracks references dynamically, and one can even imagine a version where the compiler tracks the references instead.

For example (for those who are more familiar with Rust) imagine that it had linear types and that we used them for matthieum's static-RC [0] (like suggested by frank-king at [1] to prevent leaks) and you'd have a pretty good idea of linear static RC.

I also talked about a possible alternative linear static RC at [2] and [3] (I didn't explain it well at all, happy to elaborate), though lately I suspect that one would need to add a GhostToken-ish [4] substance to allow safely reading/writing the shared value, or perhaps a RefCell.

I suspect that something like GhostToken could also solve OP's restriction that types be opaque, if Haskell has something like GhostToken... I could be wrong on that though.

[0] https://github.com/matthieu-m/static-rc

[1] https://github.com/matthieu-m/static-rc/issues/7

[2] "Linear reference counting" in https://verdagon.dev/grimoire/grimoire#the-list

[3] https://www.reddit.com/r/rust/comments/1d06gjo/comment/l61qm...

[4] https://www.reddit.com/r/rust/comments/p5f78s/ghostcell_sepa...

What does this do regarding reference cycles?

* Do strong reference cycles break soundness?

* Are weak references supported yet? Using the slim, fat, indirect, or reverse model?

Does someone know general ressources on this type of algorithm for concurrent environments? I've had to implement it recently and it was quite hard to find anything.