So you want to learn type theory 169 points by psygnisfive on Dec 21, 2014 | hide | past | web | favorite | 47 comments

 Good list, I'd also recommend http://www.cs.cmu.edu/~rwh/plbook/book.pdf for something designed for newcomers to the field
 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!
 What's Type Theory and how's it different from Set Theory and Category Theory?
 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.
 This is what I don't get... _Why_ is 'type' theory _a logic_? A type is an enumeration of values (terms), right? What's that got to do with truth values and how they may be manipulated? I've read some of the papers/texts you posted in that tremendously helpful summary (thanks by the way!) and talking about type theory always segues into talking about logic. If you could explain that _one_ thing I'd be so happy. To me, type theory seems like set theory done right...
 Ahh this is a very good question.. I'll give two answers, the first more philosophical and the second more example-driven, and both hesitant, 'cause I'm not sure anyone's really thought about deeper why's like this much. :)1:My first answer is, because of the nature of what a logic is. Logics are systems for reasoning about some problem domain, or put it another way, logics are ways of convincing yourself that you're justified in believing a judgment (`A is true`, `B is a proposition`, `C is tasty`).What this means is that, to have a proof `M` which proves a judgment `J`, is to have some piece of data which you can look at. So all proofs are some kind of data, in the same way that all novels and all movies are some kind of data.A harder question is why all data is a kind of proof and that's more subtle. Some people actually want to say they're not, proofs are just a special kind of data, while others want to just say to loosen the notion of proof and proposition. I don't think there's a good answer for this direction.2:My second answer is, it turns out they couldn't be anything else! Consider the inference rule (written in natural English):`````` if you know A is true and you know B is true then you can conclude A&B is true `````` which tells you when you can make the judgment `A&B is true`. When you use this rule, you have to supply two justifications of the premises `A is true` and `B is true`. That is, you have to provide two pieces of evidence, two proofs, one for each premise.Now consider this description of how to make pairs:`````` if you have M of type A and you have N of type B then you can make (M,N) of type A*B `````` Here we're just describing how pairs are formed: you take two things, and stick them together with a constructor to form a new piece of data.Now I ask you, what are you doing when "proving A&B" if not taking two things (two smaller proofs of `A` and `B`) and sticking them together to form a new piece of data (the proof of `A&B`)? I would argue you're not doing ANYTHING different. The act of proving a conjunction is just the same as the act of making a pair!Now do this for other logical connectives:`````` proving a disjunction is just the same as giving an element of a tagged union proving an implication is just the same as giving a function proving the trivial proposition is just giving a 0-length tuple proving the absurd proposition (which is impossible) is just giving a void-type value (which is impossible) `````` So why are type theories a logic? Well just look!----Now, I should say, this connection does not mean that all logics are type theories! Type theory has a very specific view of how inference rules are justified, by appeal to certain principles which turn out to be computational in nature.Why these principles should be so powerful as computational principles, I don't know. It's a mystery. Maybe God is a type theorist? ;p
 Thank you for taking the time to reply to me.I would like to continue this conversation with you but here is not the correct space/place. I will join the group on IRC and I hope to catch you there.
 How would you feel about something like`````` type theory : "computing" :: FOL : set theory `````` where I mean to say "computing" as generally as you like.
 Thats also an appropriate analogy, I think. The main point is, type theory is a tool for reasoning, while set theory is a thing reasoned about. At least in the context of foundational questions. You can flip them, but then it becomes kind of silly, imo.
 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....
 Type theory is a framework for doing logic that predates computers as we know them. If you have used first-order predicate logic before (e.g. ∀x∀y(P(f(x))→¬(P(x)→ Q(f(y),x,z)))), it performs a similar role to type theory and is the same sort of mathematical thing, it just has different properties. Logical frameworks are interesting to programmers and computer scientists because logical systems and programming languages/computation are related through the Curry-Howard correspondence. http://math.stackexchange.com/questions/166430/curry-howard-...This[1] isn't a perfect description of type theory in general because it is aimed at a particular branch of type theory called homotopy type theory, but I feel like it does a pretty good job of explaining the differences between type theory and set theory and what motivated those differences. [1]http://planetmath.org/11typetheoryversussettheoryCategory theory is a particularly abstract part of abstract algebra primarily concerned with extremely general mathematical structures. It concerns itself with identifying and understanding the core structures common to a large number of mathematical objects and operations such as the one shared by multiplication, the cartesian product, least common multiple, logical conjunction (&&), and structs (or record types) in programming. This structure is usually referred to as the categorical product.Category theory is often brought up when discussing type theory because there is a close relationship between these sorts of abstract structures like the one linking structs and conjunction and the structures that are described by type theory. In general, there is a close relationship between type theories and certain types of categories so you can learn interesting things about type theory from studying category theory and vice versa, but category theory contains many things which are not primarily useful for or associated with type theory.
 > It concerns itself with identifying and understanding the core structures common to a large number of mathematical objects and operations such as the one shared by multiplication, the cartesian product, least common multiple, logical conjunction (&&), and structs (or record types) in programming. This structure is usually referred to as the categorical product.This sounds more like universal algebra (http://www.encyclopediaofmath.org/index.php/Universal_algebr...) than category theory, which, almost by definition, is interested in studying structure-preserving morphisms, without too much attention to exactly what structure is being preserved.
 Category theory is about categories,. One notion which makes sense in the context of a category is the categorical product (http://en.wikipedia.org/wiki/Product_%28category_theory%29). All the examples given are examples of categorical products within suitable categories [e.g., Cartesian product within the category of sets and functions between them (amounting to multiplication of cardinals, if one just cares about the action on objects), least common multiple within the category of positive integers ordered by divisibility (a partial ordering being just a special kind of category), logical conjunction within the category of truth values (which can be thought of as sets with at most one element), and structs or record types in the category whose objects are the types of your favorite programming language and morphisms are the programs between them].
 Certainly, I didn't mean to imply that you (EDIT: I mean chas) were wrong, just that it didn't feel like the examples that you brought up were in the 'spirit' of category theory. As I mentioned in a sister comment (https://news.ycombinator.com/item?id=8780829), any sufficiently powerful formalisation can encode any other (proof: definition of 'sufficiently powerful'), so that there is no mathematical structure of which it can be said definitively that it is not an instance of category theory—but that doesn't mean that every structure should be so viewed!For example, to pick on the lcm example (just because it's the one that caught my attention): as you mention, posets are automatically categories, but I don't think that the theory of posets is best viewed as a part of category theory; and, similarly, the product is just a special case of the limit over a discrete category, but I don't think that describing the least common multiple, say, as a limit will be educational to anyone! By contrast, viewing the lcm as part of an unusual algebraic structure on the natural numbers I think can be instructive.
 I absolutely think it's instructive to view the LCM as a specific case of meets in a semilattice, and in turn to view these as specialization of a general theory of categorical products. (Why wouldn't it be instructive? If you like, the "unusual algebraic structure" on the natural numbers which might be worth considering is that of a category with products). And I also think that recognition of such analogies and general patterns ubiquitous across mathematics is a large part of the spirit of category theory.
 http://en.m.wikipedia.org/wiki/Type_theoryWikipedia and Google are quick ways to answer most kinds of "what is X?" questions.
 I am interested to hear about practical application of type theory and how it helped solve real world software and hardware problem better.
 Thank you for the thoughtful response!
 dons' suggestion, which I heartily second, is somewhat aimed at practical type theory:http://www.cs.cmu.edu/~rwh/plbook/book.pdfHarper's thesis is that type theory is the backbone for language design. When you read his book you see him elaborate this and show how it applies to understanding and designing practical languages that work right.
 Nice!
 Ask yourself why.You want to do CS, prove theorems, do theoretical research? Then, by all means, go for it!It's hip and you use a functional language to write software? Well... It's probably just a whim. But sure, give it a try.
 No, don't ask yourself why. Just learn. It's one human activity that never requires a reason
 What I meant is it would be impractical to pick one special topic of CS to study just because it happens to be a mode of the day.It's like deciding to study number theory ("because, you know, cryptography!") in isolation instead of following a sensible math curriculum ("I'm not particularly interested in math") and learning the discipline as it was meant to be learned.In short, I can't think of a "type system specialist" who is not a computer scientist. It sounds sort of like a "loop specialist" who can't program, or a "forehand specialist" who can't play tennis.
 Type theory specialists outside of CS usually fit under the banner of "Logician". Thats why they go under your radar :)
 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.
 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.
 no, don't do this. you have limited time focus what you learn just like everything else
 To be clear, most theoretical computer science research is not type theory. Not even close to it either.
 Even most PL research is not type theory; it is its own field.
 Well, of you want do implement a type system it could help too.
 The academic type theory mentioned in this post is not really terribly important to implementing type systems for general purpose languages. There's this growing divide between the engineering discipline of type systems in general languages and the pure theory people who seem only interested in theorem provers and constructive math.
 This is really not true at all. Unless what you mean by "implementing type systems for general purpose languages" is a sort of weak, generally useless type system that punishes rather than helps.This is ESPECIALLY false of Pfenning and co's work, which is aimed specifically at understanding how to apply type theoretic techniques to the design of PLs, so that you get a PL with exactly the sort of stuff you want.I added a link to the page to PFPL, which is an entire book on how to implement programming languages using type theoretic tools. It even has sections on OO programming, if you're into that sort of thing. It's all the same toolkit, in the end.
 So where did Java generics come from, then? Or pretty much anything in Scala? Or Rust or C++11 lambdas or Swift?It's all pretty much exactly the same as done in academic type theory for decades.
 It really isn't. Take a good long look at Java generics and ask yourself if they really came straight out of type theory research. They didn't, that's why they're so botched, and why Odersky wanted a do-over with Scala :]More seriously, Scala and Rust are the only things in your list that would actually claim to be influenced by academia. I'm sure Apple is not going for the type theorists with Swift, despite having some mildly interesting type structures like sum types, and C++'s "lambdas" obviously have very little to do with type theory, unless you want to make the very weak claim of "anything that has anything to do with the lambda calculus = type theory".
 One of the primary major players with generics in Java is Philip Wadler, a type theorist and one of the co-creators of Haskell. Generics comes straight out of type theory research, and normally its called parametric polymorphism, but mainstream programmers can't handle that funky terminology. Apple's work on Swift has openly acknowledge its debt to Haskell and contemporary work on type theory, and it shows. As for the rest, you'd have to ask the people who worked on them.At any rate, C++, Scala, Rust, Java.. these are not languages that take type theory very seriously, and probably couldn't. It's certainly true that the popular imperative languages don't take TT seriously.But so what? The comment was about general purpose languages, and type theory is demonstrably of use in implementing them. Just because most mainstream languages don't use type theory doesn't make that not true. It just means most mainstream languages do not make use of everything they could.Oh well. Their loss.
 Re Java generics: Nope. They came out of UPenn's featherweight java work, see here: http://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdfPierce literally wrote the book on type theory.Swift is written by type theorists; large chunks of the people who worked on it has a PhD (or part of one) in PL theory.
 I just finished writing a tiny sexp based lambda interpreter, and was thinking of adding some restricted type inference and checking on top of it. Timing.
 So I think you're right that you should have a good reason. Fashion isn't enough. Don't learn TT cause its "cool", that would be stupid.For FP, tho.. I would say that you'll be a better functional programmer by knowing TT, even if you don't have a typed language. And if you do have a typed language, you'll want to understand your type system, so learning TT gives you the tools to do that properly.But there's more than just that. Types offer a lot to the programmer from a practical perspective. Forget the whole thing about using types to prove your code works. You can do that, you can do certified programming if you want. Learn Coq, it's great for that. But types offer you something else:`````` *** types help you figure out what the right program is *** `````` This is something that is often ignored or overlooked, but it's very important. Conor McBride (who's work you might want to look into once you know some TT) talks about this a lot.A relatively trivial, but easy-to-understand example of this would be the simple programming problem of writing a program that can take a pair of type `A * B` (where `` is the pair product) and return a pair of type `B A`. That is, the flips its argument's elements around. Ok this is simple and we all know what the program is, right, but let's do a little programming in Agda to see how types help you here.We'll start with a type declaration for the function, and the LHS of an equation that defines the function:`````` swap :: A * B -> B * A swap p = {! !}0 `````` Notice I put in this funny thing `{! !}0`. This is called a "hole": it's a part of the program that's missing. The 0 indicates its identity (this is hole 0). If we put the cursor in the hole, we can ask Agda to tell us about the hole, and it'll reply:`````` Goal: B * A Context: p : A * B `````` The goal is the type of the value we have to supply for the hole, the context is all the variables in scope, together with their types.Now, still with the cursor in the hole, we can ask Agda to pattern match on `p` and split the equation into as many patterns as it can. Because we have types, Agda knows all of the constructors that a type has, so it can automatically fill in the patterns for us. Since pairs have only one constructor, we simply get a slightly more complicated equation:`````` swap :: A * B -> B * A swap (x , y) = {! !}0 `````` Now let's again ask Agda about the hole:`````` Goal: B * A Context: x : A y : B `````` Notice: `p` is gone, because we matched on it, and instead we have `x` and `y`, new variables binding the elements of the pair, and their types.Now let's ask Agda to try filling in the hole a little bit. We can tell Agda to refine the hole, and because it knows the goal is a pair type, and pairs have exactly one constructor, it can chose that constructor to fill in part of the program for us:`````` swap :: A * B -> B * A swap (x , y) = ({! !}1 , {! !}2) `````` Now we have two new holes, with goal types B and A respectively, and the same contexts as before. We can again ask Agda to work on these holes, and it will fill in:`````` swap :: A * B -> B * A swap (x , y) = (y , x) `````` And we're done, we have a definition. And notice: the only code we wrote was to specify the type of `swap`, and put in an initial equation. The rest of the program came from Agda looking at the types, and then doing stuff based on that. This is a simple example, but it's exemplary of the "conversational" back and forth between the programmer and the type checker that you can get in a strongly typed program, where the types can actually help you FIND the right program.Just as another more obnoxious example, here's the the type for an induction principle for lists (also called dependently typed "fold", or dependently typed "reduce", or whatever):`````` listInduction : (A : Set) (P : List A -> Set) -> P [] -> (forall (x : A) (xs : List A) -> P xs -> P (x :: xs)) -> forall (xs : List A) -> P xs listInduction A P n c xs = {! !}0 `````` You can do the same thing as before, button mashing until you have no more holes, with this, and you get the right answer. In fact, there are exactly two right answers, and you can get both depending on a choice of which mashing you do. At no point do you actually have to figure out yourself that the following program is a solution:`````` listInduction A P n c [] = n listInduction A P n c (x :: xs) = c x xs (listInduction A P n c xs) `````` because the type FORCES that to be one of only two solutions. This kind of ability to button-mash and get a correct solution has actually lead people to compare dependently typed programming to playing a video game.The moral is: with strong types, the types HELP you, rather than smack you on the knuckles when you've messed up. So there really is something beyond just fashion and whim. It's actually practical!
 Reminds of how in basic physics, knowing the units of the result you're looking for helps you find the correct answer.Eg : if you're computing a speed ( m/s), then you'd better divide something that has a distance unit by something that has a time unit.
 Yep, that's a perfect analogy. And people have actually used type systems to formalize the concept of units. :)
 Understanding the general ebb and flow of construction/induction is such a powerful technique for thinking about FP. Any time I'm stuck programming now my two questions are (1) do I have the right data available and, then, (2) what things should I be inducting over?