Como aprender Agda

Question

Estou tentando aprender agda.No entanto, tive um problema.Todos os tutoriais que encontrei no agda wiki são muito complexos para mim e cobrem diferentes aspectos da programação.Após a leitura paralela de 3 tutoriais sobre agda, consegui escrever provas simples, mas ainda não tenho conhecimento suficiente para usá-las para corrigir algoritmos de palavras reais.

Você pode me recomendar algum tutorial sobre o assunto?Algo semelhante a Learn Yourself a Haskell, mas para Agda.

Answer 1

Quando comecei a aprender Agda, há cerca de um ano, acho que tentei todos os tutoriais disponíveis e cada um me ensinou algo novo.

Você provavelmente deveria dar uma chance ao Coq, porque ele tem uma base de usuários maior e há dois bons livros disponíveis para ele:

1. Coq'Art - um pouco desatualizado, mas adequado para iniciantes
2. Programação Certificada com Tipos Dependentes

Fundações de software também é muito legal.

O bom é que as teorias nas quais Agda e Coq se baseiam são um tanto semelhantes, então muitos exemplos podem ser traduzidos de um para outro. Programação na Teoria dos Tipos de Martin-Löf é uma introdução muito boa e legível à teoria dos tipos dependentes, pode esclarecer algumas coisas para você.

Ajudaria saber o que você quer dizer com "algoritmos do mundo real".Muitos exemplos de desenvolvimentos são descritos em artigos que mencionam Agda.

Answer 2

Conor McBride deu Uma grande série de palestras No ano passado em programação digitada por dependência usandoAGDA.É um bom lugar para ir se você quer uma pausa de derramar através de tutoriais com tópicos.Eu acredito que também existem exercícios de acompanhamento.