如何学习agda

Question

我正在努力学习agda。然而，我有一个问题。我在agda wiki上找到的所有教程对我来说都太复杂了，涵盖了编程的不同方面。在并行阅读了agda上的3个教程后，我能够写出简单的证明，但我仍然没有足够的知识来使用它来验证真实的算法正确性。

你能给我推荐一些关于这个主题的教程吗？类似于学习Haskell的东西，但用于Agda。

Answer 1

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

您可能应该尝试一下Coq，因为它有一个更大的用户群，并且有两本很好的书可供选择：

1. Coq'Art -略显过时，但初学者friendly
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去年向a great series of lectures介绍了使用Agda的依赖类型编程。如果你想从关于这个主题的简明教程中解脱出来，这是一个很好的去处。我相信也有配套的练习。