Why I am learning category theory

Because people think “category theory” means “abstract math” in general, due to cargo-culting in and around the Haskell community.

Logic and proof theory is actually one of the areas in math where category theory is most clearly useful. Intuitively, this is because reflexivity ("A leads to A") and transitivity ("A leads to B and B leads to C, hence A leads to C") are well-known rules of any kind of proof writing or indeed of argumentation in general, and they exactly describe a category.

Eg Stuff about types and endofunctors feels like trivial examples using the jargon just to use it. OTOH discovering the Top->Grp functor in algebraic topology is kind of unexpected and revealing.

For example if it were 2008 and you want to be inventor Applicative functors for use in Haskell, then knowing lax monoidal functors from CT might be helpful. But if you want to just use Applicative functors, you don't need to learn lax monoidal functors first.

So programmers probably don't need to learn CT because they can just let the computer scientists devise their abstractions for them. But if you want to be a computer scientist and one day devise your own abstractions[0], then maybe CT would be helpful.

[0]https://news.ycombinator.com/item?id=33805923

  "foo" + "bar" -> "foobar"
  "foo" + "" -> "foo"

Similarly, with arrays:

  [:foo,:bar] + [:baz] -> [:foo,:bar,:baz]
  [:foo,:bar] + [] -> [:foo,:bar]

  defaults + user_input unless user_input_array.empty?

This is all applicable to how you can design libraries and DSLs that seem intuitive and easy to use. Instead of just thinking about bundling a number of methods together with a data structure, you can make sure that a single method within that bundle works the way you expected across a number of objects. You might even be using these ideas in your code, but don't realize it.

Category theory is the language of diagrams; it studies math from that perspective. However, it turns out that category theory is equivalent to type theory (ie, what computers use). So the reason why diagrams can be reliably used to represent the semantics of type theory expressions is category theory.

My workflow of developing ubiquitous language with clients and then converting that into a diagram mapping classes of things and their relationships followed by translating that diagram into typed statements expressing the same semantics is applied category theory.

The “category theory types” are just names for patterns in those diagrams.

Trying to understand them without first getting that foundational relationship is the path to frustration — much like reading GoF before groking OOP.

To understand category theory's appeal in a programming context, you must understand the duality of power in programming languages. Some people call a language "powerful" when it lets you do whatever you want in the particular scope you are currently operating in, so, for instance, Ruby is a very powerful language because you can be sitting in some method in some class somewhere, and you can reach into any other class you like and rewrite that other class's methods entirely. Some call a language powerful when the language itself is capable of understanding what it is your code is doing, and further manipulating it, such as by being able to optimize it well, or offer further features on top of your language like lifetime management in Rust. This type of power comes from restricting what a programmer is capable of doing at any given moment.

If your idea of "power" comes from the first sort of language, then category theory is going to be of very little value to you in my opinion. You pretty much have to be using something as deeply restrictive as Haskell to care about it at all. I am not making a value judgment here. If you never want to program in Haskell, then by all means keep walking past category theory.

Haskell is very much a language that is powerful in the second way. It restricts the programmer moreso than any other comparable language; the only languages that go farther essentially go right past the limit of what you could call a "general purpose language" and I daresay there are those who would assert that Haskell is already past that point.

Category theory then becomes interesting because it is simultaneously a set of deeply restricted primitives that are also capable of doing a lot of real work, and category theory provides a vocabulary for talking about such restricted primitives in a coherent way. There is some sense in which it doesn't "need" to be category theory; it is perfectly possible to come to an understanding of all the relevant concepts purely in a Haskell context without reference to "category theory", hence the completely correct claim that Haskell in no way necessitates "understanding category theory". You will hear terminology from it, but you won't need to separately "study" it to understand Haskell; you'll simply pick up on how Haskell is using the terminology on your own just fine. (Real mathematical category theory actually differs in a couple of slight, but important ways from what Haskell uses.)

So, it becomes possible it Haskell to say things like "You don't really need a full monad for that; an applicative can do that just fine", and this has meaning (basically, "you used more power than was necessary, so you're missing out on the additional things that can be built on top of a lower-power, higher-guarantee primitive as a result") in the community.

