larrλtheliquid -> Lemma the Ultimate
Agda course update
Status quo
I just finished chapter 3 and am starting on chapter 4 in the Agda course. Chapters 0 & 1 starts off nice and light, giving an introduction to the course. One very nice feature of chapter 1 is a gradually built up explanation of dependent types in context of more familiar monomorphic and polymorphic static typing in languages like Java, C++, and Haskell. Chapter 2 changed abruptly to explaining what reduction systems are, but don’t be deterred! Although the relation to dependent types is not clear in chapter 2, chapter 3 explains the untyped and simply typed lambda calculi. In these chapters you’ll see that a given lambda calculus can be modeled as a reduction system where T is the set of lambda terms, and beta-reduction (along with alpha-conversions) constitutes the binary relation. Although a lot of complex sounding words are used (beta-redex, beta-reduct, etc.), the underlying concepts are not that complicated. More importantly, chapter 3 ends in explaining the Curry-Howard isomorphism and what it looks like in Agda. At this point I prefer Agda’s approach of a unified system using types for everything, compared to Guru’s split between terms/types and proofs/formulae with respect to operators and syntax. Note that after finishing chapter 3 you should be able to to watch the University of Oregon Logic and Theorem Proving summer school intro video and be comfortable with all the material.
Next up
I’m going to continue reading the remainder of the course slides. Between what I’m learning in this course and what I’ve learned from the Guru book I think I’ll be able to write a good intro to dependent types post for those that do not wish to read the more theoretical material. More importantly, I have an incomplete draft post that I’m very excited about. The purpose of the post is to explain what dependent typing (and theorem proving therein) is in the context of dynamic typing, static typing, Test-driven development, and program verification in general. I’ll probably wait until I’m finished with the Agda course publishing these two. The second post especially could be an understandable and sensible reference to give to industry programmers so I’d like to get the argument right. That’s all for now, see you again soon!