如何学习Agda

Question

32

我正在尝试学习Agda，但遇到了问题。我在Agda维基上找到的所有教程都对我来说过于复杂，并涵盖了不同方面的编程。在阅读三个Agda教程的同时，我能够写一些简单的证明，但我仍然没有足够的知识将其用于实际算法正确性。

你可以推荐一些关于这个主题的教程给我吗？类似于Learn Yourself a Haskell但是针对Agda。

- Konstantin Solomatov

相关问题（稍后提出）：https://dev59.com/EGYr5IYBdhLWcg3wqr7o#14292455 - user1972140

不是Agda而是Idris，但仍然非常相关：https://vimeo.com/117221082 - Erik Kaplun

3个回答

20

Conor McBride去年在使用Agda进行依赖类型编程方面进行了一系列精彩的讲座。如果你想从枯燥的教程中休息一下，这是一个不错的去处。我相信还有相应的练习。

- Necrototem

2

链接已经失效，但是Conor McBride在2017/18年有一系列新的讲座。 - Jo Liss

2

以下是2022年的一些额外资源。

Agda编程语言基础：该书以“软件基础”为风格，但使用Agda代替Coq编写。作者曾使用“软件基础”进行授课，并写了一个说明解释为什么决定用Agda重写这本书。
PLFA笔记：这是一套评论PLFA的笔记。作者还写了一本备受好评的书籍...
逻辑与计算交织：虽然不是Agda书籍，但首先通过编写自己的小型证明助手（使用Racket编写）介绍了证明助手。该书还包含有关Agda的部分内容。
学习Agda：这是一篇较短的文章，但有助于浏览。

- jimmy

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- wjedynak · Accepted Answer

大约一年前，我开始学习Agda时，我尝试了所有可用的教程，并从中学到了新东西。

你可能应该尝试Coq，因为它有更大的用户群体，并且有两本不错的书可供选择：

值得注意的是，Agda和Coq所基于的理论有些相似，因此许多示例可以从一个转化到另一个。 Martin-Löf的类型论编程是一个真正不错且易读的依赖类型理论入门介绍，可以让你理解一些概念。

如果您能说明“真实世界算法”是什么将会很有帮助。许多在提到Agda的论文中描述了示例开发。