Différences entre Agda et Idris

Question

Je commence à plonger dans une programmation de type dépendance et j'ai découvert que les langages Agda et Idris sont les plus proches de Haskell, alors j'ai commencé là-bas.

Ma question est: quelles sont les principales différences entre elles? Les systèmes de type sont-ils également exprimés 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 type à la Haskell, tandis qu'Agda va avec des arguments d'instance
• IDRIS comprend une notation monadique et applicative
• Tous deux semblent avoir une sorte de syntaxe rédiable, mais ne savent pas vraiment s'ils sont les mêmes.

---

Éditer: Il y a d'autres 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 à ceci, car après avoir implémenté IDRIS, je suis probablement un peu biaisé! La FAQ - http://docs.idris-lang.org/en/latest/faq/faq.html - a quelque chose à dire à ce sujet, mais à développer un peu:

IDRIS a été conçu à partir de zéro pour soutenir la programmation à des fins générales avant la preuve du théorème, et en tant que telle, a des fonctionnalités de haut niveau telles que les classes de type, la notation, les supports d'idiome, les compréhensions de la liste, la surcharge, etc. IDRIS met une programmation de haut niveau avant la preuve interactive, bien que parce que IDRIS est construit sur un élaborateur basé sur la tactique, il existe une interface à un prover de théorème interactif basé sur une tactique (un peu comme CoQ, mais pas aussi avancé, du moins pas encore).

Une autre chose que IDRIS vise à bien prendre en charge est la mise en œuvre DSL intégrée. Avec Haskell, vous pouvez obtenir un long chemin avec DO Notation, et vous pouvez également avec IDRIS, mais vous pouvez également relire d'autres constructions telles que l'application et la liaison variable 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-anddrews.ac.uk/drafts/dsl-idris.pdf

Une autre différence est la compilation. Agda va principalement via Haskell, Idris via C. Il y a un back-end expérimental pour Agda qui utilise le même back-end que IDRIS, via C. Je ne sais pas à quel point il est bien entretenu. Un 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 type dans AGDA et IDRIS sont assez similaires à de nombreux égards importants. Je pense que la principale différence est dans la gestion des univers. Agda a un polymorphisme d'univers, Idris a cumulavité (et vous pouvez avoir Set : Set Dans les deux si vous trouvez cela trop restrictif et ne vous dérangez pas que vos preuves pourraient être non liées).

Answer 2

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

Pendant qu'à Agda, c'est

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

Le L dans la définition d'Agda peut être ignoré, comme cela 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 AS d'arguments, tandis qu'à Idris, il peut prendre deux valeurs avec potentiellement différent les types.

En d'autres termes, dans IDRIS, on peut affirmer que deux choses avec des types différents sont égales (même si elle finit par être une affirmation non prouvable), tandis qu'à Agda, la déclaration même est un non-sens.

Cela a des conséquences importantes et larges sur la théorie des types, en particulier en ce qui concerne la faisabilité de travailler avec la théorie du type 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'indiquer des théorèmes utiles avec une égalité hétérogène qui ne peut pas être directement énoncée avec une égalité homogène.

L'exemple le plus simple est peut-être l'associativité de la concaténation des vecteurs. Des listes indexées sur la longueur appelées ainsi des 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 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 un type Vect ((n + m) + o) a. C'est une déclaration parfaitement sensée avec une égalité hétérogène.