从哪里开始依赖类型编程？
有一个伊德里斯教程，Agda教程和许多其他教程式样的论文和介绍性材料，永无止境的参考资料可供学习。 我在所有这些中间爬行，大部分时间我都被数学符号和新术语突然出现而没有解释。 也许我的数学很糟糕:-)
是否有任何有纪律的方法来进行依赖型编程？ 就像你想要学习Haskell一样，你从“教你自己一个Haskell”开始，当你想学习Scala时，你从Odersky的书开始，对于Ruby，你会看到那个奇怪的教程，其中有变异的错误。 但我无法用他们的书开始Agda或Idris。 他们高于我的头。 我尝试了Coq并陷入了它所有关于te-test的风格。 阿格达需要一个巨大的数学背景和伊德里斯，好吧，让我们暂时离开！
我非常了解静态类型系统，我对Scala很熟练，如果需要，我可以使用Haskell。 我理解Functional Paradigm并日复一日地使用它，我理解代数数据类型和GADT（实际上相当顺利），并且最近我设法理解了Lambda Cube。 虽然我缺乏数学和逻辑部分。
我强烈推荐软件基金会。 本书很好地向您介绍Coq一步一个脚印。 有很多定理证明，是的，但这是依赖类型美味的一部分。 当“编程”和“证明”之间的界限开始模糊时，这是一种很棒的感觉。
虽然我缺乏数学和逻辑部分。
我认为Software Foundations在帮助您了解您需要了解的逻辑方面做得非常好。 虽然已经对蕴涵的概念感到满意。
（注意：这是一个自我广告）
我正在写Agda教程，我的主要目标是让人们在没有理论背景的情况下玩Agda。
本教程可能会解决您的大部分问题：
它正在开发中，但上半年已经准备就绪。
链接地址: http://www.djcxy.com/p/43347.html