Where to start with dependent type programming?

 

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.

(Notice: This is a self advertisement)

I am writing an Agda tutorial and my primary goal is to let people to play with Agda without theoretical background.

This tutorial may solve most of your problems:

  • tries to explain Agda programming without outer references
  • requires only secondary school mathemtaics
  • tries to teach programming practices also

    • It is under development, but the first half is kind of ready.

    链接地址: http://www.djcxy.com/p/43348.html

    上一篇: 有限制类型的语言吗？

    下一篇: 从哪里开始依赖类型编程？