So you want to learn type theory

Time is a limited resource. As much as I'd love to learn everything that I find interesting, I can't find the time to learn all these subjects. The criteria I use to decide when to learn something or not are not like geoka9's, but I still have to ask myself why.

Why does it hurt to ask why? Asking yourself why is also a means of learning.

There are so many interesting things to learn, and they're all readily accessible to us. I find myself discovering a new fascinating subject I'd love to learn about each day, and by now the list of fascinating things has grown unmanageable. Asking "why?" can be a good means to to make sense of such a list.

At a younger age, I was able to sustain great focus and effort on learning something without ever asking myself why. This approach helped me earn a doctoral degree on an obscure, esoteric topic without ever stopping to ask why. I assure you, I personally wish I'd asked why.

Years later, I continue to enjoy learning. But since there are so many things to learn, I have the choice of learning many things superficially (the default when something new catches my interest daily), or really digging in and learning something in depth. At this stage in my life, with many things competing for my time and attention, learning something in depth requires considerably more motivation. And (for me) having an answer to "why?" helps me sustain that motivation.

Type theory is a sort of axiomatisation of mathematical structures that is similar to (but not identical to: http://dl.acm.org/citation.cfm?id=512927.512938) set theory. As chas mentions (https://news.ycombinator.com/item?id=8780786), a lot of the modern mathematical perspective on type theory is via homotopy type theory.

Category theory is another such axiomatisation.

As with any pair of sufficiently powerful axiomatisations, any one of them can be formalised in any other of them, more or less naturally; for example, here's an n-category café hit when I Googled "category theory + type theory": https://golem.ph.utexas.edu/category/2013/03/category_theory....

Yeah, that's a great book for learning how the methodology of type theory and judgemental presentations can be used in presenting practical/everyday PL concepts.

Incidentally, I spoke with bob and he mentioned he wants to write another book some day that does the same thing, but for "pure" type theory. I think that'd be a great book, particularly given bob's unique perspective on type theory (having spent a lot of time on both sides of the fence—proof theory vs realizability). but don't count on it anytime soon!

I want to disagree a little bit with chas here and just say that type theory as we know it today emerged out of a different, post-computer tradition than old-school Russellian type theory. Modern type theory comes arguably from Martin-Löf and the FP domain.

As for what is type theory vs. set theory vs. category theory, I'd put it this way: type theory is a flavor of proof theory built on computational justification of inference rules and patterns of reasoning. But that's maybe a bit boring sounding, so another way to think of it is, type theory is a framework for thinking about what makes sense in a strongly typed programming language. Most PLs with types just throw types in as an afterthought, whereas a type theoretic perspective says, start with the types, use the types to express what you want the programming language to do, and the lambda calculus that you get from this is your programming language.

What sets it apart from set theory is that type theory is much more about inference and justification. Set theory is more a theory about sets, where you presuppose these things exist and have properties (membership, etc.) that you want to capture and reason about. Type theory, on the other hand, is a way of thinking about how to invent new sorts of things, and a tool for reasoning in and of itself. You reason about sets using some logic, type theory is a logic.

Something similar is true about category theory as well, only for a different sort of thing (whereas sets are defined by membership, etc. categories are defined by objects and maps, etc.)

A good analogy, I would argue, is this:

    type theory : set theory/CT  ::  mathematics : physics

One is a general framework of reasoning, inference, proof, etc. the other is a domain that you apply it to. It's not a perfect analogy for all the obvious reasons, but thats roughly how I'd suggest you think about it. When you do your set theory, you take for granted all the stuff like conjunction, implication, quantification, etc. just as the language you use to talk about sets. With type theory, you're looking at those very linguistic constructs.