Ash*_*ary 42 haskell scala agda dependent-type idris
有一个伊德里斯教程后,阿格达教程和许多其他的教程式的论文和介绍材料与永无止境的事情引用还得学习.我有种爬行在所有这些中间,大部分时间我坚持用数学符号和新的术语没有解释突然出现.也许我的数学很糟糕:-)
是否有任何有纪律的方法来处理依赖类型编程？就像当你想学习Haskell中,你开始与"教你一个Haskell",当你想了解斯卡拉,你开始Odersky的书,对Ruby你读与它的突变臭虫怪异的教程.但我不能用他们的书开始阿格达或伊德里斯.他们远远超过我的头脑.我试过Coq并且陷入了它的全部证明风格.Agda需要巨大的数学背景和伊德里斯,好吧,让我们暂时离开吧!
我非常了解静态类型系统,我对Scala非常熟练,如果有必要,我可以使用Haskell.我理解功能范例并且日复一日地使用它,我理解代数数据类型和GADT(实际上相当顺利),我最近成功地理解了Lambda Cube.不过,我缺乏数学和逻辑部分.
Dan*_*ton 29
我强烈推荐Software Foundations.这本书非常擅长一次向你介绍Coq.有许多定理证明,是的,但这是依赖类型的美味的一部分.当"编程"和"证明"之间的界限开始模糊时,这是一种很棒的感觉.
不过,我缺乏数学和逻辑部分.
我认为Software Foundations可以帮助您快速掌握您需要了解的逻辑.尽管如此,已经对蕴涵概念感到满意有所帮助.