有一个 Idris 教程、一个 Agda 教程和许多其他教程风格的论文和介绍性材料,其中不断引用尚未学习的东西。我有点在所有这些中间爬行,而且大多数时候我都被数学符号和突然出现的新术语所困,没有任何解释。也许我的数学很烂:-)
是否有任何规范的方法来处理依赖类型编程?就像当你想学习 Haskell 时,你从“自学 Haskell”开始,当你想学习 Scala 时,你从 Odersky 的书开始,对于 Ruby,你阅读那个带有变异错误的奇怪教程。但我不能从他们的书开始 Agda 或 Idris。他们在我的头上。我尝试了 Coq 并陷入了它的所有关于 teorm 证明的风格。Agda 需要大量的数学背景,而 Idris,好吧,让我们暂时离开吧!
我非常了解静态类型系统,我精通 Scala,如有必要,我可以使用 Haskell。我了解函数范式并每天使用它,我了解代数数据类型和 GADT(实际上非常顺利),并且我最近设法理解了 Lambda Cube。不过,我缺乏数学和逻辑部分。