从哪里开始依赖类型编程？ [英] Where to start with dependent type programming?

问题描述

有一个Idris教程，一个Agda教程和许多其他教程风格的论文和介绍性材料，永无止境地提及尚未学习的东西。我在所有这些中间爬行，大部分时间我都被数学符号和新术语突然出现而没有解释。也许我的数学很糟糕： - ）

是否有任何有纪律的方法来处理依赖类型编程？就像你想要学习Haskell一样，你从教你自己一个Haskell开始，当你想学习Scala时，你从Odersky的书开始，对于Ruby，你会看到那个奇怪的教程，其中有变异的错误。但我无法用他们的书开始Agda或Idris。他们高于我的头。我尝试了Coq并陷入了它所有关于te-test的风格。 Agda需要一个巨大的数学背景和Idris，好吧，我们暂时离开吧！

我非常了解静态类型系统，我对Scala很熟练，我可以如有必要，使用Haskell。我理解Functional Paradigm并日复一日地使用它，我理解代数数据类型和GADT（实际上相当顺利），并且最近我设法理解了Lambda Cube。虽然我缺乏数学和逻辑部分。

解决方案

我强烈建议软件基金会。本书很好地向您介绍Coq一步一个脚印。有很多定理证明，是的，但这是依赖类型美味的一部分。当编程和验证之间的界线开始模糊时，这是一种很棒的感觉。

我缺乏数学和逻辑部分，但是。

我认为Software Foundations在帮助您了解您需要了解的逻辑方面做得非常好。虽然已经对隐含概念感到满意，但是。

There is an Idris tutorial, an Agda tutorial and many other tutorial style papers and introductory material with never ending references to things yet to learn. I'm kind of crawling in the middle of all these and most of the time I'm stuck with mathematical notations and new terminology appearing suddenly with no explanation. Perhaps my math sucks :-)

Is there any disciplined way to approach dependent type programming? Like when you want to learn Haskell, you start with "Teach yourself a Haskell", when you want to learn Scala, you start with Odersky's book, for Ruby you read that weird tutorial with mutated bugs in it. But I can't start Agda or Idris with their books. They are way above my head. I tried Coq and got stuck in its all-about-teorm-proving style. Agda requires a huge math background and Idris, well, let's leave that for now!

I understand static type systems very well, I am kind of proficient with Scala and I can use Haskell if necessary. I understand the Functional Paradigm and use it day to day, I understand Algebraic Data Types and GADTs (quite smoothly actually) and I recently managed to comprehend the Lambda Cube. I'm lacking in the math and logic parts, though.

解决方案

I would highly recommend Software Foundations. This book is quite good at introducing you to Coq one step at a time. There is a lot of theorem proving, yes, but that's part of the deliciousness of dependent types. It's a great feeling when the line between "programming" and "proving" starts to blur.

I'm lacking in the math and logic parts, though.

I think Software Foundations does a pretty good job of bringing you up to speed for the logic you need to know. Already being comfortable with the concept of implication helps, though.

这篇关于从哪里开始依赖类型编程？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！