从哪里开始依赖types编程？
有一个伊德里斯教程，Agda教程和许多其他的教程风格的论文和介绍性材料，永无止境的参考事物还没有学习。 我在这些中间爬行，大部分时间我都被math符号和新术语突然出现，没有任何解释。 也许我的math糟透了:-)
有没有任何有纪律的方法来进行依赖型编程？ 就像你想要学习Haskell一样，你从“自学一个Haskell”开始，当你想学习Scala的时候，你从Odersky的书开始，对于Ruby来说，你会看到那个奇怪的教程，里边有变异的bug。 但是我不能用他们的书来启动Agda或Idris。 他们高于我的头。 我尝试了Coq，并陷入了所有关于TeX的certificate风格。 阿格达需要一个巨大的math背景和伊德里斯，好吧，让我们暂时离开！
我非常了解静态types系统，我对Scala非常熟练，如果需要，我可以使用Haskell。 我理解function范式并日复一日地使用它，我理解代数数据types和GADT（实际上相当顺利），而且我最近设法理解了Lambda Cube。 虽然我缺乏math和逻辑部分。
我会强烈推荐软件基础 。 这本书很好地介绍你一次一个的Coq。 有很多定理certificate，是的，但这是依赖types的美味的一部分。 当“编程”和“certificate”之间的界线开始模糊时，这是一种很棒的感觉。
虽然我缺乏math和逻辑部分。
我认为Software Foundations在帮助您了解您需要知道的逻辑方面做得相当不错。 虽然已经对蕴涵的概念感到舒服。
（注意：这是一个自我广告）
我正在写Agda教程 ，我的主要目标是让人们在没有理论背景的情况下玩Agda。
本教程可能会解决您的大部分问题：
- 试图解释没有外部引用的Agda编程
- 只需要中学的Mathemtaics
- 也试图教授编程实践
正在开发中，但上半年已经准备好了。
