webentwicklung-frage-antwort-db.com.de

Unterschiede zwischen Agda und Idris

Ich fange an, mich mit typabhängiger Programmierung zu beschäftigen, und habe festgestellt, dass die Sprachen Agda und Idris Haskell am nächsten sind, also habe ich dort angefangen.

Meine Frage ist: Was sind die Hauptunterschiede zwischen ihnen? Sind die Typsysteme in beiden gleich stark vertreten? Es wäre toll, einen umfassenden Vergleich und eine Diskussion über die Vorteile zu haben.

Ich konnte einige entdecken:

  • Idris hat Typklassen à la Haskell, während Agda Instanzargumenten folgt
  • Idris enthält eine monadische und eine anwendungsbezogene Notation
  • Beide scheinen eine Art wiederverbindbare Syntax zu haben, obwohl sie nicht wirklich sicher sind, ob sie gleich sind.

Bearbeiten : Auf der Reddit-Seite dieser Frage finden Sie weitere Antworten: http://www.reddit.com/r/dependent_types)/comments/q8n2q/agda_vs_idris /

159
serras

Ich bin vielleicht nicht die beste Person, um dies zu beantworten, da ich nach der Implementierung von Idris wahrscheinlich ein bisschen voreingenommen bin! Die FAQ - http://docs.idris-lang.org/en/latest/faq/faq.html - hat etwas zu sagen, aber zu erweitern Sie das ein wenig:

Idris wurde von Grund auf für die Unterstützung der Allzweckprogrammierung im Vorfeld der Satzprüfung entwickelt und verfügt als solche über Funktionen auf hoher Ebene wie Typklassen, Do-Notation, Redewendungen, Listenverständnis, Überladung usw. Idris stellt die Programmierung auf hohem Niveau vor den interaktiven Beweis. Da Idris jedoch auf einem taktikbasierten Auswerter basiert, gibt es eine Schnittstelle zu einem taktikbasierten interaktiven Theorembeweiser (ein bisschen wie Coq, aber nicht so fortgeschritten, zumindest noch nicht).

Ein weiteres Ziel von Idris ist die Unterstützung der Embedded DSL-Implementierung. Mit Haskell können Sie einen langen Weg mit der Do-Notation zurücklegen, und mit Idris auch, aber Sie können auch andere Konstrukte wie die Anwendungs- und Variablenbindung neu binden, wenn Sie dies benötigen. Weitere Informationen hierzu finden Sie im Lernprogramm oder ausführlich in diesem Artikel: http://www.cs.st-andrews.ac.uk/~eb/drafts/dsl-idris.pdf =

Ein weiterer Unterschied liegt in der Zusammenstellung. Agda geht hauptsächlich über Haskell, Idris über C. Es gibt ein experimentelles Backend für Agda, das dasselbe Backend wie Idris verwendet, über C. Ich weiß nicht, wie gut es gepflegt ist. Ein vorrangiges Ziel von Idris wird es immer sein, effizienten Code zu generieren - wir können viel besser als derzeit, aber wir arbeiten daran.

Die Typsysteme in Agda und Idris sind in vielerlei Hinsicht ziemlich ähnlich. Ich denke, der Hauptunterschied liegt im Umgang mit Universen. Agda hat Universumspolymorphismus, Idris hat Kumulativität (und Sie können Set : Set In beiden haben, wenn Sie dies zu restriktiv finden und nichts dagegen haben, dass Ihre Beweise nicht stimmen).

177
Edwin Brady

Ein weiterer Unterschied zwischen Idris und Agda besteht darin, dass die Aussagengleichheit von Idris heterogen ist, während die von Agda homogen ist.

Mit anderen Worten, die putative Definition von Gleichheit in Idris wäre:

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

während in Agda ist es

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

Das l in der Agda-Definition kann ignoriert werden, da es mit dem Universumspolymorphismus zu tun hat, den Edwin in seiner Antwort erwähnt.

Der wichtige Unterschied besteht darin, dass der Gleichheitstyp in Agda zwei Elemente von A als Argumente verwendet, während er in Idris zwei Werte mit möglicherweise verschiedenen Typen annehmen kann.

Mit anderen Worten, in Idris kann man behaupten, dass zwei Dinge mit unterschiedlichen Typen gleich sind (auch wenn es sich um eine unbeweisbare Behauptung handelt), während in Agda die Aussage Unsinn ist.

Dies hat wichtige und weitreichende Konsequenzen für die Typentheorie, insbesondere hinsichtlich der Machbarkeit der Arbeit mit der Homotopietypentheorie. Hierfür wird heterogene Gleichheit einfach nicht funktionieren, da sie ein Axiom erfordert, das nicht mit HoTT vereinbar ist. Andererseits ist es möglich, nützliche Theoreme mit heterogener Gleichheit zu formulieren, die mit homogener Gleichheit nicht einfach ausgedrückt werden können.

Das vielleicht einfachste Beispiel ist die Assoziativität der Vektorverkettung. Gegebene längenindexierte Listen, die Vektoren genannt werden, sind folgendermaßen definiert:

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

und Verkettung mit folgendem Typ:

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

wir möchten vielleicht beweisen, dass:

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

Diese Aussage ist bei homogener Gleichheit Unsinn, weil die linke Seite der Gleichheit den Typ Vect (n + (m + o)) a und die rechte Seite den Typ Vect ((n + m) + o) a hat. Es ist eine absolut vernünftige Aussage mit heterogener Gleichheit.

46