Type Theory Resources for the Layprogrammer

Over the last few years, I’ve tried getting into type theory. I even thought I would apply to Ph.D. programs for a while. I ultimately didn’t, and while I was figuring that out I spent a lot of time struggling to grasp what type theory actually is. Even once I had some kind of clue, I struggled a lot with jargon, new symbols, and learning some useful background knowledge. About that last point: I realize one might not need to know set theory to understand type theory, but I found it useful. It was a lot easier for me to understand covariance and contravariance by looking at Venn diagrams than by reading the Wikipedia page.

The below (very incomplete) list of “resources” should hopefully help someone get started on their way to going from programming in Python to knowing what type theory is, like I did. If you find that any of this is incorrect, well, that probably means you’re past the need for this kind of post. If you have ideas for things to add, please reach out!

books:

• Introductory Discrete Mathematics
  • Chapter 0 is an introduction to set theory and logic, which are two topics I found repeatedly assumed as understood in type theory books and papers.
• Naive set theory
  • Referenced by at least “Introduction to Discrete Mathematics” and “Types and Programming Languages”. Haven’t read it, but… maybe someday.
• Category Theory for Programmers
  • I hear the words “monad” and “functors” a lot in PL theory. I think this book will help with that.
  • A git repo with code for the book is here.
• The Little Typer
  • An introduction into dependent type theory, building up from relatively modest beginnings.
  • Here’s a talk on dependent types by one of the authors from around the time the book came out.
• Type-driven Development in Idris
  • A really helpful look at dependent types by learning a dependently-typed language, Idris.
• Types and Programming Languages
  • This seems to me to be considered one of, if not the, foundational textbooks on type theory
• Practical Foundations of Programming Languages
  • Along with TAPL above, this seems to me to have an important place in type/programming language theory
• Programming Language Foundations in Agda
  • Honestly, the thing that kept me from continuing this was all the non-standard (to me) characters that I’d always forget how to type. Seems good though.

blog posts:

• Type inference
• How to implement dependent type theory (and some other posts tagged with “type theory” on that blog)

communities:

• ACM Special Interest Group on Programming Languages (SIGPLAN)
  • There are a number of good conferences put on by SIGPLAN and the workshops accompanying each conference are interesting! I attended PLMW a couple times when I was considering grad school
• Oregon Programming Languages Summer School (OPLSS)
  • I attended this as well, and while it was really helpful most of the material went way over my head.