This mindset of using minimal-power primitives and "category theory" are not technically the same thing, but once you get deeply into using minimal-power primitives pervasively, and composing them together, you are basically stepping into category theory space anyhow. You can't help but end up rediscovering the same things category theorists discovered; there are a hundred paths to category theory and this is one of the more clear ones of them, despite the aforementioned slight differences. I'd say it's a fair thing to understand it as this progression; Haskell was the language that decided to study how much we could do with how little, and it so happens the branch of math that this ends up leading to is category theory, but as a programmer it isn't necessary to "study" category theory in Haskell. You'll osmose it just fine, if not better by concretely using it than any dry study could produce.

To be honest, I'm not even convinced there's that much value in "studying" category theory as its own thing as a programmer. I never studied it formally, and I wrote Haskell just fine, and I understand what the people using category theory terms are talking about in a Haskell context. If nothing else, you can always check the Haskell code.

There is a nearby parallel universe where the Haskell-Prime community in the late 1990s and early 2000s was otherwise the same, but nobody involved knew category theory terminology, so "monad" is called something else, nobody talks about category theory, and nobody has any angst over it, despite the language being otherwise completely identical other than the renames. In this universe, some people do point out that this thing in Haskell-Prime corresponds to some terms in category theory, but this is seen as nothing more than moderately interesting trivia and yet another place where category theory was rediscovered.

But I bet their Monad-Prime tutorials still suck.

Those who learn either or both, have a larger set of mental abstractions that largely transcend any one programming language. They can say, this thing and that thing share a common salient property through a certain abstract pattern. There is a certain sense of mathematical beauty in recognizing common patterns and mechanisms. There is also the choice of subtly or drastically altering one's coding style. The same with each, a programmer can use just the right design pattern in just the right place and perhaps simplify or codify a section so that it's easier to understand the next time around (or decide not to!) or they can go completely wild and over-pattern their code. The same applies to category theory. One can recognize that some section is actually a closed reduction and accepts any semigroup and then decide to codify this into the program or not.

I tend to be a collector of ideas, so learning category theory and it's application in programming gives me all these little gems and ways to re-understabd code. Sometimes I use them and sometimes I don't, but my life is more joyful just knowing them regardless.

"The Essence of the Iterator Pattern"[0] posed an open problem in type theory as to whether or not "lawful traversals", of type `∀ F:Applicative. (X -> F X) -> (B -> F B)` could appear for anything other than what is called a "finitary container"[1], B := ∃S. X^(P S) where the (P S) is a natural number (or equivalently a polynomial functor B := ∃n. C_n * X^n). Or rather, there was an open question as to what laws are needed so that "lawful traversals" would imply that B is a finitary container.

Eventually I came up with a fairly long proof[2] that the original laws proposed in "The Essence of the Iterator Pattern" were in fact adequate to ensure that B is a finitary container. Mauro Jaskelioff[3] rewrote my proof in the language of category theory to be few lines long: use Yoneda lemma twice and a few other manipulations.

Anyhow, the upshot of reframing this as a simple argument in Category Theory meant that, with the help of James Deikun, I was able go generalize the argument to other types of containers. In particular we were able to device a new kind of "optic"[6] for "Naperian containers" (also known as a representable functors) which are of the form B:=P->X (aka containers with a fixed shape).

Since then people have been able to come up with a whole host of classes of containers, optics for those classes, representations for those optics, and a complete characterization of operations available for those classes of containers, and how to make different container classes transparently composable with each other[4].

For example, we know that finitary containers are characterized by their traversal function (i.e the essence of the iterator pattern). Naperian containers are characterized by their zip function. Unary containers are characterized by a pair of getter and setter functions, something implicitly understood by many programmers. And so on.

I don't know if all this means that people should learn category theory. In fact, I really only know the basics, and I can almost but not quite follow "Doubles for Monoidal Categories"[5]. But now-a-days I have an "optical" view of the containers in, and forming, my data structures, slotting them into various named classes of containers and then knowing exactly what operations are available and how to compose them.

[0]https://www.cs.ox.ac.uk/jeremy.gibbons/publications/iterator...

[1]https://en.wikipedia.org/wiki/Container_(type_theory)

[2]https://github.com/coq-contribs/traversable-fincontainer

[3]https://arxiv.org/abs/1402.1699

[4]https://arxiv.org/abs/2001.07488

[5]https://golem.ph.utexas.edu/category/2019/11/doubles_for_mon...

[6]https://r6research.livejournal.com/28050.html

Alot of the generic interfaces you design in OOP end up being useless. Never re-used and pointless. You never needed to make these interfaces in the first place

