8

I am a computer scientist with a CS degree from the 80's. I am learning category theory by myself. I am looking for advice about learning category theory. E.g. it is quite helpful in learning category theory to have examples from a familiar topic like logic or programming languages.

What I know

I have read the answers to this question and the paper Physics, Topology, Logic and Computation: A Rosetta Stone which builds up concepts with parallels between category theory, logic, and theory of computation.

I know about the following categories:

• categories
• monoidal categories
• braided monoidal categories
• closed monoidal categories
• symmetric monoidal categories
• closed braided monoidal categories
• compact monoidal categories
• cartesian categories
• closed symmetric monoidal categories
• compact braided monoidal categories
• cartesian closed categories
• compact symmetric monoidal categories

Questions

  1. Are there any other major categories that a computer scientist should know about?

  2. Were there any that have fallen out of favor? If yes, why? Have they been replaced with other categories?

  3. When thinking about categories should I focus on the arrows first before the objects?

Community
  • 1
Guy Coder
  • 199
  • 1
  • 5
  • 2
    For what purrpose are you learning category theory? Is it for logic and semantics, or something else? – David Boshton Jul 01 '14 at 15:25
  • 1
    Obviously a good question to my open ended question. I presently tinker with theorem provers of the HOL variety and functional programming, so logic, languages, BDD, term rewriting, lambda calculus and unification are everyday concepts for me. I am also trying to learn more about SMT solvers. – Guy Coder Jul 01 '14 at 15:33
  • 2
    You could try something completely different to get some feel for the other 90% of category theory. For instance, you could have a look at the basic setup of algebraic topology. That would give you some perspective. – Andrej Bauer Jul 02 '14 at 15:30
  • @AndrejBauer How I wish I knew algebraic topology? It seems to be the typical way to introduce category theory. I will keep this as plan C as it seems to be more of a mountain than a hill for me to learn. Thanks. – Guy Coder Jul 02 '14 at 15:36
  • 2
    I dunno. There are CS students our there who learnt algebraic topology from a computational point of view in one semester. Look up things like "persistent homology". – Andrej Bauer Jul 02 '14 at 15:44
  • Since this question was stared, I will add info as comments that I find of use. If these items get to long I will hopefully edit them back into the question. – Guy Coder Jul 08 '14 at 13:22
  • relation between type theory and category theory – Guy Coder Jul 08 '14 at 13:23
  • You are asking too many questions in one place. It makes the post unfocused. I would suggest putting each in its own question. I would suggest making this one focus on categories that all computer scientists should know about would drop the list of categories you know about and your background from the post to make it more useful also for other readers. I think the first and second questions can potentially be interesting for lots of other users. Though I don't think the 3rd one is good one. You can also ask a separate soft-question about general advice on learning category theory. – Kaveh Jul 09 '14 at 06:37
  • 2
    @Kaveh I don't think there's any such thing as a "category that all computer scientists should know about". I don't think any of my current work (algorithms and complexity) or previous work (finite model theory) required or would even have benefited from any knowledge of category theory. I can't even think of a conference talk I've seen in those areas that has used category theory. – David Richerby Jul 09 '14 at 06:44
  • @David, I think you are interpreting "should" in a different way than I do. I use should in the sense of similar questions (e.g. what papers should everyone read? etc.). Even if we haven't or may not use them doesn't mean we should not know about them. There are lots of stuff that we never use but still we should know about. :) – Kaveh Jul 09 '14 at 06:48
  • @Kaveh Thanks for the edits. As this is CC I don't mind. I have thought about deleting the this question and starting again with more basic questions but this question seems to be a focal point for others with the same interest. I also think that these comments should continue as a discussion which can be used to formulate questions that could help others self-learning CT. I also believe that more CS people should know CT and these Q&A can help them gain the knowledge. – Guy Coder Jul 09 '14 at 10:44
  • solid applications of category theory in TCS – vzn Jul 09 '14 at 15:01

3 Answers3

8

Note that most of the categories you considered are 'abstract', i.e., they require structure or properties of an abstract category. As computer scientists we should also be familiar several concrete categories which turn out to be useful:

Concrete categories

  • Set
  • Set$_{\mathcal P}$ (objects are sets, morphisms are relations)
  • Rel (objects are relations, morphisms are functions preserving these relations)
  • Pred (objects are predicates (= subsets) morphisms are functions preserving these relations.
  • Posets
  • $\omega$-CPOs
  • Nominal sets
  • Lawvere theories

Abstract categories

  • Functor categories
  • Presheaf categories, in particular, monoid actions, which are equivalent to finite automata iianm
  • Locally presentable categories
  • Monads
  • Enriched categories (in particular, O-categories)
  • Kleisli and Eilenberg-Moore categories
  • Embedding-projection categories
  • Profunctors

Also, sometimes properties don't commute on the nose, and the structure under consideration is of higher-dimensional (i.e., 2-categorical).

As to your question 3: you can define a category without mentioning objects at all (though it's conceptually clearer if we do mention the objects).

Ohad Kammar
  • 2,677
  • 23
  • 28
2

If $F$ is an endofunctor in a category $C$, then the category of $F$-algebras is pretty important in the study of datatypes. In particular, initial objects in this category correspond closely to finite datastructures. See this page on Wikipedia for more details, including examples of how the types of natural numbers, cons-lists and binary trees arise in this way.

Also, a monad is just a monoid in the category of endofunctors :-) Highly tongue-in-cheek, but the category of endofunctors is important nevertheless, if you want a better theoretical understanding of (Haskell's) monads.

yatima2975
  • 276
  • 1
  • 4
0

This is not a complete answer (as I'd be surprised if any answer will complete given the disparate nature of your research), but when I was going to do a PhD in re-representation of mathematical issues one of the constructs that was suggested was Sober Spaces. They underlie schemes, which connect algebraic topology, number theory and commutative algebra. This may help with the theorem prover side of things.

David Boshton
  • 191
  • 3
  • Thanks. Yes trying to identify how to get unstuck in self-learning CT is hard as I don't know enough CT to explain my problem. One "ahh" moment came when watching this video by Mike Stay. Also working through Category Theory for Computing Science and doing the exercises is most beneficial. – Guy Coder Jul 08 '14 at 11:04
  • 3
    Is it really right to say that sober spaces "underlie" schemes? Most introductions to schemes and books that talk about schemes that I've seen don't even mention sober spaces (or perhaps they do, but only in passing). I would think it's more that sober spaces generalize schemes, but I'm not so familiar with this part of topology... – Joshua Grochow Jul 08 '14 at 12:41