2012-02-27 24 views
140

Sto iniziando a immergermi nella programmazione tipizzata in modo dipendente e ho scoperto che le lingue Agda e Idris sono le più vicine a Haskell, quindi ho iniziato da lì.Differenze tra Agda e Idris

La mia domanda è: quali sono le principali differenze tra loro? I sistemi di tipi sono ugualmente espressi in entrambi? Sarebbe bello avere una comparativa completa e una discussione sui benefici.

Sono stato in grado di individuare alcuni:

  • Idris è di tipo classi à la Haskell, mentre Agda va con argomenti esempio
  • Idris include monadica e applicativa notazione
  • Entrambi sembrano avere una sorta di sintassi rebindable, anche se non sono sicuro che siano uguali.

Edit: ci sono alcuni più risposte nella pagina Reddit di questa domanda: http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

+1

Si potrebbe desiderare di dare un'occhiata a coq aswel, la sintassi non è un milione di miglia lontano da haskell e ha classi di tipi facili da usare :) –

+2

Per la cronaca: Al giorno d'oggi Agda ha anche notazioni monadiche e applicative. – gallais

risposta

149

io possa non essere la persona migliore per rispondere a questa domanda, per aver attuato Idris probabilmente sono un po 'prevenuto! Le FAQ - http://docs.idris-lang.org/en/latest/faq/faq.html - hanno qualcosa da dire su di esso, ma per espanderci un po ':

Idris è stato progettato da zero per supportare la programmazione generale prima della dimostrazione del teorema, e come tale ha caratteristiche di alto livello come come classi di tipi, notazione, parentesi idiomatiche, list comprehensions, overloading e così via. Idris mette la programmazione ad alto livello davanti a prove interattive, anche se poiché Idris è basato su un elaboratore basato sulla tattica, c'è un'interfaccia per un proverbio interattivo basato sulla tattica (un po 'come Coq, ma non così avanzato, almeno non ancora).

Un'altra cosa che Idris mira a supportare bene è l'implementazione DSL incorporata. Con Haskell puoi fare molta strada con la notazione, e puoi farlo anche con Idris, ma puoi anche ricollegare altri costrutti come l'applicazione e il binding variabile se necessario. Puoi trovare maggiori dettagli in questo tutorial o tutti i dettagli in questo documento: http://www.cs.st-andrews.ac.uk/~eb/drafts/dsl-idris.pdf

Un'altra differenza è nella compilazione. Agda va principalmente via Haskell, Idris via C. C'è un back end sperimentale per Agda che usa lo stesso back-end di Idris, via C. Non so quanto sia ben gestito. Un obiettivo primario di Idris sarà sempre quello di generare codice efficiente: possiamo fare molto meglio di quanto facciamo attualmente, ma ci stiamo lavorando.

I sistemi di tipi in Agda e Idris sono piuttosto simili sotto molti aspetti importanti. Penso che la principale differenza sia nella gestione degli universi. Agda ha il polimorfismo dell'universo, Idris ha cumulativity (e puoi avere Set : Set in entrambi se lo trovi troppo restrittivo e non preoccuparti che le tue dimostrazioni potrebbero non essere corrette).

+33

Cosa intendi con "... non la persona migliore per rispondere ..."? Sei una delle persone migliori a cui rispondere, dato che conosci Idris intimamente. Ora abbiamo solo bisogno di NAD per rispondere, e abbiamo l'intera immagine :) Grazie per il tempo di rispondere. –

+7

C'è qualche posto dove posso leggere di più sulla cumulatività? Non ne ho mai sentito parlare prima ... – serras

+11

[il libro di Adam Chlipala] (http://adam.chlipala.net/cpdt/html/Universes.html) è probabilmente il posto migliore: –

39

Un'altra differenza tra Idris e Agda è che l'uguaglianza proposizionale di Idris è eterogenea, mentre quella di Agda è omogenea.

In altre parole, la definizione putativo di parità 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 

La l nel defintion Agda può essere ignorato, poiché ha a che fare con il polimorfismo universale che Edwin menziona nella sua risposta.

La differenza importante è che il tipo di uguaglianza in Agda prende due elementi di A come argomenti, mentre in Idris può assumere due valori potenzialmente tipi diversi.

In altre parole, in Idris si può affermare che due cose con tipi diversi sono uguali (anche se finisce per essere una richiesta non provabile), mentre in Agda, la stessa affermazione è assurda.

Questo ha conseguenze importanti e di ampia portata per la teoria dei tipi, in particolare per quanto riguarda la fattibilità di lavorare con la teoria del tipo di omotopia. Per questo, l'uguaglianza eterogenea semplicemente non funzionerà perché richiede un assioma che è incoerente con HoTT. D'altra parte, è possibile affermare teoremi utili con un'uguaglianza eterogenea che non può essere dichiarata direttamente con un'uguaglianza omogenea.

Forse l'esempio più semplice è l'associatività della concatenazione vettoriale. Date le liste di lunghezza indicizzati denominate vettori definiti nel seguente modo:

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 

ci potrebbe voler dimostrare che:

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

Questa affermazione è una sciocchezza sotto uguaglianza omogenea, perché il lato sinistro dell'uguaglianza ha tipo Vect (n + (m + o)) a e il lato destro ha tipo Vect ((n + m) + o) a. È una frase perfettamente sensata con un'uguaglianza eterogenea.

+23

Sembra che si stia commentando di più sulla libreria standard di Agda rispetto alla teoria sottostante di Agda, ma anche la libreria standard contiene un'uguaglianza sia omogenea che eterogenea (http://www.cse.chalmers.se/~nad/listings/lib/Relation. Binary.HeterogeneousEquality.html # 1). Le persone tendono ad usare il primo più spesso, ove possibile. Quest'ultimo è equivalente a un'affermazione secondo cui i tipi sono uguali seguito da uno relativo ai valori. In un mondo in cui l'uguaglianza dei tipi è strana (HoTT), allora l'heteq è una dichiarazione più strana. –

+6

Non capisco come questa affermazione sia un'assurdità in un'uguaglianza omogenea. A meno che non mi sbagli, '(n + (m + o))' e '((n + m) + o)' sono giudicazionalmente uguali per associatività di '+' su 'ℕ' (derivato dal principio di induzione). Di conseguenza, ogni lato dell'uguaglianza ha lo stesso tipo. La differenza tra i tipi di uguaglianza è importante, ma non vedo come questo sia un esempio di ciò. –

+4

@Abhishek non è l'uguaglianza di giudizio uguale all'uguaglianza di definizione? Penso che tu intenda dire (n + (m + o)) e ((n + m) + o) sono proposizionalmente uguali ma non definitivi/giudicazionalmente uguali. –