如何学习agda

Question

我在学习agda。但是，我遇到了问题。我在agda wiki上发现的所有教程对我来说都太复杂，涵盖了编程的各个方面。在平行阅读关于agda的3个教程之后，我能够编写简单的证明，但我仍然没有足够的知识将其用于真正的字算法正确性。

你能推荐我关于这个主题的任何教程吗？类似于学习你自己的Haskell，但对于Agda。

Answer 1

大约一年前，当我开始学习Agda时，我想我尝试了所有可用的教程，并且每次都教给我一些新的东西。

你或许应该给予勒柯克一试，因为它有一个更大的用户群，并有适用于它提供了两个漂亮的书：

1. Coq'Art - 有点过时，但初学者友好
2. Certified Programming with Dependent Types

Software Foundations也很好。

好的是，Agda和Coq基于的理论有点类似，所以很多例子都可以从一个翻译到另一个。 Programming in Martin-Löf's Type Theory是一个非常好的可读的介绍依赖型理论，它可以为你清除一些事情。

这将有助于了解“真实世界算法”的含义。 papers which mention Agda中描述了许多示例开发。

Answer 2

Conor McBride去年使用Agda进行了依赖型编程的a great series of lectures。如果你想从关于这个主题的简洁教程中解脱出来，这是一个很好的去处。我相信也有相应的练习。