Diferencias entre Agda e Idris

Estoy empezando a sumergirme en la programación de tipo dependiente y descubrí 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 tipos son igualmente expresivos en ambos? Sería genial tener una comparación exhaustiva y una discusión sobre los beneficios.

He podido 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 rebaddable, aunque no estoy realmente seguro de si son iguales.

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

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

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

Otra cosa que Idris pretende apoyar bien es la implementación de DSL incorporado. Con Haskell, puede obtener un largo camino con la notación do, y también con Idris, pero también puede volver a unir otras construcciones, como la aplicación y el enlace de variables, si es necesario. Puede encontrar más detalles sobre esto en el tutorial, o detalles completos en este documento: http://eb.host.cs.st-andrews.ac.uk/drafts/dsl-idris.pdf

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

Los sistemas de tipos 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 universal, Idris tiene acumulatividad (y puede tenerlo Set : Seten ambos si lo encuentra demasiado restrictivo y no le importa que sus pruebas puedan ser poco sólidas).

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 que 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 puede ignorarse, 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 se puede afirmar que dos cosas con diferentes tipos son iguales (incluso si termina siendo una afirmación no demostrable), mientras que en Agda, la afirmación misma no tiene sentido.

Esto tiene consecuencias importantes y de gran alcance para la teoría de tipos, especialmente con respecto a la viabilidad de trabajar con la teoría de tipos 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 se pueden establecer directamente con igualdad homogénea.

Quizás el ejemplo más fácil es la asociatividad de la concatenación de vectores. Dadas listas indexadas por longitud llamadas vectores definidos de esta 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

podríamos querer 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 tipo Vect (n + (m + o)) ay el lado derecho tiene tipo Vect ((n + m) + o) a. Es una declaración perfectamente sensata con igualdad heterogénea.