3 ms·

> A language with dependent types and borrow checking I'm definitely interested in this! There are significant challenges here though, particularly with respec

by bjz_ 7y ago

> A language with dependent types and borrow checking I'm definitely interested in this! There are significant challenges here though, particularly with respect to combining dependent types with effects and coeffects! This is open research, but significant progress is being made, and I'm hopeful. I'm currently keeping an eye on https://github.com/granule-project/granule https://github.com/granule-project/granule, which seems like it might have some interesting things to say about this. Currently I'm trying to learn how to implement dependent types in my programming language, Pikelet: https://github.com/pikelet-lang/pikelet https://github.com/pikelet-lang/pikelet (currently doing a rebuild of the front-end in https://github.com/brendanzab/rust-nbe-for-mltt https://github.com/brendanzab/rust-nbe-for-mltt). I'm hoping that once I've done this I might eventually be able to start looking at implementing something to do with borrow checking in it, but who knows! The more I learn the less I seem to know! Always interested in chatting to people about this at our Gitter channel: https://gitter.im/pikelet-lang/Lobby https://gitter.im/pikelet-lang/Lobby > Idris is perhaps the most famous dependently typed language. I'd probably put Coq and Agda ahead of Idris in terms of being well known and established, but Idris is certainly pretty cool in how it tries to target practical programming.

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 ago
  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 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...
swsieber 7y ago
While I know of Coq and Agda, I don't associate dependent types with them at all. I did screams dependent types to me. So it might be more famous in circles of the lay people.
- bjz_ 7y ago
  Ah, that's very interesting! Yeah, perhaps Edwin Brady has been better at marketing it to a wider audience - which is not a bad thing at all.
nickpsecurity 7y ago
Isn't ATS a system language with dependent types? http://www.ats-lang.org/ http://www.ats-lang.org/
- bjz_ 7y ago
  It is, but they are not full spectrum dependent types, as far as I know. ATS doesn't have a Rust-style region system either, as far as I'm aware. It's very cool though, and quite inspiring, if a little unfriendly UX wise! :)

by bjz_ 7y ago

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

swsieber 7y ago

While I know of Coq and Agda, I don't associate dependent types with them at all. I did screams dependent types to me. So it might be more famous in circles of the lay people.

bjz_ 7y ago
Ah, that's very interesting! Yeah, perhaps Edwin Brady has been better at marketing it to a wider audience - which is not a bad thing at all.

nickpsecurity 7y ago

Isn't ATS a system language with dependent types? http://www.ats-lang.org/ http://www.ats-lang.org/

bjz_ 7y ago
It is, but they are not full spectrum dependent types, as far as I know. ATS doesn't have a Rust-style region system either, as far as I'm aware. It's very cool though, and quite inspiring, if a little unfriendly UX wise! :)