6 ms·
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 t
by iamrecursion 7y ago
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.
[0] https://bentnib.org/quantitative-type-theory.pdf https://bentnib.org/quantitative-type-theory.pdf
[1] https://github.com/edwinb/Blodwen https://github.com/edwinb/Blodwen
- bjz_ 7y agoYeah, 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 http://www2.tcs.ifi.lmu.de/~abel/talkTYPES18.pdf [1]: https://en.wikipedia.org/wiki/Uniqueness_type#Relationship_to_linear_typing https://en.wikipedia.org/wiki/Uniqueness_type#Relationship_t...