Một khác biệt khác giữa Idris và Agda là bình đẳng mệnh đề của Idris là không đồng nhất, trong khi Agda là đồng nhất.
Nói cách khác, định nghĩa giả định về sự bình đẳng trong Idris sẽ là:
data (=) : {a, b : Type} -> a -> b -> Type where
refl : x = x
trong khi ở Agda, nó là
data _≡_ {l} {A : Set l} (x : A) : A → Set a where
refl : x ≡ x
Các l trong defintion Agda thể bỏ qua, vì nó liên quan đến sự đa hình vũ trụ mà Edwin đề cập đến trong câu trả lời của ông.
Sự khác biệt quan trọng là loại bình đẳng trong Agda lấy hai phần tử A làm đối số, trong khi ở Idris, có thể lấy hai giá trị có khả năng là loại khác nhau.
Nói cách khác, trong Idris người ta có thể tuyên bố rằng hai điều với các loại khác nhau là bằng nhau (ngay cả khi nó kết thúc là một yêu cầu không thể giải quyết), trong khi ở Agda, tuyên bố rất vô nghĩa.
Điều này có những hậu quả quan trọng và rộng lớn đối với lý thuyết loại, đặc biệt là về tính khả thi khi làm việc với lý thuyết loại đồng luân. Đối với điều này, sự bình đẳng không đồng nhất sẽ không hoạt động vì nó đòi hỏi một tiên đề không phù hợp với HoTT. Mặt khác, có thể đưa ra các định lý hữu ích với sự bình đẳng không đồng nhất mà không thể nói thẳng với sự bình đẳng đồng nhất.
Có lẽ ví dụ đơn giản nhất là tính liên kết của vectơ nối. danh sách dài-lập chỉ mục cho gọi là vectơ định nghĩa thusly:
data Vect : Nat -> Type -> Type where
Nil : Vect 0 a
(::) : a -> Vect n a -> Vect (S n) a
và nối với các loại sau đây:
(++) : Vect n a -> Vect m a -> Vect (n + m) a
chúng ta có thể muốn chứng minh rằng:
concatAssoc : (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) ->
xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
Tuyên bố này là vô nghĩa dưới sự bình đẳng đồng nhất, bởi vì phía bên trái của sự bình đẳng có loại Vect (n + (m + o)) a và phía bên phải có loại Vect ((n + m) + o) a. Đó là một tuyên bố hoàn toàn hợp lý với sự bình đẳng không đồng nhất.
Bạn có thể muốn có một cái nhìn tại Coq aswel, cú pháp không phải là một triệu dặm từ Haskell và nó có dễ dàng để sử dụng các lớp học kiểu :) –
Đối với hồ sơ: Agda cũng có ký hiệu monadic và applicative hiện nay. – gallais