Hacker News Reader

Comment by cousin_it | Hacker News Reader

The paper argues that category theory is useful for computer science. Okay, which areas of computer science? I've studied quite a lot of algorithms, computational complexity, cryptography, computer graphics, machine learning - none of it seems to get any sizeable benefit from category theory.

Most CS folks who like category theory seem to be on the functional programming side of the fence, and use it to basically shovel code around, making things parameterize and plug together in just the right ways. Which is fine, but a far cry from all of CS!

View on HN

Category theory is a useful tool for understanding the syntax and semantics of programming languages, and not just functional ones. The common practice of using category theory to provide abstraction within functional languages is interesting, but not that interesting; unfortunately, it is what most people bring up, since it is so played-up by the Haskell community.

I would say the heart of computer science lies in type theory, computability, semantics, logic, etc., and category theory is evidently useful there. (I'm not talking about these things as limited to so-called "functional" languages, but rather in their capacity as forming a complete, coherent and unified theory for computation, functional or not.)

Certain other subfields of CS (the focuses of the so-called "American" combinatorial school, for instance) seem to get less use out of CT, I'll grant.

Does category theory lead to any interesting results in computability?

I am not aware that it does on its own, but I am not an expert in category theory, so I might be wrong.

Many (most?) applications of category theory are just that—they tend to elegantly marshall disparate theories into a more general framework.

For a very round-about answer, however—since Brouwer, we have understood that a computable function corresponds to a continuous function; continuity has a nice characterization in category theory in terms of sheaves; therefore category theory provides a basis for understanding computability. Or: the syntax of (some, but not all) computable functions is the internal language of an elementary topos. I could go on and on...

The pattern here is that we could have done all this without category theory (and in fact we did!): but it provides a unifying and enriching perspective as one of the three cornerstones of computer science: logic, type theory and category theory. (See Bob Harper's amusing post on the topic for more: http://existentialtype.wordpress.com/2011/03/27/the-holy-tri...)

OK, I see. I'm a bit skeptical of anything that claims to be an enriching perspective but doesn't yield interesting results. This is similar to functional programming, which also feels beautiful and enriching to those who study it, but hard to show that it's superior in any measurable way.

I mean, I like Curry-Howard-Lambek as much as the next guy, but typed computation is mostly about constraining computation to make some things impossible, and I'd like the unifying perspective to be more about making new things possible. Somehow, the type stuff just feels boring and lifeless to me, in a way that e.g. algorithm design doesn't.

There are two lenses through which you can looked at typed computation, intrinsic and extrinsic. From the extrinsic perspective (which I actually prefer for semantical reasons), you are classifying the terms of a computation system which are already endowed with an operational semantics; in this sense, you are constraining computation. But I prefer to use the term "classify" rather than "constrain"; in systems built on this kind of theory, like Nuprl, for instance, you can give a type to any kind of computation you want, even the kinds that are typically ruled out in type theory (such as partiality).

The intrinsic perspective is where the computations and the types are inextricably linked. This is the proof-theoretic, gentzen-style way to look at it. In this case, it is harder to say that you are constraining computation; and in many systems in the intrinsic typing tradition, it is a lot more about inferring computation than constraining it.

However, do not go and think that the extrinsic perspective is "lifeless". I would say that it is the opposite, since this is the result of taking seriously the realizability-style semantics which underly the entire intuitionistic notion of Truth as understood by Brouwer and others. I consider the Curry-Howard Correspondence (the identification of program with proof) to be lifeless, in the sense that nothing is really happening there, since the programs are literally proofs of judgement in a formal system; but the Brouwer-Heyting-Kolmogorov correspondence, which is similar, is much more interesting--this is the classification of computations as witnesses/realizers for propositions.

Intensional type theory is a theory of formal proof, where the terms are literally proofs of judgement: it's pretty dead in there. Type theory based on realizability, though, is more interesting, since the computations exist on their own and we categorize them as the essential computational content of propositions.

Once you go down the rabbit hole, what seems lifeless now may not then. Though based on what you have said about algorithm design, it is entirely possible that we simply have very different aesthetics for theories.

If you are interested in reading further, I wrote something here: http://www.jonmsterling.com/posts/2014-10-29-proof-term-assi.... And follow the links which I give, since those are better than what I wrote!

Many thanks for writing that out! I can't parse most of it yet, but it looks like I have some nice pointers for further study :-)

Sure, no problem. Feel free to email me (jon at jonmsterling dot com) if you have any questions.

Here are a few examples. Here's operational transforms from CT [0][1]. Here's probability theory (and thus much of ML) [2][3][4]. Lambda calculus arises as a certain kind of category. Operads form a model for wiring diagrams. Database schemata are categories [5].

    [0] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.7744
    [1] http://bosker.wordpress.com/2012/05/10/on-editing-text/
    [2] ncatlab.org/nlab/show/Giry's+monad
    [3] arxiv.org/pdf/1410.4432v1.pdf
    [4] https://golem.ph.utexas.edu/category/2014/10/where_do_probability_measures.html#more
    [5] http://arxiv.org/abs/1302.6946

You can cast the broadest abstractions in a categorical light, but that ignores the theoretical details that are 99% of the theory of probability/wiring/databases that is of interest to most scholars and practictioners.

Yes, it's interesting, but it's not at all clear that category theory pays back the opportunity cost for someone who is interested in understanding field X beyond the generalized abstraction.

It's not clear, no. CT is another language for abstraction and the same argument as always hold: languages are equally expressive so it's "just a matter of taste" as to what you use.

Category theory emphasizes focusing on the relations between thinfs instead of the things themselves. This can be a natural fit for some theories. For instance, anyone studying probability theory knows that random variables are already functions instead of "objects" but they are the primary thing to study. The CT-minded expression of probability theory is obviously equivalent to the Kolgomorov one, but takes that r.v. emphasis further. You can decide whether or not that's a good thing.

Not all Category Theory is about FP.

I am trying to use Category Theory to understand the programming patterns in the book Python in Practice.

The book talks about abstract notions like decorators and factories and proxies. These layers of abstraction don't really change how your program runs, but they help you be more oraganized as a programmer. That's what Category Theory is about.

In fact, any case in programming where you are drawing diagrams with boxes and arrows, that can be considered category theory.

Reply on news.ycombinator.com