Category Theory for Programmers (2014) [pdf]

Thanks for this, super interesting. Your second link is repeated though, I assume it should be this: https://math.mit.edu/~dspivak/informatics/notes/unorganized/...

Can someone please explain to me the excitement for category theory in this forum?

I've gone through the first 10 chapters + exercises of this book, and truth be told the content is interesting but the ROI is low for programming (FWIW I started this book as part of a study group in a large unicorn co, and after approximately one month I was the only person left grinding through the exercises, hoping for some payoff).

It's cool that I know what a functor is, I guess, but where others tout CT as unlocking a higher level view of programming, all I see are little curiosities (when you do X you are really doing Y, isn't that cool!?).

I've heard it said that CT's true power comes as a "refactorer" for what would otherwise be complicated proofs. I.E. we discovered a new tool to make proofs that already existed more elegant. That's cool that it has a use! Does this somehow extend to programming?

I don't mean to sound like a grouch, but I'm genuinely baffled by the level of excitement around this topic.

If you're looking to scratch a math itch, ML has plenty of opportunities to hobby some math while advancing your career and marketability.

For programming in general, there are tens of topics I would pick before reaching for this, with major immediate payoff to our occupation as programmers.

Finally, after going through 10 chapters I skipped to the end to see if there was some culminating breakthrough that we were striving towards... and I found more definitions stacked upon other definitions. I suppose memorizing all these definitions is supposed to give me a different mental model about programming. Is that right?

I'll quote here the first line of the Analects, "Isn't it a pleasure to study and practice what you have learned?". This is what I look for in studying any topic: something that gives me joy to put into use. In the best cases it gives me a feeling of a super power - something that was previously impossible or extremely difficult is now elegant and clear. Can CT offer that in any way to programming?

-Sincerly, Guy that doesn't get it, but wants to

The problem for someone like myself is that I have taken some classes on basic abstract algebra in high school (groups, monoid, rings etc) and came out of it with some definitions and... Nothing else. I can probably still tell if some operation on some set forms a group or not, but that has never been a directly useful tool in what I learned further through high-school and university. It didn't help in linear algebra. It didn't help with calculus. It didn't help with control theory. It didn't help with numerical methods. Sure, I could go around and see if new operations I learned about formed, say, rings, and I'm sure a lot of them do, but that was never used in theorems or demonstrations in those fields (the way I was taught them, anyway).

It was only ever a set of definitions. And almost everything I've seen browsing on category theory seemed the same - like it's just definitions, new names for old concepts, with few theorems shown that elucidate the need for these new names.

For example, lists and optionals and Either are monads. IO is also a monad. The most I've seen make use of knowing this fact is some nice-ish syntax sugar that works for all 3 of these seemingly disparate concepts. But even then, the 'work' for enabling that sugar seems to be done by the simple properties of the monad, more than some theorem that had been proven on monads in general.

Are there some examples of common CS abstractions that are almost but not quite category theory constructs? Are there any simple examples where we get new proofs by recognizing that some old CS concept is, say, a monad?

I understand your point about theorems for free in principle, but I have never seen one in these kinds of discussions (at least, not one that wasn't also a definition, e.g. if X is a monad than Y must be a functor).

Unix pipeline a category, with text be object, and executable be morphisim converting text to text(monoid). Forth is a category, with stack as object, functions as morphisim. There are many examples. Best learn from haskell.

I watched the first part of his lectures on category theory. Keep in mind I'm the furthest thing from a mathematician you can find.

The feeling I'm getting when learning category theory is that if there was a formal theory for how to design programs. Category theory is it. Application is therefore not straightforward... You have to get really creative and think really hard to see the insights that category theory has to offer.

The notion of a isomorphism and a functor and lifting was directly applicable to programming after I learned about it. Here's what happened:

In postgresql there are specific library functions for dealing with specific types of json structures in the postgresql library. If your json blob doesn't fit the structured type parameter that the library function accepts you have to do some very awkward joins to convert the json into the right format which can cause massive slow downs.

I use the notion of two isomorphic objects and the opposing functors between them to convert the json into a string functor. Then I did string manipulations to convert the serialized json into a different form of serialized json then re-lifted the serialized json back into the json functor. The converted json type fit the parameter of a library json function and thus the result was a query that executed 10x faster then the other implimentation.

If I didn't know category theory the code would look absolutely crazy. I cast json to a string, replace a bunch of characters in the string then cast it back to json. The notion that a string can contain another type as a functor and the notion that string manipulations operations on serialized json have an isomorphic equivalent in "json space" was what allowed me to creatively come up with this optimization.

Note that the json equivalent morphisms I needed do not actually exist in the postgresql implimentation but because of the isomorphism that exists between stringified json and actual json I can build the json morphisms I need by composing two opposing functors and a string manipulation operation.

The thing about this though is that it's debatable whether or not you would actually need such "creativity" in a language that wasn't as terrible as SQL.