In category theory, you will be able to create and identify interfaces that are universal, general and widely used throughout your code. Category theory allows you to organize your code efficiently via interfaces and thus enable Maximum reuse of logic.

When creating an interface you largely use your gut. Category theory allows you to draw from established interfaces that are more fundamental. Basically class types in haskell.

If you want to see the benefit of category theory, you really need to use haskell. Monads for example are a pattern from category theory.

Also a lot of what people are talking about in this thread is exactly what I'm saying^^. I'm just saying it in less complicated jargon.

A good example is LINQ, they use monads and functors. They just gave them other names.

- Triviality

The most trivial cases are actually the most important. If I build a little DSL, I give it an explicit "identity" construction in the internal representation, and use it liberally in the implementation, transformation phases, and tests, even though obviously its denotation as a no-op will be optimized away by my little DSL compiler, and it may not even be exposed as an atomic construct in the user-facing representation.

- Free constructions

When it's difficult to separate a model from an implementation, when simple interfaces are not enough because the model and implementation are substantially complex, multilayered systems on their own, often the answer is to use a free construction.

Free constructions are a killer tool for allowing the late-binding of rather complex concerns, while allowing for reasoning, transformation, and testing of the underlying components without worrying about that late-bound behavior. "Late-bound" here does not have to mean OO-style dynamic dispatch -- in fact now you have more expressive power to fuse some behaviors together in a staged manner with no runtime indirection, or to make other behaviors legitimately dynamic, differing from one call to the next. Tradeoffs in the flexibility/performance space are easier to make, to change, and to self-document.

This is particularly useful when you need to start addressing "meta" concerns as actual user-facing concerns -- when your project matures from a simple application that does Foo into a suite of tools for manipulating and reasoning about Foo and Fooness. Your Foo engine currently just does Foo, but now you want it to not just do Foo, but return a description of all the sub-Foo tasks it performed -- but only if the configuration has requested those details, because sometimes the user just wants to Foo. So you embed the basic, non-meta-level entities representing the actual component tasks in a free construction, compose them within that free construction, and implement the configurable details of that composition elsewhere.

- "Sameness"

Making clear distinctions between different notions of sameness is important. Identity, equality, isomorphism, adjointness -- sure, you might never explicitly implement an adjunction, but these are important notions to keep separate, at least conceptually if not concretely in source code entities, as a piece of software grows more complex. If you treat two things as fundamentally the same in more ways than they really are, you reach a point where you now can no longer recover crucial information in a later phase of computation. In an indexed/fibered construction, this X may be basically the same as that X, but this X, viewed as the image of a transformation applied to Y is quite different from that X, viewed as the image of a transformation applied to Z, although the images are equal. So can I just pass my X's around everywhere, or do I need to pass or at least store somewhere the references to Y and Z? What if computationally I can only get an X as the result of applying a function to Y, but conceptually the functional dependency (that is, as a mathematical function) points the other way around, from X to Y? Paying attention to these easy-to-miss distinctions can save you from code-architecting yourself into a corner. You may discover that the true reserve currency of the problem domain is Y when it looks like X, or vice versa.

Patterns for decomposing problems and composing solutions.

To ask “How is it useful?” Is to ask “How are design patterns useful in OO?”.

But you already know the answer…

Is there an advantage over just inventing your own vocabulary? Yeah! You don’t have to reinvent 70+ years of Mathematics, or teach your language to other people before you can have a meaningful design discussion.

The 80/20 rule really applies here. Most of the time there's only a few key type classes that people use. Pretty much just Monad, Monoid, Applicative, Functor. If you grok those, then what people say makes a lot more sense.

> Can anyone give me a practical applied way in which category theory is a benefit to your design

Monad is probably the best example, because so many different, important libraries use it. Once you know how to code against one of them, you kinda know how to code against all of them!

The following is code written in the STM monad. It handles all the locking and concurrency for me:

   transfer x from to = do
       f <- getAccountMoney from
       when (f < x) abort
       t <- getAccountMoney to
       setAccountMoney to   (t + x)
       setAccountMoney from (f - x)

As well as the 4 monads mentioned above, parsers are monadic, same with Maybe and Either, List. The main concurrency library 'async' is also monadic (though it just uses the IO monad rather than defining an Async monad).

