[Twey]

Insofar as ‘computation’ is about mapping one state or value to another state or value, it has a lot to do with CT!

The question of whether CT is _useful_ for studying computation is different, and there are certainly other lenses you can see computation through that some people would argue are better. But it's hard to deny that they're _related_.

[ctenb]

I mean, technically almost all of math can be related to other math one way or another. To say the CT has a lot to do with computation is definitely a stretch. CT is not a recognized Computer Science subject. It's mostly used in the functional programming community to name certain concepts and theorems, but then applied to a specific type system (so it's not actually doing CT, since your restricting yourself to a single category, whereas CT is really about connecting different categories by generalizing over them).

[sesm]

Good point, algebraic topology is mostly concerned with Top -> Grp functors to prove the properties of continuous transformation, while Haskel community focuses on Hask -> Hask endofunctors to use fancy names for mundane things.

[feanaro]

And yet the categorical concepts in Hask are undoubtedly practically useful, more so than an arbitrary sample of concepts, and compose extraordinarily well. Does that have nothing to do with those concepts deriving from (even more general concepts of) category theory?

[Twey]

> To say the CT has a lot to do with computation is definitely a stretch.

I think the argument I presented above adequately justifies CT as fundamentally connected to computation, at least as we study it today, though I think there are other formalisms as well that are just as worthy.

> CT is not a recognized Computer Science subject

I'm not sure who decides this :) Certainly when I studied computer science we had modules on category theory, along with other applicable ‘discrete math’ subjects.

CS is a bit of a grab-bag of a discipline, so it's very hard to say what does or doesn't belong on a CS curriculum. But I think programming language semantics, which is the field where you see CT pop up the most, is probably uncontroversially CS, or at least I don't know what other discipline would claim it.

> It's mostly used in the functional programming community to name certain concepts and theorems

It's mostly used in the PL community; its use in functional programming is an attempt to connect the language more directly to that lineage (or because functional programming languages traditionally came from that community, where the language is already understood and available to describe things).

> but then applied to a specific type system (so it's not actually doing CT, since your restricting yourself to a single category, whereas CT is really about connecting different categories by generalizing over them)

I agree that there's not a lot of interesting category theory to do when restricted to a single category, but this isn't quite correct. Some type systems, e.g. simply typed lambda calculus, are adequately _described_ by a single category, though in more advanced cases you usually need more than one (e.g. dependently typed languages are often described by ‘categories with families’, which are a slightly more sophisticated category-theoretical construction). But even within a single type system you usually find many categories; for example a type system can often be described by a category of terms that map between its typing contexts, but within that category you also have a category of types and functions between them, a category of (functorial) type constructors and natural transformations, et cetera. An important family of examples are the Kleisli categories over monads: every monad actually defines a category of its own, whose categorical laws give the good behaviour of monads that make them useful for composing effectful computations. Interactions between these different categories are where inspiration comes from for CT-flavoured API design, e.g. the ‘interpreter’ pattern that's popular in Haskell (https://softwareengineering.stackexchange.com/questions/2427...). Even in pure CT the study of ‘connecting different categories’ can be seen mostly as taking a sufficiently close look at the category `Cat` of categories and functors!