Differences between Agda and 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).

One other difference between Idris and Agda is that Idris's propositional equality is heterogeneous, while Agda's is homogeneous.

In other words, the putative definition of equality in Idris would be:

data (=) : {a, b : Type} -> a -> b -> Type where
  refl : x = x

while in Agda, it is

data _≡_ {l} {A : Set l} (x : A) : A → Set a where
    refl : x ≡ x

The l in the Agda defintion can be ignored, as it has to do with the universe polymorphism that Edwin mentions in his answer.

The important difference is that the equality type in Agda takes two elements of A as arguments, while in Idris it can take two values with potentially different types.

In other words, in Idris one can claim that two things with different types are equal (even if it ends up being an unprovable claim), while in Agda, the very statement is nonsense.

This has important and wide-reaching consequences for the type theory, especially regarding the feasibility of working with homotopy type theory. For this, heterogeneous equality just won't work because it requires an axiom that is inconsistent with HoTT. On the other hand, it is possible to state useful theorems with heterogeneous equality that can't be straightforwardly stated with homogeneous equality.

Perhaps the easiest example is associativity of vector concatenation. Given length-indexed lists called vectors defined thusly:

data Vect : Nat -> Type -> Type where
  Nil : Vect 0 a
  (::) : a -> Vect n a -> Vect (S n) a 

and concatenation with the following type:

(++) : Vect n a -> Vect m a -> Vect (n + m) a

we might want to prove that:

concatAssoc : (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) ->
              xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

This statement is nonsense under homogeneous equality, because the left side of the equality has type Vect (n + (m + o)) a and the right side has type Vect ((n + m) + o) a. It's a perfectly sensible statement with heterogeneous equality.