Diferenças entre Agda e Idris

Estou começando a mergulhar na programação de tipo dependente e descobri que as linguagens Agda e Idris são as mais próximas de Haskell, então comecei por lá.

Minha pergunta é: quais são as principais diferenças entre eles? Os sistemas de tipos são igualmente expressivos em ambos? Seria ótimo ter um comparativo abrangente e uma discussão sobre benefícios.

Consegui identificar alguns:

• Idris tem classes de tipo à Haskell, enquanto Agda acompanha argumentos de instância
• Idris inclui notação monádica e aplicativa
• Ambos parecem ter algum tipo de sintaxe reconectável, embora não tenham muita certeza se são os mesmos.

Editar : existem mais respostas na página do Reddit desta pergunta: http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

Talvez eu não seja a melhor pessoa para responder a isso, como tendo implementado Idris, provavelmente sou um pouco tendenciosa! O FAQ - http://docs.idris-lang.org/en/latest/faq/faq.html - tem algo a dizer sobre isso, mas para expandir um pouco:

O Idris foi projetado desde o início para oferecer suporte à programação de uso geral antes da prova do teorema e, como tal, possui recursos de alto nível, como classes de tipos, notação, colchetes de idiomas, compreensão de listas, sobrecarga e assim por diante. Idris coloca a programação de alto nível à frente da prova interativa, embora, como o Idris seja construído em um elaborador baseado em tática, haja uma interface para um provador de teoremas interativos baseado em tática (um pouco como Coq, mas não tão avançado, pelo menos ainda não).

Outra coisa que Idris pretende apoiar bem é a implementação do DSL incorporado. Com o Haskell, você pode percorrer um longo caminho com a notação, e também com Idris, mas também é possível religar outras construções, como a aplicação e a associação de variáveis, se necessário. Você pode encontrar mais detalhes sobre isso no tutorial ou detalhes completos neste artigo: http://eb.host.cs.st-andrews.ac.uk/drafts/dsl-idris.pdf

Outra diferença está na compilação. A Agda passa principalmente por Haskell, Idris por C. Há um back-end experimental para a Agda que usa o mesmo back-end que Idris, por C. Não sei o quão bem ele é mantido. O principal objetivo de Idris será sempre gerar código eficiente - podemos fazer muito melhor do que atualmente, mas estamos trabalhando nisso.

Os sistemas de tipos em Agda e Idris são bastante semelhantes em muitos aspectos importantes. Eu acho que a principal diferença está na manipulação de universos. A Agda tem polimorfismo no universo, Idris tem cumulatividade (e você pode ter Set : Setnos dois se achar isso muito restritivo e não se importar que suas provas possam não ser verdadeiras).

Outra diferença entre Idris e Agda é que a igualdade proposicional de Idris é heterogênea, enquanto a da Agda é homogênea.

Em outras palavras, a suposta definição de igualdade em Idris seria:

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

enquanto estiver na Agda, é

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

O l na definição de Agda pode ser ignorado, como tem a ver com o polimorfismo do universo que Edwin menciona em sua resposta.

A diferença importante é que o tipo de igualdade no Agda aceita dois elementos de A como argumentos, enquanto no Idris ele pode aceitar dois valores com tipos potencialmente diferentes .

Em outras palavras, em Idris, pode-se afirmar que duas coisas com tipos diferentes são iguais (mesmo que isso acabe sendo uma reivindicação improvável), enquanto na Agda, a própria afirmação é um absurdo.

Isso tem conseqüências importantes e abrangentes para a teoria dos tipos, especialmente no que diz respeito à viabilidade de trabalhar com a teoria dos tipos de homotopia. Para isso, a igualdade heterogênea simplesmente não funciona porque requer um axioma inconsistente com o HoTT. Por outro lado, é possível afirmar teoremas úteis com igualdade heterogênea que não podem ser declaradas diretamente com igualdade homogênea.

Talvez o exemplo mais fácil seja a associatividade da concatenação de vetores. Dadas as listas indexadas em comprimento chamadas vetores definidos da seguinte forma:

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

e concatenação com o seguinte tipo:

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

podemos querer provar que:

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

Essa afirmação não faz sentido sob igualdade homogênea, porque o lado esquerdo da igualdade tem tipo Vect (n + (m + o)) ae o lado direito tem tipo Vect ((n + m) + o) a. É uma afirmação perfeitamente sensata com igualdade heterogênea.