I haven’t written anything here in a while, which is mostly due to my paper about syntactic metaprogramming. It is close to being finished, but the remaining edits terrify me right now, so I thought I’d write my thoughts about this topic in hope that it will be useful to someone.

Let me prefix this by a couple of words about my experience and why I didn’t include Lean and Idris2. At the time of writing, I have roughly equal experience with the three languages named in the title. I have written Meta-Cedille in Agda, used Coq to do verification of Haskell blockchain code and Idris at Statebox for various things. The reason I don’t want talk much about Lean and Idris2 here is that I don’t have much experience with both of them, and Idris2 is unfinished. What I will say is that from what I’ve seen, Lean does compete much more with Coq than with Agda and Idris, so if you wouldn’t choose Coq reading this, you probably don’t need to consider Lean. If you would choose Coq however, then I’d advise to seriously consider Lean as well (don’t choose Lean simply because it supports quotients though. This claim is somewhat disingenuous and all the other languages here support quotients in the same way that Lean does. See for example here).

We will consider a few different categories in which the languages should compete, which should give you a good way to compare the things you care about. There are a lot more things that can be said about all of the languages, but I feel that this is already a long comparison.

  • Programming language features
    • Agda: Haskell-like syntax, very powerful mixfix notation, compiles to Haskell or JS with a very nice FFI
    • Coq: Ocaml-like syntax, recursive notation, exports to a large variety of languages
    • Idris: Haskell-like syntax, C and JS FFI

They all support type classes (sometimes under a different name) and in general everything that you might expect from Haskell-like languages with some changes in syntax. So if you’re used to writing Haskell code, it should be rather quick to get started in any of these, with a few caveats. First, Coq does not natively support IO. There are external tools like coq-io that you can use, but I haven’t tried them so I can’t say much about it. Agda and Idris both have an IO monad built-in. Agda’s implementation is missing some functions that you would expect from Haskell, but the FFI gives you easy access to every Haskell function you want. There is also the issue of termination checking. Because non-terminating functions allow you to produce a member of the empty type (which proves a false statement), all functions in all of these languages have to be terminating by default. This is enforced by a termination checker, which only finds ‘obviously’ terminating functions. In my experience maybe one in ten functions or so are not of this type. You then have to prove that your function terminates (if it does) or enable non-termination. There are also similar issues with datatype definitions and universe consistency that you might want to disable sometimes. The most recent version of Coq allows you to disable all of these checks globally (for a file). In Agda and Idris, you instead tag single functions and types to skip these checks. This is much nicer, as when you run into an infinite loop, you can easily search for functions that might be responsible. In Agda, you even have different pragmas for terminating and non-terminating functions. I also want to mention here how well the languages handle resolution of implicit arguments, as this may clutter the code quite a bit if not working properly. This is of course not a big deal in Haskell because of the Hindley-Milner algorithm. In a dependently typed setting, this algorithm doesn’t work, and there is no algorithm that always works, so we have to rely on heuristics to some extent. Long story short, Agda and Coq have very good algorithms, where I don’t think I have seen a case where the argument they didn’t figure out was very easy and obvious. Idris’s algorithm for figuring out implicits seems to be slow and fails much more often. The failures also seem sort of random to me, whereas in Agda and Coq you get an intuition about when it might fail after using it for a while.

  • Proof assistant features
    • Agda: Good metaprogramming
    • Coq: Provides large amount of tactics and a large proof library
    • Idris: Reasonable metaprogramming, does not emphasize proving

