Hacker News Reader

Comment by tristramb | Hacker News Reader

So category theory is really the theory of composition of mappings. I conjecture that all programming can be seen as just the composition of mappings. If this is correct then category theory is a theory of programming.

View on HN

It can very much be. Here’s one example of this phenomenon (there are many others but this is the most famous): https://wiki.haskell.org/Curry-Howard-Lambek_correspondence

You don't need category theory to connect dots with arrows, graph theory is enough for this.

Category theory is actually a ‘simplified’ graph theory, i.e. you can see categories as a restricted class of graphs. E.G. ‘Category Theory for Computing Science’ introduces categories this way (a category is a directed graph with associative composition and identity; the free category on a graph is the graph with all identities and compositions filled in). But the restrictions (associative composition and identity) are harmless and natural for programming applications where there's always a notion of ‘do nothing’ or ‘do one thing after another’, and unlock a lot of higher structure.

But what's the utility of this definition? Does it help solve or prove something?

It helps you build an intuition for categories, if you're used to graphs :)

If you have a working intuition for categories then in most cases the specific formulation you choose as a foundation doesn't matter, just as most mathematicians work nominally in set theory without worrying about the subtleties of ZFC.

IMO the right intuition about a tool comes from applying it in the context where it provides a real leverage. In case of Category Theory that would be advanced algebraic topology (not re-phrasing basic things which are easier to understand without CT).

Rephrasing things is useful when it allows you to draw equivalences with other things that might have results or insights that translate across, which is something a lot of people use CT for. As with most maths the payoffs aren't always immediate, though, which leads to a lot of frustration with from programmers who expect immediate results from their insights.

From a programming perspective, though, a fair few important things have (by now) turned out to be useful that have come as a result of rephrasing programming in mathematical terms. Some top contenders are monads (directly from CT — think Haskell, but also LINQ, JavaScript Thenables, async/await, Rust Option/Result combinators, parser combinators), proof assistants and modern approaches to type systems, linear/substructural logic (think Rust or C++ move semantics), functional programming (which is now embraced at least to some extent by all mainstream programming languages), functional reactive programming (the core ideas behind things like React), et cetera.

If you allowed infinite graphs maybe. How would you define a functor or natural transformation in graph theory? Seems like you would need to construct a conceptual system that is just equivalent to category theory

No, but if you want to talk about composing those arrows (and a sensible notion of composition should probably be associative, and perhaps have a unit) you eventually end up reinventing category theory.

Reply on news.ycombinator.com