5 ms·

What's Type Theory and how's it different from Set Theory and Category Theory?

by Pyret 12y ago

chas 12y ago
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-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/11typetheoryversussettheory 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.
- JadeNB 12y ago
  > 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_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.
  - Chinjut 12y ago
    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 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].
    - JadeNB 12y ago
      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 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.
      - throwaway_99837 12y ago
        I think you should not attach yourself emotionally to whether a certain perspective is "educational" or "instructive" to anyone. Rather, look at both perspectives in a [detached] clinical manner as just things that are.
JadeNB 12y ago
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 http://dl.acm.org/citation.cfm?id=512927.512938) set theory. As chas mentions (https://news.ycombinator.com/item?id=8780786 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_in_homotopy_ty.html https://golem.ph.utexas.edu/category/2013/03/category_theory....
psygnisfive 12y ago
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.
mkramlich 12y ago
http://en.m.wikipedia.org/wiki/Type_theory http://en.m.wikipedia.org/wiki/Type_theory Wikipedia and Google are quick ways to answer most kinds of "what is X?" questions.

What's Type Theory and how's it different from Set Theory and Category Theory?

by Pyret 12y ago

What's Type Theory and how's it different from Set Theory and Category Theory?

chas 12y ago

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-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/11typetheoryversussettheory 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.

JadeNB 12y ago
> 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_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.
- Chinjut 12y ago
  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 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].
  - JadeNB 12y ago
    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 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.
    - throwaway_99837 12y ago
      I think you should not attach yourself emotionally to whether a certain perspective is "educational" or "instructive" to anyone. Rather, look at both perspectives in a [detached] clinical manner as just things that are.

JadeNB 12y ago

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 http://dl.acm.org/citation.cfm?id=512927.512938) set theory. As chas mentions (https://news.ycombinator.com/item?id=8780786 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_in_homotopy_ty.html https://golem.ph.utexas.edu/category/2013/03/category_theory....

psygnisfive 12y ago

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.

mkramlich 12y ago

http://en.m.wikipedia.org/wiki/Type_theory http://en.m.wikipedia.org/wiki/Type_theory Wikipedia and Google are quick ways to answer most kinds of "what is X?" questions.