Differences between Agda and Idris

Question

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/

Solution 1

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).

Solution 2

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.

Comments

[Admin]

You might wanna have a look at coq aswel, the syntax is not a million miles away from haskell and it has easy to use type classes :)

[gallais]

For the record: Agda also has monadic and applicative notations nowadays.

[n247s]

What do you mean, "... not the best person to answer ..."? You're one of the best people to answer, since you know Idris intimately. Now we just need NAD to reply as well, and we have the whole picture :) Thanks for taking the time to reply.

[serras]

Is there any place where I can read more about cumulativity? I've never heard about that before...

[Edwin Brady]

Adam Chlipala's book is probably the best place:

[David Christiansen]

The first chapter of the HoTT book also describes it fairly clearly, if concisely.

[Mysterious Dan]

You seem to be commenting more on the Agda standard library than Agda's underlying theory, but even the standard library contains both homogeneous and heterogeneous equality (cse.chalmers.se/~nad/listings/lib/…). People just tend to use the former more often where possible. The latter is equivalent to a statement that the types are equal followed by one about the values. In a world where type equality is weird (HoTT) then heteq is a weirder statement.

[Admin]

I don't understand how that statement is nonsense under homogeneous equality. Unless I'm mistaken, (n + (m + o)) and ((n + m) + o) are judgmentally equal by associativity of + on ℕ (derived from the induction principle). Accordingly each side of the equality does have the same type. The difference between the types of equality is important, but I don't see how this is an example of that.

[Tom Crockett]

@Abhishek isn't judgmental equality the same as definitional equality? I think you mean to say (n + (m + o)) and ((n + m) + o) are propositionally equal but not definitionally/judgmentally equal.

[Abhishek Anand]

right. I meant propositional equality when I said judgemental equality. Sorry. Here is the corrected comment: (n + (m + o)) and ((n + m) + o) are propositionally equal but not definitionally equal. If you have a:A , a:B holds only if A and B are definitionally equal types. For decidability of typechecking, definitional equality has to be decidable. In extensional type theories, definitional equality coincides with propositional equality and hence typechecking is undecidable.In Coq, definitional equality only includes computation, alpha equality, definitional unfolding.

[joel]

is that DSL only in Idris 1? If so, would it be worth mentioning that?