Hi Isaac,
I've read (parts of) the book as well. I'm not too fond of it. It is
probably one of the only books that explains type theory for
functional programmers - which is great of course. Unfortunately, I
read through most of it and could not shake the feeling that I wasn't
really learning anything. It somehow doesn't always convey the "joy
of type theory" (well, for my personal taste at least).
Other background reading you might be interested in include:
Programming in Martin-Lofs Type Theory. Available from:
http://www.cs.chalmers.se/Cs/Research/Logic/book/
http://www.amazon.co.uk/Lectures-Curry-Howard-Isomorphism-Foundations-
Mathematics/dp/0444520775/ref=sr_1_2/026-1815313-5521242?
ie=UTF8&s=books&qid=1176630898&sr=8-2
Lecture notes on the Curry-Howard Isomorphism.
A bit technical, but contains just about everything you'll ever need
to know.
I also found it instructive to familiarize myself with other proof
assistants based on dependent types. You might want to look into Coq,
for instance. It's a very mature and well-documented system. The
Coq'Art book is a great place to start.
Hope these comments help,
Wouter
