First impressions of Idris

By: on April 30, 2016

Lately I’ve invested some time learning Idris. I wanted to share some thoughts on being a beginner at Idris, in no particular order. My experience has been positive overall, so if you’ve been tempted to try it out, I hope this will encourage you to go ahead.

I’m not going to discuss my motivation for learning Idris in this post, though I’d like to write about that separately at some point. I’m also not aiming to try to convince you that you should learn it, but if you want a tiny taste of the appeal, check out this video of a ‘typesafe printf’.

Here are my thoughts, then:

  • I’m pretty sure I’ve only scratched the surface so far. I’ve only really been playing with dependent types, but there a bunch of other interesting features, like the effect system and uniqueness types just to name a couple.

  • The project seems pretty mature. I’m not sure exactly when it was started, but if you look around you’ll find resources on it going back a good few years. The upshot is that everything feels quite polished; for example I found the compiler/REPL to be fast and user-friendly, and I didn’t even manage to crash it.

  • I found it very easy to start playing with Idris. Installation was a matter of

    pacman -S idris

    . It’s probably worth noting at this point that I’ve been playing with version 0.11. The REPL felt very ergonomic, and moving from REPL to my usual editor involved remarkably little ceremony: you can just start writing definitions in a file and then loading them into the REPL à la Python.

  • There’s a pretty good written tutorial if you’re into that kind of thing, but personally I found watching the videos of a course given by Edwin Brady to be more entertaining. There’s also a book, Type-Driven Development with Idris; I haven’t looked at it yet but certainly plan to.

  • Editor integration looks promising. They have the usual suspects covered in the idris-hackers Github org, but more than that, they’ve actually designed an IDE protocol, so if your favourite editor isn’t supported yet, you can probably fix that without too much effort. I tried the emacs mode briefly and it seemed fairly comprehensive, though I had to turn it off due (I suspect) to the rest of my config being a bit finicky. I felt like I got most of the benefit of an IDE just by using a normal editor plus the REPL, which is surely a credit to the quality of the REPL plus some features of the language which deserve their own point:

  • I think I’m going to miss so-called metavars/holes when using other languages now. This feature of the language allows you to run the type-checker before finishing the program. I found this to be a significant productivity booster and ended up running the type-checker much more frequently than with, say, Haskell, and therefore getting nudged back on track sooner by the feedback from the compiler. (To be fair, I think GHC is getting/has recently got typed holes, too.)

  • A lot of the interest in languages like Idris comes from the idea that you can do ‘real proofs’ in them. I wasn’t sure how well this would work in practice, so I decided to just dive in and ‘port’ a theorem such as you might find in an undergraduate math course (together with its proof, of course) to Idris. The theorem I chose was ‘there are infinitely many prime numbers’, based on a dim recollection from university that it admits a simple, elementary proof. I’m pleased to say that I did manage to prove it in Idris, though it took rather longer than I expected. I might dissect this proof in a future post.

  • My experiences with the Idris community so far have been positive. There’s an IRC channel (#idris on Freenode) and a mailing list, both of which seem quite active. While I was proving the theorem about prime numbers I got stuck a few times and asked questions in the IRC channel, and promptly received patient responses from some more experienced Idris users. (Many thanks to them for that.)

  • Before I started I was a little concerned that the dependent type system would feel alien or unintuitive to use, or would have some inscrutable edge cases, but so far that fear has been unwarranted. It probably helps to know the basics of Martin-Löf type theory though. I found the first chapter of the Homotopy Type Theory book to be an approachable introduction.

  • If you’re interested in Idris but don’t know Haskell (well), you may want to play around with that first. The syntax is very similar (though diverging), and data type definitions in Idris have a similar feel to GADTs in Haskell. Haskell fans, take note: Idris is eager by default. (Personally, I didn’t miss the laziness-by-default at all…)

Share

Leave a Reply

Your email address will not be published.

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>

*