Diferenças entre Agda e Idris

165

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/

serras
fonte
1
Você pode querer ter um olhar para aswel coq, a sintaxe não é de um milhão de milhas de distância de Haskell e tem fácil de classes tipo uso :)
4
Para constar: a Agda também possui notações monádicas e aplicativas atualmente.
Gallais

Respostas:

190

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).

Edwin Brady
fonte
49
O que você quer dizer com "... não é a melhor pessoa para responder ..."? Você é uma das melhores pessoas para responder, já que conhece Idris intimamente. Agora só precisamos responder ao NAD, e temos toda a imagem :) Obrigado por reservar um tempo para responder.
Alex R
9
Existe algum lugar onde eu possa ler mais sobre cumulatividade? Eu nunca tinha ouvido falar disso antes ...
serras 28/02
13
O livro de Adam Chlipala é provavelmente o melhor lugar:
Edwin Brady
8
O primeiro capítulo do livro HoTT também o descreve de maneira bastante clara, embora concisa.
David Christiansen
50

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.

David Christiansen
fonte
26
Você parece estar comentando mais sobre a biblioteca padrão da Agda do que a teoria subjacente da Agda, mas mesmo a biblioteca padrão contém igualdade homogênea e heterogênea ( cse.chalmers.se/~nad/listings/lib/… ). As pessoas tendem a usar o primeiro com mais frequência, sempre que possível. O último é equivalente a uma declaração de que os tipos são iguais, seguidos por um sobre os valores. Em um mundo em que a igualdade de tipos é estranha (HoTT), o heteq é uma afirmação mais estranha.
Mysterious Dan
6
Não entendo como essa afirmação é absurda sob igualdade homogênea. A menos que eu esteja enganado, (n + (m + o))e ((n + m) + o)seja julgadamente igual pela associatividade de +on (derivada do princípio da indução). Consequentemente, cada lado da igualdade tem o mesmo tipo. A diferença entre os tipos de igualdade é importante, mas não vejo como isso é um exemplo disso.
5
@Abhishek não é igualdade de julgamento o mesmo que igualdade de definição? Eu acho que você quer dizer (n + (m + o)) e ((n + m) + o) são proposicionalmente iguais, mas não definicionalmente / julgadores iguais.
Tom Crockett
3
certo. Eu quis dizer igualdade proposicional quando disse igualdade julgadora. Desculpe. Aqui está o comentário corrigido: (n + (m + o)) e ((n + m) + o) são proposicionalmente iguais, mas não definicionalmente iguais. Se você tiver a: A, a: B será retido apenas se A e B forem do tipo definicionalmente iguais. Para a decidibilidade da digitação, a igualdade de definição deve ser decidida. Nas teorias do tipo extensional, a igualdade definicional coincide com a igualdade proposicional e, portanto, a digitação é indecidível. Em Coq, a igualdade definicional inclui apenas computação, igualdade alfa e desdobramento definicional.
Abhishek Anand 28/03