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://www.cs.st-andrews.ac.uk/~eb/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.

    链接地址: http://www.djcxy.com/p/43342.html

    上一篇: 直觉型理论的组合逻辑等价物是什么？

    下一篇: Agda和Idris的区别