Различия между Агда и Идрисом

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

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

Я смог заметить некоторые из них:

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

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

Ответы

Ответ 1

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

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

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

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

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

Ответ 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

l в определении Агды можно игнорировать, поскольку это связано с полиморфизмом Вселенной, о котором упоминает Эдвин в своем ответе.

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