Idris doesn’t really want to compete in this space, so don’t use it for that if you don’t have to. A big issue with Idris is that because of its weak handling of implicits, even if you write a nice tactic that solves something for you, you often have to provide it with a bunch of additional arguments. This seems to be the only major difference between Agda and Idris in the tactic space, but the fact that Agda is much faster and more convenient because of its better handling of implicits make it the clear winner of the two in terms of a proof assistant. Agda and Coq are much more difficult to compare, but generally Coq proofs can be much shorter, while Agda proofs are often more readable. Also, it is sometimes a lot easier to write the same function in Agda than in Coq, which sometimes translates to an easier proof in Agda. This is especially the case when you deal with many instances of dependent pattern matching. Coq has the Equations plugin that helps with that, but then you have to learn how to use it in addition to Coq. If you really want to focus on proofs though, the extra effort might be worth it.

  • Libraries
    • Agda: A few libraries exist
    • Coq: Has the most out of the three
    • Idris: Less than Coq, more than Agda

As expected, Coq libraries are mostly about proofs and Idris libraries are mostly about programming. Agda has a little bit of both, but this is definitely its weak point. It does however have the advantage that its Haskell FFI is very good and easy to use, so you can use any Haskell library in Agda, or use Agda to write a Haskell library.

  • Tooling
    • Agda: Great emacs mode
    • Coq: CoqIDE and great emacs mode
    • Idris: Meh

If you aren’t an Emacs user, my recommendation is to bite the bullet and install it just for those languages. Install evil if you like vim and learn the few keybindings for the mode you’re using (search, etc). If you really hate Emacs, choose an editor that has a similarly powerful mode and use that, but be careful not to choose something that only gives you syntax highlighting. If your favorite editor does only support syntax highlighting for the language of your choice then pick something else. If these constraints mean that you have to learn vim, do that or reconsider your constraints. I want to further stress this point, but at this point I don’t know how. Anyway, this is especially true for Agda, which has such powerful features that I don’t think any other programming environment can really compete with it. It does allow you to put holes in your code and then gives you the ability to write terms in the holes. You can then view the type of the hole, of all bound variables and of the expression in the hole (which can contain new holes) at the same time. It also supports case-splitting and some nice search features. Coq gives you a similarly powerful interaction in proofs (using tactics), but when writing functions you are on your own. The Emacs mode does have a feature similar to case-splitting, but it’s not quite as nice as Agda’s. Idris tries to do many of the same things that Agda does, and supports more editors, but its editor interaction software has a space leak, so in addition to Idris being slow, the integration crashes every 5th time or so you want to typecheck something, and case-splitting doesn’t seem to work reliably. You also cannot put terms in holes to view their types in the context. Thus, I’ve seen people use the Idris repl and just use syntax highlighting in the editor, which is still slow and much less powerful.

So for a conclusion, if you’ve read everything above, you should clearly see my preference of Agda over Idris in almost every scenario. If you haven’t used either, but you think you need Idris for its C FFI, I think you should start with Agda, see if you can wrap the Haskell C FFI into something that you use from Agda (the answer is probably yes), and only if this fails use Idris. If you choose Idris, be prepared to wait a lot for code to compile and things to randomly not work. There are a few more things that I haven’t said about their comparison, but those wouldn’t help the case for Idris. The question Idris vs. Coq is very easy: you know already which one you want to choose by looking at the type of your project. This leaves Coq vs. Agda. This is in my opinion the most difficult of the three, if you care about proofs (otherwise, choose Agda if you don’t need to compile to Ocaml or something special like that). Generally, I would say that if you expect to have complex code, use Agda, except if you expect to have a very large amount of proofs.

As a final note, I want to redeem Idris a little bit. Even though I was very hard on it, I think the goal of having a dependently typed language that focuses on programming is a very fine one. It seems to me that because of the development of Idris2, many of the issues of Idris have been ignored for quite some time, which is how it ended up like this. I really hope that Idris2 fixes the issues mentioned here and I’m excited for its linear types. This does not change my recommendation however: if you want to switch to Idris2 later, you should use Agda and try to avoid using anything that cannot easily be translated to Idris (like Unicode and mixfix syntax). Converting source code between the two isn’t that difficult, and you save yourself a lot of headaches.

If you want to comment, please do so on the reddit thread.

TL;DR: If you care about proofs much more than about code, use Coq. Use Idris if you have a very good reason to use Idris specifically. Otherwise, use Agda.