Diferencias entre Agda e Idris

type-theory

Question

Estoy comenzando a bucear en la programación de tipos dependientes y he descubierto que los idiomas Agda e Idris son los más cercanos a Haskell, así que comencé allí.

Mi pregunta es: ¿cuáles son las principales diferencias entre ellos? ¿Los sistemas de tipo son igualmente expresivos en ambos? Sería genial tener una comparación completa y una discusión sobre los beneficios.

Pude detectar algunos:

• Idris tiene clases de tipo a la Haskell, mientras que Agda va con argumentos de instancia
• Idris incluye notación monádica y aplicativa
• Ambos parecen tener algún tipo de sintaxis rebindable, aunque no están muy seguros de si son los mismos.

Editar : hay algunas respuestas más en la página de Reddit de esta pregunta: http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

Answer 1

Otra diferencia entre Idris y Agda es que la igualdad proposicional de Idris es heterogénea, mientras que la de Agda es homogénea.

En otras palabras, la definición putativa de igualdad en Idris sería:

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

mientras está en Agda, es

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

El l en la definición de Agda se puede ignorar, ya que tiene que ver con el polimorfismo del universo que Edwin menciona en su respuesta.

La diferencia importante es que el tipo de igualdad en Agda toma dos elementos de A como argumentos, mientras que en Idris puede tomar dos valores con tipos potencialmente diferentes .

En otras palabras, en Idris uno puede afirmar que dos cosas con diferentes tipos son iguales (incluso si termina siendo un reclamo indemostrable), mientras que en Agda, la misma declaración es una tontería.

Esto tiene consecuencias importantes y de amplio alcance para la teoría de tipos, especialmente con respecto a la viabilidad de trabajar con la teoría del tipo de homotopía. Para esto, la igualdad heterogénea simplemente no funcionará porque requiere un axioma que es inconsistente con HoTT. Por otro lado, es posible establecer teoremas útiles con igualdad heterogénea que no pueden establecerse de manera directa con igualdad homogénea.

Quizás el ejemplo más fácil es la asociatividad de la concatenación vectorial. Dadas listas indexadas de longitud llamadas vectores definidas de la siguiente manera:

data Vect : Nat -> Type -> Type where
  Nil : Vect 0 a
  (::) : a -> Vect n a -> Vect (S n) a 

y concatenación con el siguiente tipo:

(++) : Vect n a -> Vect m a -> Vect (n + m) a

es posible que deseemos probar que:

concatAssoc : (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) ->
              xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

Esta afirmación no tiene sentido bajo igualdad homogénea, porque el lado izquierdo de la igualdad tiene el tipo Vect (n + (m + o)) a y el lado derecho tiene el tipo Vect ((n + m) + o) a . Es una declaración perfectamente sensata con igualdad heterogénea.

Answer 2

Puede que no sea la mejor persona para responder a esto, ya que al haber implementado Idris, ¡probablemente soy un poco parcial! Las preguntas frecuentes - http://docs.idris-lang.org/en/latest/faq/faq.html - tienen algo que decir al respecto, pero para ampliarlo un poco:

Idris ha sido diseñado desde cero para soportar la programación de propósito general antes de la demostración de teoremas, y como tal tiene características de alto nivel como clases de tipo, notación, paréntesis idiomáticos, listas de comprensión, sobrecarga, etc. Idris pone la programación de alto nivel por encima de la prueba interactiva, aunque debido a que Idris se basa en un elaborador basado en táctica, hay una interfaz para un probador de teoremas interactivo basado en táctica (un poco como Coq, pero no tan avanzado, al menos no todavía).

Otra cosa que Idris pretende apoyar es la implementación Embedded DSL. Con Haskell puedes hacer un largo camino con la notación do, y también puedes hacerlo con Idris, pero también puedes volver a enlazar otras construcciones como la aplicación y el enlace variable si es necesario. Puede encontrar más detalles al respecto en el tutorial, o los detalles completos en este documento: http://www.cs.st-andrews.ac.uk/~eb/drafts/dsl-idris.pdf

Otra diferencia está en la compilación. Agda va principalmente a través de Haskell, Idris vía C. Hay un back-end experimental para Agda que utiliza el mismo back end que Idris, a través de C. No sé qué tan bien conservado está. Un objetivo principal de Idris siempre será generar código eficiente; podemos hacerlo mucho mejor de lo que lo hacemos actualmente, pero estamos trabajando en ello.

Los sistemas tipo en Agda e Idris son bastante similares en muchos aspectos importantes. Creo que la principal diferencia está en el manejo de universos. Agda tiene polimorfismo en el universo, Idris tiene cumulativity (y puede tener Set : Set en ambos si esto le resulta demasiado restrictivo y no le molesta que sus pruebas no sean correctas).