16
$\begingroup$

I have a basic working knowledge of category thoery since I do research in programming languages and typed lambda-calculus. Indeed, I have refereed many papers in my area based on category theory.

But, in doing this refereeing, and in reading many important categorial papers in my area, I simply find the terminology and presentation style extremely opaque compared to style that I prefer which instead emphasizes logic inference rules and extensions of the lambda calculus.

Given the (extended) Curry-Howard Isomorphism between programming languages, logics, and categories, it's clear that I can understand the concepts I need by mapping category theory into the other two. But, am I missing something in the process, or are the papers I'm refereeing just making things more difficult than they need to be?

Improve this question
$\endgroup$
5
  • 5
    $\begingroup$ So just to clarify, you are not asking for (a) a justification for category theory as tool in various branches of mathematics, but rather for (b) a justification for category theory in the study of programming languages. (Correct?) I think there are many people here ready to answer (a), but not so many with an opinion on (b). $\endgroup$
    – Kevin Walker
    Commented Oct 24, 2009 at 14:29
  • $\begingroup$ Well, I tried to point out that the author seems to refer to a different part of category theory, and you can read this exchange below. $\endgroup$
    – Ilya Nikokoshev
    Commented Oct 24, 2009 at 16:47
  • $\begingroup$ @Kevin Walker: yes, I'm mostly asking about the context of theory of programming languages. (I've studied algebraic topology many years ago and I can see why it fits well there.) $\endgroup$
    – RD1
    Commented Jul 29, 2010 at 3:49
  • $\begingroup$ It's clear I was in a bad mood when I posted this - largely due to refeering a particular paper that only presented in categorial terms when it could have been much more accessible. Actually the categorical perspective has added quite a lot to the field of programming languages - I even use it myself, a little, just that always I relate it to the other main views in my field. $\endgroup$
    – RD1
    Commented Jul 29, 2010 at 11:10
  • 1
    $\begingroup$ It would be interesting to see the reactions of people had this question been posted today (exactly two years later!). I feel now that the question verges on "subjective and argumentative", and is in one respect impossible to answer (we don't know what papers you're refereeing!!). It's also, I find, somewhat unfocused and imprecise. $\endgroup$
    – Todd Trimble
    Commented Oct 25, 2011 at 3:56

4 Answers 4

Reset to default
22
$\begingroup$

Although to you, category theory is merely an inefficient framework for data about logic and programming languages, to mathematicians working in areas like algebraic geometry and algebraic topology, categories are truly essential. For us, some of our most basic notions make no sense and look extremely awkward (in fact, some of them are from pre-category days, and no one really knew what we wanted intuitively until after we started using categories) until you phrase them in terms of categories and universal properties of objects and morphisms (and 2-morphisms, etc). Additionally, it helps us tell what various types of mathematical objects have in common, and how they relate via functors and natural transformations.

As far as recasting algebraic topology and algebraic geometry in terms of lambda calculus, I'd rather like to see that if anyone can manage to, say, give an alternative definition of stack or gerbe or model structure which are more intuitive without using categories and groupoids and the like.

Improve this answer
$\endgroup$
21
$\begingroup$

As a topologist/category theorist with an interest in type systems I can assure you that I find pages full of sequents hard to understand :)

Actually I think the approaches are complementary. Suppose I wanted to talk about the simply-typed lambda calculus (with base types B) and its semantics. Category theory gives you a very simple definition: we take the free closed cartesian category C on the set B; if I choose interpretations of the types as sets, I get the semantics as the functor from C to Set induced from the map B -> Set and the fact that Set is a CCC. In the traditional presentation of the STLC, I have to define

  • the syntax of types
  • well-formedness and typing rules for terms
  • reduction rules to put terms in normal form
  • how to interpret a terms as a function on a set

