There are a bunch of new features (scroll down to that in the doc) but the main thing seems to be moving to QTT (seems similar in theme to the bicolored calculus of constructions?) which allows explicit handling of erasure. Nice to see this as its the logical next step and consitent with Edwin Brady's larger project of making dependent types practical.
Note also the default target is Chez Scheme (Racket and Gambit supported) instead of C because its faster. Wouldn't it be funny to port it to Chicken?
> Note also the default target is Chez Scheme (Racket and Gambit supported) instead of C (which it still supports) because its faster.
That was Idris 1 with the slow C backend.
I believe he needs help on backends as he is not an expert at that; Idris 2 really has a chance of becoming a quite optimal language. I wish Rise4fun.com (MS research) would fund this work; they are doing everything right (for a decade already), I just don't want a language like this to run on the jvm/clr, well, I mean solely; it should be a choice. But I do think the funding (it's MS...) and the people at this particular research dep could really help. For instance F* has really cool 'targets' like;
I don't think that we're really at odds here, I think I'm just more conservative when representing the status of the feature than you are. It's already taken over three years for the minimal version of the feature, and the author of the PI types trilogy RFCs has quit open source entirely. I just don't want to give the impression that this is happening any time soon.
In Idris2 they are quite practical already; it is not trivial (to say it lightly) to add them to mainstream languages. Even in a not much used research language, like Idris, it already breaks quite a lot of backward compatibility.
idris2 is its own package on brew (and should be everywhere, idris and idris2 doesn't share any code) and there should be no problems installing them in parallel.
17 comments
[ 4.0 ms ] story [ 53.7 ms ] threadThere are a bunch of new features (scroll down to that in the doc) but the main thing seems to be moving to QTT (seems similar in theme to the bicolored calculus of constructions?) which allows explicit handling of erasure. Nice to see this as its the logical next step and consitent with Edwin Brady's larger project of making dependent types practical.
Note also the default target is Chez Scheme (Racket and Gambit supported) instead of C because its faster. Wouldn't it be funny to port it to Chicken?
[1]. https://idris2.readthedocs.io/en/latest/updates/updates.html
Idris 2 currently doesn't have C code generator. But you can still use external shared libraries implemented in C
> Wouldn't it be funny to port it to Chicken?
Idris 2 used to have Chicken CG :) but it was then removed due to the maintenance burden
That was Idris 1 with the slow C backend.
I believe he needs help on backends as he is not an expert at that; Idris 2 really has a chance of becoming a quite optimal language. I wish Rise4fun.com (MS research) would fund this work; they are doing everything right (for a decade already), I just don't want a language like this to run on the jvm/clr, well, I mean solely; it should be a choice. But I do think the funding (it's MS...) and the people at this particular research dep could really help. For instance F* has really cool 'targets' like;
https://fstarlang.github.io/lowstar/html/LowStar.html
more info;
https://github.com/project-everest/hacl-star
https://rise4fun.com/FStar/tutorial/jsStar
Part 0 (the minimal const generics) might be stabilized in the near future. Parts 1-3 would hopefully be explored next. Fully dependent types are introduced in part 3: https://github.com/ticki/rfcs/blob/pi-types-ext-2/text/0000-...
In favor of https://github.com/rust-lang/rfcs/pull/2000
No other designs have been accepted to extend this yet. We're still implementing what was already accepted!
Can be reopened after minimal const generics implementation is finished (like the post discussing closure suggests) which it almost is.
> In favor of https://github.com/rust-lang/rfcs/pull/2000
That's the minimal const generics RFC.
> No other designs have been accepted to extend this yet.
A design does not need to be accepted for exploration about such a design to start.