Differences between Agda and Idris

I'm starting to dive into dependently-typed programming and have found that the Agda and Idris languages are the closest to Haskell, so I started there.

My question is: which are the main differences between them? Are the type systems equally expresive in both of them? It would be great to have a comprehensive comparative and a discussion about benefits.

I've been able to spot some:

• Idris has type classes à la Haskell, whereas Agda goes with instance arguments
• Idris includes monadic and applicative notation
• Both of them seem to have some sort of rebindable syntax, although not really sure if they are the same.

Edit: there are some more answers in the Reddit page of this question: http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

I may not be the best person to answer this, as having implemented Idris I'm probably a bit biased! The FAQ - http://docs.idris-lang.org/en/latest/faq/faq.html - has something to say on it, but to expand on that a bit:

Idris has been designed from the ground up to support general purpose programming ahead of theorem proving, and as such has high level features such as type classes, do notation, idiom brackets, list comprehensions, overloading and so on. Idris puts high level programming ahead of interactive proof, although because Idris is built on a tactic-based elaborator, there is an interface to a tactic based interactive theorem prover (a bit like Coq, but not as advanced, at least not yet).

Another thing Idris aims to support well is Embedded DSL implementation. With Haskell you can get a long way with do notation, and you can with Idris too, but you can also rebind other constructs such as application and variable binding if you need to. You can find more details on this in the tutorial, or full details in this paper: http://eb.host.cs.st-andrews.ac.uk/drafts/dsl-idris.pdf

Another difference is in compilation. Agda goes primarily via Haskell, Idris via C. There is an experimental back end for Agda which uses the same back end as Idris, via C. I don't know how well maintained it is. A primary goal of Idris will always be to generate efficient code - we can do a lot better than we currently do, but we're working on it.

The type systems in Agda and Idris are pretty similar in many important respects. I think the main difference is in the handling of universes. Agda has universe polymorphism, Idris has cumulativity (and you can have Set : Set in both if you find this too restrictive and don't mind that your proofs might be unsound).