4 ms·

What's the difference between type theory and category theory? How are they related?

• mbid 9y ago
  People think of type theory as "internal language" of categories with certain properties (e.g. simply typed typed type theory for cartesian closed categories). A formal way to say this is that the syntax of type theory gives rise to category with certain properties, and this category is initial among such categories. This means that it is, in a sense, the minimal category that satisfies these properties, so that all constructions in type theory give rise to this construction in every such category. To me personally, type theory feels a little like an ugly definition of this initial "category with X", and I'm currently exploring in my thesis whether a syntax derived from the categorical definitions itself could also be used for the same purpose as type theory is today.
• vladsotirov 9y ago
  Originally, categories arose as (mathematical) descriptions of various universes of functions. For example, there is universe of functions that are given linear functions (i.e. matrices), which is contained in the universe of functions given by polynomial expressions, which is itself contained in the universe of functions given by rational expressions (i.e. fractions of polynomials). If you've studied calculus other example are also universes of analytic functions, of smooth functions, of differentiable functions, and of continuous functions. Significantly these are not just single-variable functions, or even functions whose values are real numbers; all that is necessary to describe a category is for functions to have specified domains and codomains and that any two functions with matching source and target can be composed into a third function by feeding the target of one into the source of the other, subject to the condition that composition is associative (it doesn't matter in what order you pipe the functions together), and for any object there is an identity function with from the object to itself, meaning a function which does nothing when composed with another function. It turned out that the above axiomatization of how functions behave (i.e. that they have sources and targets and can be composed in an associative fashion) is very flexible. For example, you can essentially implement the category of linear maps (between finite-dimensional spaces) as the category whose "functions" are matrices, with source and target given by the numbers of rows or columns, and whose composition is given by matrix multiplication. Note in particular that matrices are just tables of numbers, i.e. they are not actually functions, and that the sources and targets are not the spaces themselves, but just their dimensions. The relationship with type theory comes about as follows. The fundamental object of type theory is the type judgement "if a term x is known to be type X, and a term t is known to be of type T, then a term p(x,t) is known to be of type P". But the term p(x,t) can be understood as a function transforming a pair of terms of types T and X to a term of type P. The type judgment is then the validation that the expression p(x,t) determines a legitimate function (in the context of the specific type theory). Hence in this way, each type theory can be understood as being a syntactic presentation of a specific category of functions.