[bjz_]

Yeah, I'm aware of Quantitative Type Theory, it's very cool! Another neat iteration is described in "Resourceful Dependent Types"[0]. I'm interested in what the Granule people are doing though - they can track usage information at the type level too. It's still non-dependent for now, but I hear that they are interested in extending it to dependent types too. They use an SMT solver to track usage information which is really neat - apparently it allows to track more interesting usage patterns than Blodwen can.

Sadly this doesn't do everything I want though - AFAIK, you can still have multiple out-standing references in linear typing [1]. I'd really like some story for uniqueness too in order to have support for in-place updates while avoiding a GC.

[0]: http://www2.tcs.ifi.lmu.de/~abel/talkTYPES18.pdf

[1]: https://en.wikipedia.org/wiki/Uniqueness_type#Relationship_t...