43

有一个 Idris 教程、一个 Agda 教程和许多其他教程风格的论文和介绍性材料，其中不断引用尚未学习的东西。我有点在所有这些中间爬行，而且大多数时候我都被数学符号和突然出现的新术语所困，没有任何解释。也许我的数学很烂:-)

是否有任何规范的方法来处理依赖类型编程？就像当你想学习 Haskell 时，你从“自学 Haskell”开始，当你想学习 Scala 时，你从 Odersky 的书开始，对于 Ruby，你阅读那个带有变异错误的奇怪教程。但我不能从他们的书开始 Agda 或 Idris。他们在我的头上。我尝试了 Coq 并陷入了它的所有关于 teorm 证明的风格。Agda 需要大量的数学背景，而 Idris，好吧，让我们暂时离开吧！

我非常了解静态类型系统，我精通 Scala，如有必要，我可以使用 Haskell。我了解函数范式并每天使用它，我了解代数数据类型和 GADT（实际上非​​常顺利），并且我最近设法理解了 Lambda Cube。不过，我缺乏数学和逻辑部分。

4

2 回答 2

30

我强烈推荐Software Foundations。这本书非常适合一次一步地向您介绍 Coq。有很多定理证明，是的，但这是依赖类型美味的一部分。当“编程”和“证明”之间的界限开始模糊时，这是一种很棒的感觉。

不过，我缺乏数学和逻辑部分。

我认为 Software Foundations 在让您快速了解您需要了解的逻辑方面做得非常好。不过，已经熟悉暗示的概念会有所帮助。

于 2012-11-21T17:30:33.877 回答
22

（注意：这是一个自我广告）

我正在写一个Agda 教程，我的主要目标是让人们在没有理论背景的情况下使用 Agda。

本教程可能会解决您的大部分问题：

  • 试图解释没有外部引用的 Agda 编程
  • 只需要中学数学
  • 也尝试教授编程实践

它正在开发中，但前半部分已经准备就绪。

于 2013-01-12T10:32:29.993 回答