Différences entre Agda et Idris

Je commence à me plonger dans la programmation à typage dépendant et j'ai trouvé que les langages Agda et Idris sont les plus proches de Haskell, alors j'ai commencé là.

Ma question est: quelles sont les principales différences entre eux? Les systèmes de types sont-ils également expressifs dans les deux? Ce serait formidable d'avoir un comparatif complet et une discussion sur les avantages.

J'ai pu en repérer:

• Idris a des classes de types à la Haskell, alors qu'Agda utilise des arguments d'instance
• Idris inclut la notation monadique et applicative
• Les deux semblent avoir une sorte de syntaxe rebindable, bien que je ne sache pas vraiment s'ils sont identiques.

Edit : il y a plus de réponses dans la page Reddit de cette question: http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

Je ne suis peut-être pas la meilleure personne pour répondre à cela, car ayant implémenté Idris, je suis probablement un peu partial! La FAQ - http://docs.idris-lang.org/en/latest/faq/faq.html - a quelque chose à dire là-dessus, mais pour en dire un peu plus:

Idris a été conçu dès le départ pour prendre en charge la programmation à usage général avant la démonstration des théorèmes, et en tant que tel, il possède des fonctionnalités de haut niveau telles que les classes de types, la notation do, les crochets idiomatiques, la compréhension de listes, la surcharge, etc. Idris place la programmation de haut niveau avant la preuve interactive, bien qu'Idris soit construit sur un élaborateur basé sur la tactique, il existe une interface vers un prouveur de théorème interactif basé sur la tactique (un peu comme Coq, mais pas aussi avancé, du moins pas encore).

Une autre chose qu'Idris vise à bien prendre en charge est la mise en œuvre du DSL intégré. Avec Haskell, vous pouvez obtenir un long chemin avec la notation do, et vous pouvez aussi avec Idris, mais vous pouvez également relier d'autres constructions telles que l'application et la liaison de variables si vous en avez besoin. Vous pouvez trouver plus de détails à ce sujet dans le tutoriel, ou tous les détails dans cet article: http://eb.host.cs.st-andrews.ac.uk/drafts/dsl-idris.pdf

Une autre différence réside dans la compilation. Agda passe principalement via Haskell, Idris via C. Il existe un back-end expérimental pour Agda qui utilise le même back-end qu'Idris, via C. Je ne sais pas à quel point il est bien entretenu. Un objectif principal d'Idris sera toujours de générer un code efficace - nous pouvons faire beaucoup mieux que ce que nous faisons actuellement, mais nous y travaillons.

Les systèmes de types d'Agda et d'Idris sont assez similaires à bien des égards. Je pense que la principale différence réside dans la gestion des univers. Agda a un polymorphisme d'univers, Idris a une cumulativité (et vous pouvez avoir les Set : Setdeux si vous trouvez cela trop restrictif et que vos preuves ne sont peut-être pas fondées).

Une autre différence entre Idris et Agda est que l'égalité propositionnelle d'Idris est hétérogène, tandis que celle d'Agda est homogène.

En d'autres termes, la définition putative de l'égalité dans Idris serait:

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

tandis qu'à Agda, c'est

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

Le l dans la définition Agda peut être ignoré, car il a à voir avec le polymorphisme de l'univers mentionné par Edwin dans sa réponse.

La différence importante est que le type d'égalité dans Agda prend deux éléments de A comme arguments, tandis que dans Idris, il peut prendre deux valeurs avec des types potentiellement différents .

En d'autres termes, dans Idris, on peut affirmer que deux choses de types différents sont égales (même si cela finit par être une affirmation non démontrable), tandis que dans Agda, l'affirmation même est absurde.

Cela a des conséquences importantes et de grande portée pour la théorie des types, en particulier en ce qui concerne la faisabilité de travailler avec la théorie des types d'homotopie. Pour cela, l'égalité hétérogène ne fonctionnera tout simplement pas car elle nécessite un axiome incompatible avec HoTT. D'un autre côté, il est possible d'énoncer des théorèmes utiles avec une égalité hétérogène qui ne peuvent pas être énoncés directement avec une égalité homogène.

L'exemple le plus simple est peut-être l'associativité de la concaténation vectorielle. Étant donné les listes indexées en longueur appelées vecteurs définis ainsi:

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

et concaténation avec le type suivant:

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

nous pourrions vouloir prouver que:

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

Cette déclaration est absurde sous égalité homogène, car le côté gauche de l'égalité a un type Vect (n + (m + o)) aet le côté droit a un type Vect ((n + m) + o) a. C'est une déclaration parfaitement sensée avec une égalité hétérogène.