Idris 1.0 Released

What do we mean by “1.0”?

Idris version 1.0 corresponds to the language as described in Type-Driven Development with Idris, published last week by Manning.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Idris' uptake

In the recent years, Idris had a surprisingly uptake in adoption. It used to be, in some ways, the poor sibling of Agda, which can be explained by the fact that it is more programming-oriented than proof-assistance-oriented, and that the userbase for dependently typed programming language was mostly restricted to people interested in proof assistants.

I would guess that this community focus remains true in general, but Idris managed to make enough improvements to its usability to become approachable by less-experts. In particular, while Idris used to be mostly a one-developer (Edwin Brady) show, there are now strictly more than one people actively contributing to the codebase (see github statistics); David Christiansen's PhD work on the language helped not only in terms of code contributions, but also in continuing to increase the language visibility.

I think that this is very good news for the "rich type systems" community. The enthusiasm for Idris among, for example, Haskell programmers, is a sure sign that there is a sizeable community of people that are interested in adopting yet more advanced, yet less-understood type systems and programming language designs. I used to be surprised that languages such as Haskell and OCaml could manage to form a critical mass despite their otherness; Idris is one of today's underdogs (not alone: other dependent languages and proof assistants, such as Coq, Agda, Isabelle, Lean, also made a ton of progress in the last decade), and the interest for them says something positive about the world of programming (and proving): people are curious and interested in advanced topics, even at a cost.

(In particular, as a programming language researcher I would see this as a motivation to keep explaining our work in a way that is accessible to interested programmers -- and non-programmers. They actually care.)

Open Issues

I think I like Idris but it also seems to have a lot of issues ranging from errors in the typing system to stack overflows.

I personally wanted to go into the other direction: No types, since that always seems to open a humongous can of worms, and no stack, since my experience with stack-based functional languages is rather lousy.

I like KISS robust stuff but I'll also gladly admit it's probably a lousy absurdist idea.