[rssoconnor]

Apologies for the jargon, but there isn't room in a comment box for a detailed explanation.

"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

[i_am_toaster]

This is a lot to digest, but I’m responding to this one because of I think this attempts to answer my question and because of your 4th reference. That being said I need to ask some questions.

Would I be correct in saying — there are less complex objects, which are defined in category theory, that are useful in a generic way in combination with one another?

If the answer to that question is yes, is there a place I look to find the mappings of these software topics/designs to these category theory objects such that I can compose them together without needing the underlying design? If that were the case, I could see the use in understanding category theory so that I could compose more modular and generically useful code.

I have to admit though, I’m still fairly speculative and my thinking on this is very abstract and probably very flawed.

[rssoconnor]

I think your understanding is a little off the mark, at least with respect to my not-so-well written comment, which was just meant as a rambling story about how category theory influenced my and others development of (functional) programming "optics" over the last decade.

The new "optics" people are have designed in reference 4 are not themselves "elements of category theory", but category theory provides the theoretical framework that these composable optics live in. Once that framework is identified, it becomes much easier to say "oh, this new optic definition I've just identified, fits into this framework, and so does this other optic, and so forth"

To make a loose analogy, one could imagine identifying triangles and cubes and such and such that have these rotational and reflective symmetries, and notice how you can compose those operations, and then see how performing specific shuffles of cards is also composable and has some properties similar to rotating cubes in that repeated operations have a certain period and other such things. Then when someone introduces you to group theory and says yes both the cube rotations and the card shuffling can all be seen as a group and group theory can be used to generically answer your questions about these otherwise seemingly very different operations. And then you start seeing that lots of things are groups, like that Rubik cube puzzle you have, or lines through an elliptic curve. Coming up with new optics is analogous to noticing various things are groups, a task that is much easier when you have group theory and know how to recognize a group when you see it.

That said, I think a better answer to your question may be in one of my later replies https://news.ycombinator.com/item?id=33806744: Category Theory has been useful for devising an entirely new (functional) programming abstraction, the theory of "optics" in my case. But for day-to-day programming you don't normally need to invent entirely new programming abstractions, you can just use the ones that have already been developed by the computer scientists.

[i_am_toaster]

I’m curious if this is an answer that others would agree with. I could see your reasoning being valid on this, but I tend to see others responding that it has much more broad utility than that.

Typically when something is confusing to me and I see nothing to grasp onto, it usually means something is flawed or poorly communicated. In other words, when no one can explain why something has utility (in everyday programming) and there are a fair number of responses, then the chance of bad communication goes down and bad reasonings (non-answers) goes up. I have a feeling it is not coincidence that you have the opinion it is not utilitarian in everyday programming and that I responded to your initial post.

[larve]

I'm not entirely sure if that is what you are asking, but for example pure functions from a type A to a type B can be compose with pure functions from a type B to a type C, to form a pure function from A to C. A lot of programmer oriented CT takes place in the category of types, with morphisms being a function from one type to another. Programming in a purely functional style makes composition of functions... trivial, compared to a function that has side-effects due to mutation.

Now of course this sounds trivial, but you can build much more refined concepts out of that simple idea. For example, creating product and sum types.

And that's where the rabbit hole starts.