Intense study of type systems and type theory

I want to understand the actual theory behind types rather than just learning about the latest practical change made in some existing language (e.g., not just how Haskell or Scala's type system works).

What is the best way to pick up this background?

Solution

Type theory is a big area. First of all, the term "types" is a kind of a misnomer in computer science, for a few reasons, even though they are mostly used for the same basic idea. Types have arisen in many contexts, philosophy, computer science, and mathematics, for mostly the same reasons. The origin of types in mathematics comes from trying to formalize set theory and running into nitty paradoxes, though similar paradoxes arise in computer science. (For example, I like to point to Girard's paradox on this one).

The way you probably interpret types at the current moment is an idea that became popular throughout the 70s-90s in computers: types are a lightweight flow insensitive analysis that allow us to make concise logical guarantees about the programs we write. Types can be used for this, but you can actually take them all the way out to encoding higher order logic, where programs are proofs. Once you go here, you can take a proof, extract the computational component, and turn it into a program which computes a "correct" result (with respect to the theorem you proved).

There are a few roads you can take from here:

Grab yourself a copy of Ben Pierce's Types and Programming Languages. This is the book to read, and one of the best books in computer science. It covers the theory for why we need types, and how we can use them to enforce constraints about our programs!
Learn a language where you use types on a regular basis to enforce things about the program semantics. In particular, you can learn OCaml, Haskell, or Agda. Haskell seems to be the best choice at the moment, it's got quite a few extensions that make it really attractive, and a really active user community. In fact, it's very common that results published at top conferences flow to widespread use in the community within only a few years!
Learn to use a theorem prover based on a constructive type theory. In my opinion, this is the only real way to grok the real issues behind type theory. There are a number of good options, though Coq and Isabelle stand out as the real contenders now. Coq has one great advantage: Ben Pierce also has a book that covers it! Software Foundations covers an amount of theory from Programming Languages in depth, and you really get to prove things using it.

You might also want to look into a few related fields:

Category theory is the math that tends to underlie this stuff. For example, it's possible to take a categorical interpretation to (co-)inductive datatypes given in these languages.
Logic. Learning a bit of good old traditional logic can be helpful, though I feel confident that most of what you need can be picked up from reading through Ben Pierce's SF book. However, there is still lots of reference to older systems (sequent calculus and natural deduction).
Learn about the Haskell community! They are moving quickly, as I said, and ask deep questions about types in computer science.
Great Works in Programming Languages has a number of great articles!

There are a few great recommendations I have for learning beyond this, but I'd definitely start with Ben Pierce's books (I've never really gotten into the follow up book "advanced topics in types and computer science," but that's also perhaps interesting to you). In particular, I remember the Handbook of Automated Reasoning having a great article on high order type theory.

P.s., I'm convinced that the answer to this question is concretely, "get a PhD. in programming languages, philosophy, or logic..." ;-)