8
$\begingroup$

The subtleties of the correspondence between type theory and category theory are outside my ken. However, by my naive understanding of the relationship between the two historically convergent disciplines, the latter entirely subsumes the former. If this is so, can the language and formal/graphical descriptions used by category theorists replace those of type theorists? And should they (e.g., in pedagogy and academic publishing)?

Different formalisms can inspire novel perspectives and lay bare conceptual connections that might otherwise be obscure. However, a multiplicity of dialects probably also limits the size of a receptive audience, and, should a polyglot approach be taken, the length and complexity of exposition is compounded.

If category theory does subsume type theory, should the dialectical differences of the two disciplines be retained, and if so, why? For the sake of historical or cultural value? To retain different but salient differences of instructional or theoretical emphasis? What might these be?

$\endgroup$
  • 1
    $\begingroup$ Which type theory? Is this specifically the Type Theory Russel came up with? Or Martin-Lof Type Theory? Or Homotopy Type Theory, which seems to include types and category theory? I'm not certain there is a single "type theory". $\endgroup$ – jmite Aug 25 '17 at 22:53
  • 2
    $\begingroup$ @jmite There isn't a single "type theory" (though there is a field), but there are connections between many possible specific type theories and category theory. Indeed, at this point I would say it would be a bit suspicious if a type theory didn't have some connections to category theory. $\endgroup$ – Derek Elkins Aug 26 '17 at 4:23
  • 2
    $\begingroup$ I'd tend to regard a type system as a proof system for a logic: the entailment is an RE relation, terms/types are formulae, etc. We can establish normalization, consistency, ... at this level. This also has some strong connections with programming languages theory. Then, categories are used to build models for that logic. This is very enlightening, but if we looked at category/models only, we'd forget an important part, I think. STLC is easier to understand than generic CCCs. System F is simpler than dinatural transformations. Seeing both sides, and connecting them, is very nice. $\endgroup$ – chi Aug 26 '17 at 9:02
  • 1
    $\begingroup$ This is part of what we usually call Curry-Howard-Lambek isomorphism. $\endgroup$ – xuq01 Aug 26 '17 at 14:22
  • 1
    $\begingroup$ @chi, what "important part" might be forgotten if category theory (or model theory) were used exclusively instead of type theory? Also, why do you say STLC and System F are easier to understand than CCCs and dinatural transformations? Are the former systems simpler because of customary use or greater specificity or some other reason? $\endgroup$ – Polytope Aug 29 '17 at 21:53
9
$\begingroup$

Since you say that "the subtleties of the correspondence between type theory and category theory are outside your ken", perhaps the best way to understand the correspondence is to read non-technical expositions on the topic. I can recommend two:

  1. Steve Awodey, From Sets to Types, to Categories, to Sets, In: Sommaruga G. (eds) Foundational Theories of Classical and Constructive Mathematics. The Western Ontario Series in Philosophy of Science, vol 76. Springer, Dordrecht (free preprint here)

  2. Robert Harper's blog post The Holy Trinity, and also see these slides.

I suppose, the lesson to take away is that each approach has something to offer and that they work best together, and not so much if you try to replace or subsume one with the other.

