I enjoyed Types and Programming Languages by Benjamin Pierce. Also vaguely related is the Implementation of Functional Programming Languages by Simon Peyton Jones (this is more about lambda calculus, but I found that when you pair type theory with lambda calculus you get some nice synergies as a programmer).