3 ms·

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-sc

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.

tel 12y ago
How would you feel about something like type theory : "computing" :: FOL : set theory where I mean to say "computing" as generally as you like.
- psygnisfive 12y ago
  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.
igravious 12y ago
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...
- psygnisfive 12y ago
  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

tel 12y ago

How would you feel about something like type theory : "computing" :: FOL : set theory where I mean to say "computing" as generally as you like.

psygnisfive 12y ago
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.

igravious 12y ago

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...

psygnisfive 12y ago
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