So you want to learn type theory
purelytheoretical.com
purelytheoretical.com
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!
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/11typetheoryversussettheory
Category 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.
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.
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.
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....
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
type theory : "computing" :: FOL : set theory
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
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
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)
----
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
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.
Wikipedia and Google are quick ways to answer most kinds of "what is X?" questions.
http://www.cs.cmu.edu/~rwh/plbook/book.pdf
Harper'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.
The more common practical uses are:
1) If you're using a statically typed language, knowing some basic TT will let you understand the hows and whys of its type system. This is especially true of static langs that have richer type systems, like Haskell.
2) Rich type systems actually help you program! a lot of people complain that type systems merely complain when you mess up -- which is helpful, because you now know you've messed, but not completely helpful because it feels like the types don't help you. The truth is,, this is mostly true only of BAD type systems.
A GOOD type system can guide you to the right answer by making the number of possible programs very tiny. Instead of infinitely many programs, there might just be one or two.
A GOOD type system can guide you to the right answer by making it possible for the computer to write parts of the program for you because the types make it obvious what the options are at any moment program construction.
For specific examples, you'd have to look around. I don't have any offhand (nor am I trying to convince you to learn TT!). Conal Elliot and Edward Kmett no doubt have plenty of good examples, or could tell you who does.
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.
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.
It's all pretty much exactly the same as done in academic type theory for decades.
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".
Pierce 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.
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.
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.
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.
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 ***
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
Goal: B * A
Context:
p : A * B
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
Goal: B * A
Context:
x : A
y : B
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)
swap :: A * B -> B * A
swap (x , y) = (y , x)
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
listInduction A P n c [] = n
listInduction A P n c (x :: xs) = c x xs (listInduction A P n c xs)
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!
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.