| 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... |
Linear constraints are technically just sugar, but without them it's too manual with bare -XLinearTypes.