44

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.

Vitus
  • 11,822
  • 7
  • 37
  • 64
Ashkan Kh. Nazary
  • 21,844
  • 13
  • 44
  • 68

2 Answers2

30

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.

csl
  • 10,937
  • 5
  • 57
  • 89
Dan Burton
  • 53,238
  • 27
  • 117
  • 198
22

(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.

  • Would be nice to have an RSS feed for it so that one can be notified about updates. Maybe use a blog? – Kim Stebel Jan 15 '13 at 13:44
  • @KimStebel, I would like to have full control on the presentation, so I prefer not to write it as a blog. I plan to release the source in darcs, which may help to follow the changes. –  Jan 15 '13 at 18:19
  • As long as you use your own template, you have all the control over the presentation you want. Please post the URL of the repo here. – Kim Stebel Jan 15 '13 at 19:48
  • @KimStebel, the URL is http://hub.darcs.net/divip/AgdaTutorial/ –  Jan 23 '13 at 13:59
  • @KimStebel, sorry for no feeds. If you cannot watch the repo then I made something wrong. Can't you? –  Jan 23 '13 at 14:33
  • I don't see any way to watch it. I am logged in. How am I supposed to do it? – Kim Stebel Jan 23 '13 at 14:35
  • On the left there is "files" and "changes", so you can browse either by file or patches. What do you see? –  Jan 23 '13 at 14:39
  • 1
    I meant "watch" as it's used on github. It means you get change notifications. I can view the files and commits just fine. – Kim Stebel Jan 23 '13 at 14:49
  • @PéterDiviánszky I've been working through this and it's the best resource I've found so far! – user833970 Aug 07 '13 at 23:29
  • upvoted! it explains every part of every line. e.g. "`data Bool : Set where true : Bool false : Bool` Interpretation: Bool is a Set; true is a Bool; false is a Bool; there is nothing else which is Bool; true and false are different. – sam boosalis Apr 26 '14 at 22:46