3 ms·

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 si

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.

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.