我正在努力学习agda。但是，我遇到了一个问题。我在 agda wiki 上找到的所有教程对我来说都太复杂了，并且涵盖了编程的不同方面。在并行阅读了 3 篇关于 agda 的教程后，我能够编写简单的证明，但我仍然没有足够的知识来使用它来实现真实单词算法的正确性。
你能推荐我关于这个主题的任何教程吗？类似于 Learn Yourself a Haskell 但适用于 Agda 的东西。
问问题
5031 次
2 回答
23
当我大约一年前开始学习 Agda 时，我想我尝试了所有可用的教程，每个教程都教会了我一些新东西。
您可能应该尝试一下 Coq，因为它拥有更大的用户群，并且有两本不错的书籍可供使用：
- Coq'Art - 略显陈旧，但对初学者友好
- 具有依赖类型的认证编程
软件基础也很不错。
好消息是 Agda 和 Coq 所基于的理论有些相似，所以很多例子可以从一个翻译到另一个。使用 Martin-Löf 的类型理论编程是对依赖类型理论的一个非常好的和可读的介绍，它可以为你清楚一些事情。
了解“现实世界算法”是什么意思会有所帮助。在提到 Agda的论文中描述了许多示例开发。
于 2012-02-26T19:53:27.700 回答
18
Conor McBride去年就使用 Agda 进行依赖类型编程进行了一系列精彩的讲座。如果您想从阅读有关该主题的简洁教程中休息一下，这是一个不错的去处。我相信也有伴随的练习。
于 2012-11-05T15:13:50.147 回答