Learn Type Theory
I’ve been trying to write a blog post to this effect for a while now, hopefully this one will stick. I intend for this to be a bit more open-ended than most of my other posts, if you’re interested in seeing the updated version look here. Pull requests/issues are more than welcome on the repository. I hope you learn something from this.
Lots of people seem curious about type theory but it’s not at all clear how to go from no math background to understanding “Homotopical Patch Theory” or whatever the latest cool paper is. In this repository I’ve gathered links to some of the resources I’ve personally found helpful.
Reading Advice
I strongly urge you to start by reading one or more of the textbooks immediately below. They give a nice self-contained introduction and a foundation for understanding the papers that follow. Don’t get hung up on any particular thing, it’s always easier to skim the first time and read closely on a second pass.
The Resources
Textbooks
Practical Foundations of Programming Languages (PFPL)
I reference this more than any other book. It’s a very wide ranging survey of programming languages that assumes very little background knowledge. A lot people prefer the next book I mention but I think PFPL does a better job explaining the foundations it works from and then covers more topics I find interesting.
Types and Programming Languages (TAPL)
Another very widely used introductory book (the one I learned with). It’s good to read in conjunction with PFPL as they emphasize things differently. Notably, this includes descriptions of type inference which PFPL lacks and TAPL lacks most of PFPL’s descriptions of concurrency/interesting imperative languages. Like PFPL this is very accessible and well written.
Advanced Topics in Types and Programming Languages (ATTAPL)
Don’t feel the urge to read this all at once. It’s a bunch of fully independent but excellent chapters on a bunch of different topics. Read what looks interesting, save what doesn’t. It’s good to have in case you ever need to learn more about one of the subjects in a pinch.
Proof Assistants
One of the fun parts of taking in an interest in type theory is that you get all sorts of fun new programming languages to play with. Some major proof assistants are
Coq
Coq is one of the more widely used proof assistants and has the best introductory material by far in my opinion.
Agda
Agda is in many respects similar to Coq, but is a smaller language overall. It’s relatively easy to learn Agda after Coq so I recommend doing that. Agda has some really interesting advanced constructs like induction-recursion.
Idris
It might not be fair to put Idris in a list of “proof assistants” since it really wants to be a proper programming language. It’s one of the first serious attempts at writing a programming language with dependent types for actual programming though.
Twelf
Twelf is by far the simplest system in this list, it’s the absolute minimum a language can have and still be dependently typed. All of this makes it easy to pick up, but there are very few users and not a lot of introductory material which makes it a bit harder to get started with. It does scale up to serious use though.
Type Theory
The Works of Per Martin-Löf
Per Martin-Löf has contributed a ton to the current state of dependent type theory. So much so that it’s impossible to escape his influence. His papers on Martin-Löf Type Theory (he called it Intuitionistic Type Theory) are seminal.
If you’re confused by the papers above read the book in the next entry and try again. The book doesn’t give you as good a feel for the various flavors of MLTT (which spun off into different areas of research) but is easier to follow.
Programming In Martin-Löf’s Type Theory
It’s good to read the original papers and here things from the horses mouth, but Martin-Löf is much smarter than us and it’s nice to read other people explanations of his material. A group of people at Chalmer’s have elaborated it into a book.
The Works of John Reynold’s
John Reynold’s works are similarly impressive and always a pleasure to read.
Computational Type Theory
While most dependent type theories (like the ones found in Coq, Agda, Idris..) are based on Martin-Löf later intensional type theories, computational type theory is different. It’s a direct descendant of his extensional type theory that has been heavily developed and forms the basis of NuPRL nowadays. The resources below describe the various parts of how CTT works.
- Type Theory and its Meaning Explanations
- A Non-Type-Theoretic Definition of Martin-Löf’s Types
- Constructing a type system over operational semantics (Similar to the above, they’re helpful to read together)
- Equality in Lazy Computation System (of general interest)
- Naive Computational Type Theory
- Innovations in CTT using NuPRL
Homotopy Type Theory
A new exciting branch of type theory. This exploits the connection between homotopy theory and type theory by treating types as spaces. It’s the subject of a lot of active research but has some really nice introductory resources even now.
Proof Theory
Frank Pfenning’s Lecture Notes
Over the years, Frank Pfenning has accumulated lecture notes that are nothing short of heroic. They’re wonderful to read and almost as good as being in one of his lectures.
Category Theory
Learning category theory is necessary to understand some parts of type theory. If you decide to study categorical semantics, realizability, or domain theory eventually you’ll have to buckledown and learn a little at least. It’s actually really cool math so no harm done!
Category Theory for Computer Scientists
This is the absolute smallest introduction to category theory you can find that’s still useful for a computer scientist. It’s very light on what it demands for prior knowledge of pure math but doesn’t go into too much depth.
Category Theory
One of the better introductory books to category theory in my opinion. It’s notable in assuming relatively little mathematical background and for covering quite a lot of ground in a readable way.
Ed Morehouse’s Category Theory Lecture Notes
Another valuable piece of reading are these lecture notes. They cover a lot of the same areas as “Category Theory” so they can help to reinforce what you learned there as well giving you some of the author’s perspective on how to think about these things.
Other Goodness
Gunter’s “Semantics of Programming Language”
While I’m not as big a fan of some of the earlier chapters, the math presented in this book is absolutely top-notch and gives a good understanding of how some cool fields (like domain theory) work.
OPLSS
The Oregon Programming Languages Summer School is a 2 week long bootcamp on PLs held annually at the university of Oregon. It’s a wonderful event to attend but if you can’t make it they record all their lectures anyways! They’re taught be a variety of lecturers but they’re all world class researchers.