Often the people writing your mainstream libraries know this stuff too. If you're calling flatMap (or thenCompose), you're calling monadic code. The writers just shirk from calling it monadic because they're worried people will suddenly not understand it if it has a scary name.

https://www.youtube.com/watch?v=nY1BCv3xn24

Oh and also when you recognize your design to be something from ct its probably quality. Shit code cant be described with simple math (simple as in all math is simple, not as in math that is easy to understand).

I think of category theory as an easy way to remember things. If some concept can be expressed as category theory, it can often be expressed in a very simple way that’s easy to remember. However, if you try to teach math using category theory from the beginning, it feels a little like trying to teach literature to someone who can’t read yet.

Anything directly useful from category theory can be expressed as something more concrete, so you don’t NEED category theory, in that sense. But category theory has the funny ability to generalize results. So you take some theorem you figured out, express it using category theory, and realize that it applies to a ton of different fields that you weren’t even considering.

The effort to reward of category theory is not especially high for most people. It did give us some cool things which are slowly filtering into day to day life—algebraic data types and software transactional memory are two developments that owe a lot to category theory.

> Category theory is the mathematics of composition.

I don't know why you're being downvoted (tone?) but you're right. Categories formalize exactly and only the notion of composition; its power is that this notion appears everywhere when you know what to look for. Most mathematical abstractions have composition baked in at one level or another, so I think the author should be pardoned for their phrasing; but I find yours more enlightening.

I have no formal critique of him, or even concrete things to point at to say why it doesn't work for me, but I wanted to add my comment in case someone else was also feeling discouraged by not taking much away from the writings/lectures of an often and highly recommended person.

I generally learn very well from lectures/essays, but that hasn't been true for me re: his work.

One of the most interesting things in CT are adjoints. They happen literally everywhere. For example, static analysis via abstract interpretation is an example of adjoint (which in this case is called Galois connection). Free structures also give rise to adjoints.

The fact it's so rare to find a counterintuitive fact in CT, so that you rarely find yourself proving something and you mostly spend your time constructing effective tools, it's a feature not a bug! McBride's "Don't touch the green slime!" is a great paper/saying about this principle. Work with the compiler, not against it. The compiler is very dumb so it understands only trivial things.

There's a legacy pseudomachist culture of 'hard is good' in mathematics (but really, it's transversal to science) which rewards working hard and not working smart.

Software engineers and (non-categorical) mathematicians are both forced to deal with patterns of abstraction on a regular basis, so they naturally pick up a lot of what category theory concerns itself with. This can make category theory sound like quite a lot of words for very little gain. But I do think that formalizing one's intuition -- taking something understood implicitly and giving it explicit form -- can be a useful tool in its own right.

Most of the material out there on category theory attempts to formalize the algebraist's intuition. Software engineers then have to learn algebra just to learn category theory. I don't think that's essential to category theory, and I think we're starting to see more and more "elementary" category theory that doesn't take some other whole edifice as given. The fact that so many software engineers exist who do find value in a categorical perspective (it's more than you'd expect!) suggests that we'll get there eventually.

However, it is "generative" knowledge. Having a good intuition for monads is what allows me to break down a fair amount of the mundane tasks I have to do (say, breaking down and migrating infrastructure configuration) in steps that work and stand the test of time. That's the thing about say, monad. An applied monad just looks utterly trivial, because, really, they are. If they weren't they wouldn't be worth using.

It also allows me to mine the literature or reuse things I've worked out in the past, for example exploiting monoidal structure for optimizing computation by leveraging associativity, for example.

Learning almost anything is useful in some capacity. Is everything you learn equally important? Maybe, maybe not, but you never know in advance how things might end up useful.

Of all the things one can study, math seems to be a pretty safe bet in terms of ROI.

(edit: typo)

Google search first result:

    Functor - Wikipedia
    https://en.wikipedia.org › wiki › Functor
    In mathematics, specifically category theory, a functor is a

https://en.wikipedia.org/wiki/Monoid_(category_theory)

As far as mathematics is generally concerned, I think the category theory concept is the origin. Monoids, on the other hand, did exist before category theory; the modern conception as one-object categories is nice, but it's definitely an import.

Will it make you write code that is more optimal and yet harder to penetrate by others?

const renderer = props => <h1>Hello {props.pageName}</h1>

const Title = ReactComponent(renderer).contramap(props => { pageName: props.title })

Title.fold({ title: 'Home page' }) // <h1>Hello Home page</h1>