Differenze tra Agda e Idris

Question

Sto iniziando a tuffarsi dipendente tipizzate di programmazione e abbiamo scoperto che la Agda e Idris lingue sono il più vicino al Haskell, così ho iniziato lì.

La mia domanda è:quali sono le principali differenze tra di loro?Sono il tipo di sistemi altrettanto espressive in entrambi?Sarebbe bello avere una completa e comparativa e una discussione sui benefici.

Sono stato in grado di individuare alcuni:

• Idris ha classi di tipo à la Haskell, mentre Agda va con istanza argomenti
• Idris include monadico e applicativi notazione
• I due sembrano avere una sorta di rebindable sintassi, anche se non so se sono la stessa cosa.

---

Modifica:ci sono alcune risposte in Reddit pagina di questa domanda: http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

Answer 1

Non posso essere la persona migliore per rispondere a questa, come di aver attuato Idris io sono probabilmente un po ' di parte!FAQ - http://docs.idris-lang.org/en/latest/faq/faq.html - ha qualcosa da dire su di esso, ma di espandere un po':

Idris è stato progettato da zero per supportare scopo generale di programmazione avanti del teorema di dimostrare, e come tale ha un elevato livello di caratteristiche come il tipo di classi, fare notazione, idioma parentesi, list comprehensions, sovraccarico e così via.Idris mette di programmazione ad alto livello davanti interattiva di prova, anche se a causa Idris è costruito su una tattica basata su elaboratore, c'è un'interfaccia per una tattica interattivo su theorem prover (un po ' come il Coq, ma non è avanzato, almeno non ancora).

Un'altra cosa Idris, che mira a sostenere ben Incorporato DSL attuazione.Con Haskell è possibile ottenere una lunga strada da fare, notazione, e si può con Idris troppo, ma si può anche rifare la connessione ad altri costrutti come applicazione e variabile vincolante, se è necessario.Potete trovare maggiori dettagli su questo tutorial, tutti i dettagli in questo articolo: http://eb.host.cs.st-andrews.ac.uk/drafts/dsl-idris.pdf

Un'altra differenza è nella compilation.Agda va principalmente tramite Haskell, Idris via C.C'è sperimentale di back-end per Agda, che utilizza lo stesso back-end come Idris, via C.Non so come ben mantenuto è.Un obiettivo primario di Idris sarà sempre quello di generare codice efficiente - si può fare molto meglio di quanto noi oggi, ma stiamo lavorando su di esso.

Il tipo di sistemi di Agda e Idris sono abbastanza simili in molti aspetti importanti.Penso che la principale differenza è nella gestione degli universi.Agda ha universo polimorfismo, Idris ha cumulativity (e si può avere Set : Set sia se si trova questo troppo restrittive e non la mente che le prove potrebbero essere sbagliate).

Answer 2

Un'altra differenza tra Idris e Agda è che Idris del proposizionale uguaglianza è eterogeneo, mentre Agda è omogenea.

In altre parole, il putativo definizione di uguaglianza in Idris sarebbe:

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

mentre in Agda, è

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

L in Agda definizione può essere ignorato, in quanto ha a che fare con l'universo di polimorfismo che Edwin cita nella sua risposta.

La differenza importante è che la parità di tipo di Agda prende due elementi di argomenti, mentre in Idris può assumere due valori potenzialmente diversi tipi di.

In altre parole, in Idris si può pretendere che le due cose con diversi tipi sono uguali (anche se si finisce per essere un'affermazione indimostrabile), mentre in Agda, la stessa affermazione è una sciocchezza.

Questo è importante e di ampio respiro, conseguenze per il tipo di teoria, soprattutto per quanto riguarda la fattibilità di lavoro con homotopy tipo di teoria.Per questo, eterogenei uguaglianza non funzionano, perché richiede un assioma che non è coerente con HoTT.D'altra parte, è possibile affermare utile teoremi eterogenei di uguaglianza che non può essere semplicemente indicato con omogenea uguaglianza.

Forse il modo più semplice esempio è l'associatività del vettore di stringhe.Data la lunghezza indicizzati elenchi chiamate vettori definiti protettori così:

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

e la concatenazione con il seguente tipo:

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

si potrebbe desiderare di provare che:

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

Questa affermazione è priva di senso sotto omogenea di uguaglianza, perchè il lato sinistro dell'uguaglianza è il tipo di Vect (n + (m + o)) a e il lato destro ha il tipo Vect ((n + m) + o) a.E ' perfettamente sensato istruzione eterogenei uguaglianza.