Yeah, that's a great book for learning how the methodology of type theory and judgemental presentations can be used in presenting practical/everyday PL concepts.

Incidentally, I spoke with bob and he mentioned he wants to write another book some day that does the same thing, but for "pure" type theory. I think that'd be a great book, particularly given bob's unique perspective on type theory (having spent a lot of time on both sides of the fence—proof theory vs realizability). but don't count on it anytime soon!