I’m quite serious about “if you don’t understand it, it’s a bug”. I’m not exactly experienced when it comes to teaching people about type theory, so if you’re not grokking something it’s likely my fault not yours. I’d hate for my incompetence to scare someone away from dependent types or type theory!
Please let me know so I can either help or send you a kitten as a consolation prize.
Would it be reasonable for people to describe what they didn’t understand in this comment thread so you can respond/edit?
Certainly. Also wrt our conversation last night, I’m trying to decide how to implement your suggestion, but I haven’t forgotten about it :)
I just want you to get feedback. :)
The article is actually quite good as we’ve already said on twitter :). It is just that people who are not already equipped with the theoretical baggage behind it may have to read it multiple times and find external links explaining to them what everything in the code does. The trick is to find the balance between theory/examples so that everybody gets it and that is the obvious goal of its author.
The nice thing about such articles is that they upgrade the collective knowledge of everybody involved (whether reading or writing them). I would definitely like to see more articles like this :)
Did you just introduce peano numbering and then define addition? (eg: 1+1 = 2 .. plus (S z) (Sz) = S (S z))
Maybe try and link to that as a reference ;)
Yeah I didn’t spend too much time on Nat, I’ll try to dig up a nicer reference on that than too quick sentences :) Thanks!