Idris 2 version 0.2.1 | Hacker News Reader

Idris 2 version 0.2.1

idris-lang.org

129 pointsthomasdziedzic16 comments

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

> 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

Woops, misread that, edited my comment. Thanks.

> 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

more info;

https://github.com/project-everest/hacl-star

https://rise4fun.com/FStar/tutorial/jsStar

a target is something you compile to, but LowStar is a subset, it is something you compile from.

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.

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

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

These RFCs were closed https://github.com/rust-lang/rfcs/issues/1930

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!

> 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

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.

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.

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

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

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.

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.

Reply on news.ycombinator.com