type-systems - 如何学习 Agda

Question

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

你能给我推荐一些关于这个主题的教程吗？类似于 Learn Yourself a Haskell 但适用于 Agda。

Answer 1

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

您或许应该尝试一下 Coq，因为它拥有更大的用户群，并且有两本不错的书籍可供使用:

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 中描述了许多示例开发。 .