Learn Type Theory

Posted on August 14, 2015
Tags: types

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

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

Type Theory

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.

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.

John Reynold’s works are similarly impressive and always a pleasure to read.

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.

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

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!

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.

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.

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

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.

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.

comments powered by Disqus