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.
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 :) –
Per la cronaca: Al giorno d'oggi Agda ha anche notazioni monadiche e applicative. – gallais