[verdagon]

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...

[whateveracct]

It's a ways out, but an extension to -XLinearTypes, "linear constraints", has been shown to be able to be used to implement Rust-like ownership. See Section 4 of https://richarde.dev/papers/2021/linear-constraints/linear-c...

Linear constraints are technically just sugar, but without them it's too manual with bare -XLinearTypes.

[MarcusE1W]

Austral uses linear types as a main feature https://austral-lang.org/