Comment by shadowfox

While that is an excellent book, I would say that it focuses on type theory from a somewhat more theoretical perspective than (say) TAPL which is more on type _systems_ from a programming languages perspective. Both are great reads though.