A good foundation for such a language would be one based on Quantitative Type Theory [0]. It’s a dependent type theory that records usage information in every typing judgement.
The Idris successor, Blodwen [1] is being based on it.
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.
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...