Différences entre Agda et Idris

Question

Je commence à plonger dans la programmation dépendante 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 cas? Ce serait formidable d'avoir un comparatif complet et une discussion sur les avantages.

Je suis en mesure de repérer quelques-uns:

• Idris est de type cours à la Haskell, alors que Agda va de pair avec des arguments d'instance
• Idris comprend la notation monadique qu'applicatif
• Les deux semblent avoir une sorte de syntaxe rebindable, mais pas vraiment sûr si elles sont identiques.

---

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 peux pas être la meilleure personne pour répondre, comme ayant mis en œuvre Idris Je suis probablement un peu biaisé! La FAQ - http://docs.idris-lang.org/en/latest/faq/faq.html - a quelque chose à dire là-dessus, mais pour développer un peu:

Idris a été conçu à partir de zéro pour soutenir la programmation générale avant la démonstration du théorème, et en tant que telle a des caractéristiques de haut niveau telles en tant que classes de types, faites la notation, les parenthèses d'idiome, les compréhensions de liste, la surcharge et ainsi de suite. Idris met la programmation de haut niveau avant la preuve interactive, mais comme Idris est construit sur un élaborateur tactique, il existe une interface avec un prouveur de théorème interactif tactique (un peu comme Coq, mais pas aussi avancé, du moins pas encore).

Une autre chose que Idris vise à bien soutenir est l'implémentation DSL embarquée. Avec Haskell vous pouvez obtenir un long chemin avec la notation Do, et vous pouvez le faire avec Idris aussi, 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 ce document: http://www.cs.st-andrews.ac.uk/~eb/drafts/dsl-idris.pdf

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

Les systèmes de types dans Agda et Idris sont assez similaires sur de nombreux points importants. Je pense que la principale différence est dans la gestion des univers. Agda a un polymorphisme de l'univers, Idris a cumulativity (et vous pouvez avoir Set : Set dans les deux si vous trouvez cela trop restrictif et que cela ne vous dérange pas que vos preuves soient erronées).

Answer 2

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 supposée de l'égalité dans Idris serait:

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

tout en Agda, il est

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

L dans la défintion Agda peut être ignoré, comme a à voir avec le polymorphisme de l'univers qu'Edwin mentionne 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 potentiellement différents types. 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 revendication indémontrable), tandis que dans Agda, l'affirmation même est un non-sens.

Ceci a des conséquences importantes et étendues 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 d'égalité hétérogène qui ne peuvent être énoncés directement avec une égalité homogène.

L'exemple le plus simple est peut-être l'associativité de la concaténation vectorielle. Compte tenu des listes indexées longueur appelés 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 

que 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 un non-sens sous é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.