How to learn agda

Question

I am trying to learn agda. However, I got a problem. All the tutorials which I found on agda wiki are too complex for me and cover different aspects of programming. After parallel reading of 3 tutorials on agda I was able to write simple proofs but I still don't have enough knowledge to use it for real word algorithm correctness.

Can you recommend me any tutorials on the subject? Something similar to Learn Yourself a Haskell but for Agda.

Answer 1

When I started learning Agda about a year ago I think I tried all available tutorials and each taught me something new.

You should probably give Coq a try, because it has a larger user base and there are two nice books available for it:

1. Coq'Art - slightly dated, but beginner friendly
2. Certified Programming with Dependent Types

Software Foundations is also very nice.

The nice thing is that the theories Agda and Coq are based on are somewhat similar, so many examples can be translated from one to another. Programming in Martin-Löf's Type Theory is a really nice and readable introduction to the dependent type theory, it can clear some things for you.

It would help to know what do you mean by "real world algorithms". Many example developments are described in papers which mention Agda.

Answer 2

Conor McBride gave a great series of lectures last year on dependently-typed programming using Agda. It's a good place to go if you want a break from pouring through terse tutorials on the topic. I believe there are also accompanying exercises.