A Categorical Manifesto (1991) [pdf]
citeseerx.ist.psu.edu
citeseerx.ist.psu.edu
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!
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.
[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.6946Yes, 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.
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.
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.
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...)
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.
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!
[1] http://picpaste.com/pics/c5f9cc612f213523876362234155499e.14...
[1] - http://picpaste.com/76610ba89c0650c0a80a48574c965aff.png
[2] - http://blog.kowalczyk.info/software/sumatrapdf/free-pdf-read...
Some people are just used to using their existing document processing pipelines rather than using more modern tools like pdflatex, I guess.
Edit: the file predates pdftex. Back then, the file would've just been sent to a printer rather than rendered on screen for anything other than a preview, and it looks fine when rendered. If it was passed through pdflatex these days, it'd look much better.
Reading this reminds me of how cool category theory is, how I didn't use any in my thesis, and how I dodged a bullet :-)