All told it probably takes a few pages. (As an aside, it's also not clear what kind of mathematical object is being described, which I think can be a little off-putting to non-logicians.)

Of course the traditional presentation has one big advantage: it tells us what the objects and morphisms of C actually are! But this is a computation which we could (and presumably would) do if we adopted the category-theoretic definition of C. The category approach explains why we wrote down those few pages of syntax/typing/reduction rules rather than slightly different ones.

Naturally in other parts of mathematics it's common to have objects determined by universal properties (as the free CCC was here) and to want to compute more explicit presentation of them. If those objects are sufficiently similar to CCCs, then techniques from lambda-calculus may be useful.

Improve this answer
$\endgroup$
2
  • $\begingroup$ A direct presentation of the syntax and types of the simply typed lambda-calculus in the Twelf logical framework is given at twelf.plparty.org/wiki/Intrinsic_encoding. It's five lines, and adding reduction adds just 4 more lines to obtain a self contained, machine checked, and executable system - this is much less than "a few pages", and it achieves more than a categorical explanation. $\endgroup$
    – RD1
    Commented Jul 29, 2010 at 11:31
  • $\begingroup$ Also, I don't agree that category theory is the best way to explain the choices in syntax/typing/reduction. The Curry-Howard isomorphism with implication in natural deduction seems better to me. In my experience requiring a proper relationship with a appropriate logic is more restrictive than interpreting things categorically. A good example of this cs.cmu.edu/~fp/papers/mscs00.pdf introduced some important refinements and concepts to the monadic account of effects by relating to modal logic instead. The categorial view is impartial to these unlike the logical view. $\endgroup$
    – RD1
    Commented Jul 29, 2010 at 11:54
19
$\begingroup$

I think the other answers miss one aspect of this question. Mathematicians vary in how they do math. Some are "syntactic thinkers" (maybe you), some are "conceptual", and some are "geometric" in the way they think. That is the way Leone Burton's book Mathematicians as Enquirers: Learning about Learning Mathematics., Kluwer, 2004, analyzes it. Others take geometric and conceptual to be variations of the same category, and different names are used for the categories, too.

People are different, and in how they think about abstract ideas they are different in a very deep way. That is my own experience in both my research career in and teaching. I took logic from Joe Shoenfield (which gives me a respectable background!) and did work in abstract algebra and then discovered category theory and thought: Way to go! That is because I think primarily conceptually.

Mike Barr said that to a person with a hammer, everything looks like a nail. I keep translating problems into categorical language. You go the other way. These differences run deep, and should be taken into account when reading other people's stuff.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ Actually, I'm not that much of a syntactic mathematician. To me proofs are geometric objects that dynamically reconfigure themselves via proof reduction, and the rules of logic require some deep concepts to justify. I guess to me everyone should learn how to think well in all the different styles, but I guess I know from teaching that not everyone will. I do understand the deep conceptual side of category theory - I only have a problem when authors appear to ignore important non-categorical views of a subject. $\endgroup$
    – RD1
    Commented Jul 29, 2010 at 12:06
0
$\begingroup$

I think for mathematicians, especially the algebraic geometers, category theory has a somewhat different meaning that in your area.

For us, it's primarily an important and quite straightforward way to formalize important properties of natural things, like vector spaces or derived categories or whatever.

In this way category theory is not much different from other subjects, e.g. group theory studies groups. Category theory studies categories. There are some hard to read books on group theory. There are some hard to read books on category theory. Lots of articles about group theory seem to be hard and don't appear to give any benefit to outsider. Same about category theory.

If you search for it, there are really good introductions to the subject. MO already had some questions with links.

Improve this answer
$\endgroup$
5
  • $\begingroup$ As I said, I have a working knowledge. I don't need an introduction. I need to understand why people frame things in terms of category theory in the papers I referee, when there are some standard and much simpler frameworks in logic. BTW - I did a major in Pure Mathematics, and my PhD is in Logic. I learnt my first category theory first in my honours year, in a course on algebraic topology. I still find that it tends to obscure the underlying logical ideas. (Indeed, I think too much of mathematics ignores modern concepts in logic.) $\endgroup$
    – RD1
    Commented Oct 24, 2009 at 10:20
  • $\begingroup$ I'd add this: has anyone tried replacing category theory with lambda-calculus in areas like algebraic topology? Certainly it simplifies the notation and terminology considerably in my field, I will have to think whether the same would happen in those kind of areas. $\endgroup$
    – RD1
    Commented Oct 24, 2009 at 13:28
  • 1
    $\begingroup$ I'm not aware of the logical concepts that would be as relevant to algebraic geometry as category theory is! Maybe if you think topoi and model categories belong to logic, then yes, but if not, then I think you just happened to be taught category theory by a wrong professor. As my feelings to the subject go, it's very useful and straightforward. $\endgroup$
    – Ilya Nikokoshev
    Commented Oct 24, 2009 at 13:30
  • 1
    $\begingroup$ Addition: I'm challenging you to "[replace] category theory with lambda-calculus in areas like algebraic topology" for the material given on the first pages and somewhere in the middle of Lurie's article Higher Topos Theory, arxiv.org/abs/math/0608040. If you do, I think this is something new and many people will be interesting in reading it. But my suspicion is that this cannot be effectively done because this is not logic but rather a separate discipline. $\endgroup$
    – Ilya Nikokoshev
    Commented Oct 24, 2009 at 13:33
  • 13
    $\begingroup$ "Indeed, I think too much of mathematics ignores modern concepts in logic." This is an intriguing statement that should be elaborated upon. $\endgroup$
    – Deane Yang
    Commented Oct 24, 2009 at 16:34

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .