What's Type Theory and how's it different from Set Theory and 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
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.
type theory : "computing" :: FOL : set 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....
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.
Wikipedia and Google are quick ways to answer most kinds of "what is X?" questions.