Различия между Agda и Idris

Question

Я начинаю погружаться в программируемое программирование и обнаружил, что языки Agda и Idris наиболее близки к Haskell, поэтому я начал там.

Мой вопрос: что является основным отличием между ними? Являются ли системы типов одинаково экспрессивными в обоих из них? Было бы здорово иметь всестороннюю сравнительную и дискуссию о преимуществах.

Я был в состоянии определить некоторые из них:

• Идрис имеет тип классы а-ля Haskell, в то время как Agda идет с аргументами экземпляра
• Идрис включает одноместную и аппликативного обозначения
• Оба из них, кажется, имеют какой-то перезаписываемый синтаксис, хотя и не совсем уверены, что они одинаковы.

---

Edit: есть еще несколько ответов на странице Reddit этого вопроса: http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

Answer 1

не может быть лучшим человеком, чтобы ответить на этот вопрос, как и реализовав Идрис я, вероятно, немного предвзято! Часто задаваемые вопросы - http://docs.idris-lang.org/en/latest/faq/faq.html - есть на что сказать, но немного расшириться:

Idris был разработан с нуля, чтобы поддерживать программирование общего назначения перед доказательством теоремы, и, как таковой, имеет функции высокого уровня, такие как как типы классов, обозначают обозначения, скобки идиомы, списки, перегрузки и т. д. Идрис ставит высокоуровневое программирование перед интерактивным доказательством, хотя, поскольку Идрис построен на тактическом разработчике, есть интерфейс с тактикой, основанной на интерактивной теоретической проверке (немного похожей на Coq, но не такой продвинутой, по крайней мере, пока).

Другое дело, что Идрис стремится хорошо поддерживать внедрение встроенных DSL. С Haskell вы можете пройти долгий путь с помощью обозначений, и вы тоже можете с Идрисом, но вы также можете перестроить другие конструкции, такие как привязка приложений и переменных, если вам нужно. Более подробную информацию об этом вы можете найти в учебнике или в полной информации в этой статье: http://www.cs.st-andrews.ac.uk/~eb/drafts/dsl-idris.pdf

Другое отличие в компиляции. Агда идет главным образом через Хаскелл, Идрис через С. Существует экспериментальный задний конец для Агда, который использует тот же задний конец, что и Идрис, через С. Я не знаю, насколько хорошо он поддерживается. Основной целью Idris всегда будет генерировать эффективный код - мы можем сделать намного лучше, чем мы сейчас делаем, но мы над этим работаем.

Системы типов в Агда и Идрисе довольно похожи во многих важных аспектах. Я думаю, что основное отличие заключается в обработке вселенных. У Агды вселенский полиморфизм, у Идриса есть cumulativity (и вы можете иметь Set : Set в обоих случаях, если вы считаете это слишком строгим и не против, что ваши доказательства могут быть необоснованными).

Answer 2

Еще одно отличие между Идрисом и Агдой состоит в том, что пропозициональное равенство Идриса является гетерогенным, а Агда - однородным.

Другими словами, предполагаемый определение равенства в Идриса будет:

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

а в Agda, это

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

л в Defintion Агда можно пренебречь, так как он имеет отношение к полиморфизму вселенной, о котором упоминает Эдвин в своем ответе.

Важным отличием является то, что тип равенства в Agda принимает два элемента A в качестве аргументов, тогда как в 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. Это совершенно разумное утверждение с гетерогенным равенством.