Еще одно различие между Идрисом и Агдой состоит в том, что пропозициональное равенство Идриса неоднородно, в то время как Агда однородно.
Другими словами, предполагаемое определение равенства в Идрисе будет:
data (=) : {a, b : Type} -> a -> b -> Type where
refl : x = x
в Агде -
data _≡_ {l} {A : Set l} (x : A) : A → Set a where
refl : x ≡ x
Значение l в определении Агды можно игнорировать, так как оно связано с полиморфизмом вселенной, который Эдвин упоминает в своем ответе.
Важным отличием является то, что тип равенства в Agda принимает два элемента A в качестве аргументов, в то время как в Idris он может принимать два значения с потенциально различными типами.
Другими словами, в Idris можноутверждают, что две вещи с разными типами равны (даже если это оказывается недоказуемым утверждением), тогда как в Агде само утверждение является бессмысленным.
Это имеет важные и далеко идущие последствия для теории типов, особенно в отношении возможности работы с теорией гомотопических типов.Для этого гетерогенное равенство просто не сработает, потому что для этого нужна аксиома, несовместимая с HoTT.С другой стороны, можно сформулировать полезные теоремы с неоднородным равенством, которые не могут быть прямо сформулированы с однородным равенством.
Возможно, самый простой пример - ассоциативность конкатенации векторов.Для заданных индексированных по длине списков, называемых векторами, определенными таким образом:
data Vect : Nat -> Type -> Type where
Nil : Vect 0 a
(::) : a -> Vect n a -> Vect (S n) a
и конкатенация со следующим типом:
(++) : Vect n a -> Vect m a -> Vect (n + m) a
, мы можем доказать, что:
concatAssoc : (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) ->
xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
Это утверждение бессмысленно при однородном равенстве, потому что левая часть равенства имеет тип Vect (n + (m + o)) a, а правая часть имеет тип Vect ((n + m) + o) a.Это совершенно разумное утверждение с неоднородным равенством.