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

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



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



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




  • Идрис классов типа а-ля Хаскель, в то время как Agda идет с аргументами экземпляра

  • Идрис включает в себя монадические и прикладные обозначения

  • у обоих из них, похоже, есть какой-то повторно связываемый синтаксис, хотя и не совсем уверен, что они одинаковы.



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

367   2  

2 ответов:

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

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

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

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

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

161  
2018-03-09 21:21:22

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

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

важным отличием является то, что тип равенства в Agda принимает два элемента A в качестве аргументов, в то время как в Idris он может принимать два значения с потенциально разные типы.

это имеет важные и широкие последствия для теории типов, особенно в отношении возможности работы с теорией гомотопических типов. Для этого гетерогенное равенство просто не будет работать, потому что оно требует аксиомы, несовместимой с Хоттом. С другой стороны, можно сформулировать полезные теоремы с гетерогенным равенством, которые не могут быть прямо сформулированы с однородным равенством.

пожалуй, самый простой пример-ассоциативность векторного конкатенации. Заданные индексированные по длине списки называются векторами, определенными таким образом:

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

42  
2014-01-08 12:02:05

Comments

    Ничего не найдено.
Click here to cancel reply.