$\endgroup$
  • $\begingroup$ May I ask, though, what distinctive advantages each approach offers? $\endgroup$ – Polytope Aug 29 '17 at 21:42
  • $\begingroup$ Andrej Bauer, thank you for the link to Awodey's paper. Awodey describes some interesting advantages of type theory: (1) "Type theory [is more manageable because it] has something of a concrete, 'nominalistic' [systematically generated] character." (2) "By contrast, [with] the purely structural approach of category theory, it can be harder to give an invariant proof." However, these advantages listed are still fairly vague. Could you possibly elaborate upon them or provide examples demonstrating this comparative utility of type theory? $\endgroup$ – Polytope Aug 30 '17 at 4:21
  • $\begingroup$ The advantages are vague because this is a non-technical paper comparing the practices of type theory, category theory and set theory. I could not possibly elaborate on them, as there is no way to instill in anyone the experiences of having worked in these areas for years by showing an example or two. Moreover, I do not really want to do it because this whole post has a definite "my math is better than your math" feeling, and I don't want to participate in it. $\endgroup$ – Andrej Bauer Aug 30 '17 at 19:32
  • $\begingroup$ Andrej Bauer, you're a professional mathematician, so I'm sure many other projects deserve your finite time and attention more than this. However, this really was an earnest question. I'm barely even an amateur, so of course everyone else's math is better than mine, but I was hoping the cs.stackexchange community might help me better understand why, when alternatives might be possible, type theory was anything other than a vestige of the historical development of the study of logic and programming languages. I'm sorry that I've offended you. $\endgroup$ – Polytope Aug 30 '17 at 20:55
  • $\begingroup$ I am not at all offended! And I respect your request. But I felt it would be dishonest and impolite of me to just ignore you. I prefer to give you a straight answer. I cannot invest the time to try to answer you because that would require writing a rather long exposition of questionable value. I would have to know a lot about your background to target it right. As you say, this is a community. Perhaps someone can answer in my place, that would be great. $\endgroup$ – Andrej Bauer Aug 30 '17 at 22:13
9
$\begingroup$

My view is more or less similar to chi's. I see category theory as (roughly) being to type theory what model theory is to logic. Some of the consequences of that are, first, each can exist autonomously. Indeed, type theory predates category theory, and the creation of category theory was not motivated by these concerns. Second, many of the distinctions category theory/model theory are purposely trying to blur are of primary interest in type theory/logic.

As a very basic example, all presentations of the axioms of a group give rise to the same class of models (namely groups). From the perspective of universal algebra, a variety (in the universal algebra sense, or a finitary algebraic category from a CT perspective) forgets its presentation. Meanwhile, from the perspective of equational logic, presentation is all there is. A primary computational topic here is E-unification which operates entirely at the level of equational logic, i.e. presentation.

This is typical. We say the simply typed lambda calculus (with products) (STLC) is the internal language of Cartesian closed categories, but it is really just one presentation of the internal language and not even the most "direct" one. The Categorical Abstract Machine (CAM) is arguably a more "direct" representation. Even with the STLC, the arrows of corresponding syntactic category are $\beta\eta$-equivalence classes of lambda terms! (But see this.) So either we somehow directly describe the syntactic category as a mathematical structure whose hom-sets just happen to coincide with $\beta\eta$-equivalance classes of STLC terms and have no computational content, or we need to already understand the STLC external to category theory, or we need to talk instead of presentations of Cartesian closed categories which, taking a fairly natural approach, will lead to something CAM-like. In the last case, equality of arrows becomes something like an E-unification problem. Understanding and simplifying this process as well as placing the more ergonomic facade of the STLC in front of it, requires techniques that are the bread and butter of logic and type theory but are not particularly natural within category theory.

A massively over-simplified picture that may nevertheless give a better idea of how category theory and type theory interrelate is the following. You can imagine them as two dimensions. The tools, techniques, and notations of type theory are geared toward moving vertically between different presentations of the same object, meanwhile the tools, techniques, and notations of category theory and geared toward moving horizontally between different mathematical objects. You might even say that a category is a whole vertical line and that category theory talks about moving one vertical line to another but not how the points of the two lines correspond. In this picture, category theory is not even capable of talking about the distinctions type theory is making, but this is intentional because it means that the arbitrarily complicated mapping of points on one vertical line to points on another is just irrelevant to what category theory cares about and can be ignored.

In my blog post, Category Theory, Syntactically, I describe an approach that makes category theory look more like type theory (rather than the other way around). Unsurprisingly, what I'm really discussing there are presentations of categories. Further, you can see aspects of normalization enter the picture, e.g. in my discussion of "product theories", even though this is not a focus at all of that particular post.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.