5 ms·

Idris 2 version 0.2.1

129 points by thomasdziedzic 6y ago

guerrilla 6y ago
Differences beteen Idris 1 and 2: [1] 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? [1]. https://idris2.readthedocs.io/en/latest/updates/updates.html https://idris2.readthedocs.io/en/latest/updates/updates.html
- ska80 6y ago
  > Note also the default target is Chez Scheme (Racket and Gambit supported) instead of C (which it still supports) because its faster. 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
  - guerrilla 6y ago
    Woops, misread that, edited my comment. Thanks.
- tluyben2 6y ago
  > 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; https://fstarlang.github.io/lowstar/html/LowStar.html https://fstarlang.github.io/lowstar/html/LowStar.html more info; https://github.com/project-everest/hacl-star https://github.com/project-everest/hacl-star https://rise4fun.com/FStar/tutorial/jsStar https://rise4fun.com/FStar/tutorial/jsStar
  - iso8859-1 6y ago
    a target is something you compile to, but LowStar is a subset, it is something you compile from.
    - tluyben2 6y ago
      Well it is a subset of F* which compiles to C. So you do not compile to lowstar, lowstar is the F* you write which compiles to C.
Smaug123 6y ago
Quantitative types would have caught so many of my bugs over the years. I can't wait for this to become mainstream!
- fluffything 6y ago
  There is a Rust RFC for extending Rust's const generics to dependent types. 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-fully-dependent-pi-types.md https://github.com/ticki/rfcs/blob/pi-types-ext-2/text/0000-...
  - steveklabnik 6y ago
    These RFCs were closed https://github.com/rust-lang/rfcs/issues/1930 https://github.com/rust-lang/rfcs/issues/1930 In favor of https://github.com/rust-lang/rfcs/pull/2000 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!
    - deleted 6y ago
      [deleted]
    - fluffything 6y ago
      > These RFCs were closed 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 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.
      - steveklabnik 6y ago
        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.
vmchale 6y ago
Good stuff! Thanks to all contributors, I'll have to start porting my libraries :p
davidwritesbugs 6y ago
I'm waiting for someone to update Brew which is currently at 1.3. Installing 2.0 is currently a bit of a faff.
- kryptiskt 6y ago
  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.
  - davidwritesbugs 6y ago
    Thanks. I'd assumed idris2 would replace idris so I didn't try searching for anything else. I've just grabbed it, thanks very much for the tip.

Differences beteen Idris 1 and 2: [1] 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? [1]. https://idris2.readthedocs.io/en/latest/updates/updates.html https://idris2.readthedocs.io/en/latest/updates/updates.html

ska80 6y ago
> Note also the default target is Chez Scheme (Racket and Gambit supported) instead of C (which it still supports) because its faster. 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
- guerrilla 6y ago
  Woops, misread that, edited my comment. Thanks.
tluyben2 6y ago
> 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; https://fstarlang.github.io/lowstar/html/LowStar.html https://fstarlang.github.io/lowstar/html/LowStar.html more info; https://github.com/project-everest/hacl-star https://github.com/project-everest/hacl-star https://rise4fun.com/FStar/tutorial/jsStar https://rise4fun.com/FStar/tutorial/jsStar
- iso8859-1 6y ago
  a target is something you compile to, but LowStar is a subset, it is something you compile from.
  - tluyben2 6y ago
    Well it is a subset of F* which compiles to C. So you do not compile to lowstar, lowstar is the F* you write which compiles to C.

Smaug123 6y ago

Quantitative types would have caught so many of my bugs over the years. I can't wait for this to become mainstream!

fluffything 6y ago
There is a Rust RFC for extending Rust's const generics to dependent types. 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-fully-dependent-pi-types.md https://github.com/ticki/rfcs/blob/pi-types-ext-2/text/0000-...
- steveklabnik 6y ago
  These RFCs were closed https://github.com/rust-lang/rfcs/issues/1930 https://github.com/rust-lang/rfcs/issues/1930 In favor of https://github.com/rust-lang/rfcs/pull/2000 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!
  - deleted 6y ago
    [deleted]
  - fluffything 6y ago
    > These RFCs were closed 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 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.
    - steveklabnik 6y ago
      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.

vmchale 6y ago

Good stuff! Thanks to all contributors, I'll have to start porting my libraries :p

davidwritesbugs 6y ago

I'm waiting for someone to update Brew which is currently at 1.3. Installing 2.0 is currently a bit of a faff.

kryptiskt 6y ago
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.
- davidwritesbugs 6y ago
  Thanks. I'd assumed idris2 would replace idris so I didn't try searching for anything else. I've just grabbed it, thanks very much for the tip.