I’d like to learn more about type theory. Is there a book you’d recommend?
Please, list the intended audience level and/or prerequisites with your recommendations if any. I do coding for a living, but I would like to deepen my general CS degree with robust knowledge.
I’d like to be literate about concepts in TT and fluent in reasoning about TT problems.
I’d recommend starting with Types and Programming Languages by Benjamin Pierce. It’s an absolute classic and does a great job bridging the gap between theory and practice. It’s intended as an introductory graduate-level textbook, so the prerequisites include familiarity with programming in general and comfort with basic mathematical formalisms. Should be perfect for someone who codes for a living and is looking to deepen their theoretical knowledge.
+1 for that recommendation.
Types and Programming Languages is often advised, but I think it is more a reference than an introduction, and more about specific features of industrial type systems than about Type Theory itself. It describes, but it does not motivate. You could shuffle the chapters and it will be essentially the same book.
My alternative suggestion is Type Theory and Formal Proof: an Introduction by Rob Nederpelt and Herman Geuvers. It is indeed an introduction that made it easy for me to understand why type systems exist and what problems they can solve. Also, unlike Benjamin’s book, it goes all the way to dependent types.
The above mentioned are great books. If those are not enough then you might try:
If you are trying to study Type Theory in a context that is not dependent on computer programming, I’d recommend reading Type Theory and Formal Proof: An Introduction
The book is very fluent. It starts with untyped lambda calculus and then proceeds to go as far as lambda-D.
If you are trying to approach it in a more CS way, as others mentioned, Benjamin Pierce’s book is the one to go with.
also had suggested proofs and types, hadn’t seen jarors comment. Still +1.
One thing to think about is what you mean by “type theory” - there’s at least two meanings in common currency.
Some people use the term “type theory” to refer specifically to Per Martin-Löf’s intuitionistic type theory and (sometimes) the specific logical systems that descend from it. Or to dependent type theories that are broadly related, like the Calculus of Constructions, “book HoTT”, etc. Often, “learning type theory” will be taken to mean “learning to express mathematical objects, proofs, and programs in these systems”, or “learning the details of the metatheory of these systems”. In addition to the other books recommended here, Programming in Martin-Löf’s Theory by Nordström, Petersson, and Smith is a good (though dated and dry) reference that’s available for free online. If you want a really gentle introduction, you might also like The Little Typer (sorry for the shameless self-promotion). It also helps to pick up an implementation and start hacking - Software Foundations is great.
Others use the term “type theory” to refer to the general theoretical exploration of types and programming languages. For this, TaPL is still a great intro, as is Software Foundations. PFPL and PLFA are also worth exploring. I’d say that TaPL and PFPL really require you to have a certain amount of formal math background, at least corresponding to an undergrad discrete math class, and it’s hard to know if you’ve done the exercises right. The books based on a proof assistant make it much easier to know if you’ve understood things properly, as the computer corrects your homework.