Différences entre Agda et Idris

Question

Je commence à me plonger dans la programmation typée de manière dépendante et j'ai trouvé que les langages Agda et Idris sont les plus proches de Haskell, donc j'ai commencé par là.

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

J'ai été capable d'en repérer quelques-uns :

• Idris a des classes de type à la Haskell, tandis qu'Agda utilise des arguments d'instance.
• Idris inclut la notation monadique et applicative
• Les deux semblent avoir une sorte de syntaxe réversible, mais je ne suis pas sûr qu'il s'agisse de la même chose.

---

Modifier : 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/

Answer 1

Je ne suis peut-être pas la meilleure personne pour répondre à cette question, 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 à ce sujet, mais je voudrais m'étendre un peu sur le sujet :

Idris a été conçu dès le départ pour supporter la programmation générale avant la démonstration de théorèmes, et en tant que tel, il possède des caractéristiques de haut niveau telles que les classes de types, la notation do, les parenthèses idiomatiques, les compréhensions de listes, la surcharge, etc. Idris privilégie la programmation de haut niveau par rapport à la preuve interactive, bien qu'étant donné qu'Idris est construit sur un élaborateur basé sur les tactiques, il existe une interface vers un proverbe de théorème interactif basé sur les tactiques (un peu comme Coq, mais pas aussi avancé, du moins pas encore).

Une autre chose qu'Idris vise à bien supporter est l'implémentation de DSL embarqués. Avec Haskell, vous pouvez aller loin avec la notation do, et vous le pouvez aussi avec Idris, mais vous pouvez aussi relier d'autres constructions comme 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 des détails complets 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 par Haskell, Idris par 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 s'il est bien maintenu. Un des objectifs principaux d'Idris sera toujours de générer du 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 sur de nombreux points importants. Je pense que la principale différence réside dans la gestion des univers. Agda a le polymorphisme d'univers, Idris a le polymorphisme d'univers. cumulativité (et vous pouvez avoir Set : Set dans les deux cas si vous trouvez cela trop restrictif et que cela ne vous dérange pas que vos preuves puissent être bancales).

Answer 2

Une autre différence entre Idris et Agda est que l'égalité propositionnelle d'Idris est hétérogène, alors 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

alors qu'en Agda, c'est

data __ {l} {A : Set l} (x : A) : A  Set a where
    refl : x  x

Le l de la définition d'Agda peut être ignoré, car il a trait au polymorphisme de l'univers qu'Edwin mentionne dans sa réponse.

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

En d'autres termes, en Idris, on peut affirmer que deux choses de types différents sont égales (même si cette affirmation n'est pas prouvable), alors qu'en Agda, cette affirmation est absurde.

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

L'exemple le plus simple est peut-être l'associativité de la concaténation de vecteurs. Étant donné des listes indexées par la 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 la concaténation avec le type suivant :

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

nous pourrions vouloir le prouver :

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

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