Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Software refactoring as natural transformations

ww (Mar 14 2026 at 09:01):

So I've been working on a language called "plumbing" for hooking up "AI agents" into networks. It is based on the copy-discard category with a bit of extra structure that @John Baez kindly let me write about on the n-Category cafe.

Last night I was doing some work on the runtime. A fairly major refactor. I am using a "coding agent" to assist with this and a methodology that basically involves a whole bunch of discussion and design before passing it over to "engineering" to do the actual implementation. Here is a diagram of what the process looks like, roughly, from a talk I gave a couple of weeks ago at the Quantum Software Lab in Edinburgh,

I explain in a bit more detail what happened at the link below, but it looks like, because I set the whole thing up in categorical terms, and gave quite precise instructions about the target of the refactor -- a design note and an explicit operational semantics -- when the coding agent came upon a question in its planning and review cycle, the framing of "software refactor" happened in terms of natural transformations. This is a very good way to look at it and not something I have seen before. Maybe it is known to people who work with proof assistants?

The really nice thing about this is that sort of framing constrainst the implementation so much that the coding agent doesn't have much scope to go off and do nonsense. It just gets on with the tedious mechanical details.

https://leithdocs.com/ldc/documents/notes/research/bridge-as-natural-transformation.md

John Baez (Mar 14 2026 at 17:06):

I don't understand this sentence:

when the coding agent came upon a question in its planning and review cycle, the framing of "software refactor" happened in terms of natural transformations.

The passive voice at the end is confusing to me, I guess, and "framing" is quite abstract. Did the coding agent doing the refactoring take advantage of the naturality? Or did you, knowing the naturality, take advantage of it to answer a question the coding agent had?

ww (Mar 14 2026 at 17:15):

I mean it noticed the naturality and used it to organise its work so that it could check it was doing the right thing.

John Baez (Mar 14 2026 at 17:17):

Oh wow, that's the best of all.

John Baez (Mar 14 2026 at 17:19):

I wish your article included some quotes from Claude showing how it "noticed the naturality". Some people will be very dubious without evidence. And it would be fun.

ww (Mar 14 2026 at 17:38):

The article (below the editorial bit, which was me) was written by claude after I noticed a mention of a discussion between the "engineer" agent and the "theorist" agent about naturality. I stopped them and said, "hey, what did you do there? write it up".

ww (Mar 14 2026 at 17:46):

I will try to set up to record of everything that happens to have a better audit trail for the next time something like this occurs. It's a bit cumbersome (until I can get the plumbing runtime developed enough to be able to replace claude code...).

John Baez (Mar 14 2026 at 17:47):

Oh! The article doesn't say: "The following was written by Claude". I think you should add something like that, for a whole bunch of reasons.

ww (Mar 14 2026 at 17:49):

Good idea! Done.

ww (Mar 14 2026 at 18:41):

Actually, it isn't cumbersome at all to extract the transcripts. I've put it here (it's quite long, you'll want to search for "natural transformation") https://river.styx.org/transcripts/bridge-natural-transformation/

ww (Mar 14 2026 at 19:08):

I've caused it to make a nice summary. The key passage:

Architect was asked:

Review for architectural soundness, boundary correctness, system vision alignment. Specific questions: Is "close fabric sockets, agent creates fresh ones" the right boundary? Should make_zmq_handler be in bridge.ml or a separate module? Is the two-backend transport abstraction unnecessary complexity? Does tool dispatch through pipe adapters add too many layers?

The Architect responded (unprompted) with the key observation: "The bridge is a natural transformation between representations; a ZMQ-native handler is not a bridge at all" — answering the make_zmq_handler location question by reframing the entire module boundary in categorical terms.

(Evidently it was not the "Theorist" it was the "Architect")

Matteo Capucci (he/him) (Mar 15 2026 at 16:05):

So... in which sense is a refactor a natural transformation? I don't understand if this is a thing inside plumbing (ie there is a 'refactor' operation or smh) or you're talking about the codebase implementing plumbing

John Baez (Mar 15 2026 at 16:37):

He's talking about the codebase that implements plumbing. He wants to refactor it, so he got Claude to do it using a network of agents, and the "Architect" agent realized that the refactoring process can be thought of as a natural transformation:

ww said:

So I've been working on a language called "plumbing" for hooking up "AI agents" into networks. It is based on the copy-discard category with a bit of extra structure that John Baez kindly let me write about on the n-Category cafe.

Last night I was doing some work on the runtime. A fairly major refactor. I am using a "coding agent" to assist with this and a methodology that basically involves a whole bunch of discussion and design before passing it over to "engineering" to do the actual implementation. Here is a diagram of what the process looks like, roughly, from a talk I gave a couple of weeks ago at the Quantum Software Lab in Edinburgh,

I explain in a bit more detail what happened at the link below, but it looks like, because I set the whole thing up in categorical terms, and gave quite precise instructions about the target of the refactor -- a design note and an explicit operational semantics -- when the coding agent came upon a question in its planning and review cycle, the framing of "software refactor" happened in terms of natural transformations. This is a very good way to look at it and not something I have seen before. Maybe it is known to people who work with proof assistants?

https://leithdocs.com/ldc/documents/notes/research/bridge-as-natural-transformation.md

John Baez (Mar 15 2026 at 16:40):

Having worked with Claude Opus 4.6, this level of cleverness does not shock me.

Matteo Capucci (he/him) (Mar 15 2026 at 16:46):

Ok but then I'm having a hard time understanding if the claim is actually formal? How's a codebase a functor? How is refactoring a natural transformation? And how did Claude leverage this fact to constrain the edits? :thinking:

ww (Mar 15 2026 at 16:57):

Hi Matteo!

So here's the argument. I have some category $C$ which is the interface that I am preserving. In this case it is a category (a copy-discard category with some extra structure). In general, maybe it isn't, I don't know.

There is a functor $F : C \rightarrow Impl$ that gives it an implementation. Again, people might not habitually make their implementations of interfaces well-behaved like this, but I try to.

Now in this case, we want to change implementations, so we want a different functor, $G : C \rightarrow Impl$.

In the example above, we are actually replacing a compiler back end which is a bit of a complicated to do, so we end up with intermediate states in the refactor where some parts of the compiler are using $F$ and some parts are using $G$.

To make the whole thing stay coherent, we need a morphism (actually an isomorphism) $F(x) \rightarrow G(x)$.

If we insist that there is a natural transformation $F \Rightarrow G$ then this is a guarantee that the compiler keeps doing the right thing even in the intermediate state of refactoring.

This kind of semantics preservation is exactly what refactoring means I think.

ww (Mar 15 2026 at 17:02):

Matteo Capucci (he/him) said:

And how did Claude leverage this fact to constrain the edits? :thinking:

It did this by including in its plan unit tests that checked (not with total coverage so not perfectly, but enough to be useful) that the naturality continued to hold throughout the process.

The actual execution of the plan diverged though because of bugs in $F$ which mean that we didn't actually want a natural transformation. But that also means that it wasn't a true, bug-for-bug, refactor.

John Baez (Mar 15 2026 at 18:03):

So you or Claude caught the bugs in $F$ when trying to do the refactor? Was $F$ a functor despite the bugs?

Ryan Wisnesky (Mar 15 2026 at 18:04):

if one's theories are categories and one's models/implementations are functors, then according to the original functorial semantics ideas I would expect that one's model morphisms to indeed be exactly the natural transformations. I think it would be more surprising if Claude said a model morphism wasn't a natural transformation (maybe it is extra natural or two natural transformations or something else entirely)

ww (Mar 15 2026 at 19:08):

John Baez said:

So you or Claude caught the bugs in $F$ when trying to do the refactor? Was $F$ a functor despite the bugs?

It actually kept trying to replicate the bugs and I kept telling it to stop!

This is one area where it loses sight of what the "right" thing to do is.

$F$ ought to have been a functor but it's really impossible to tell because in the original implementation there was no explicit operational semantics to define it. That was the problem that led to the refactoring exercise.

Its replacement, $G$, has such a definition.

John Baez (Mar 15 2026 at 19:51):

Okay. Now you should do another refactor from $G$ to $H$ and demand that it be a natural transformation, just to give a flawless example of this methodology. :wink:

ww (Mar 16 2026 at 07:08):

You joke, but there are two reasonable choices of message queue system for the implementation: ZeroMQ and nanomsg. ZeroMQ is more well known and has Ocaml bindings so I chose that path, reasoning that it was a big enough piece of work to get rid of $F$ and write $G$ properly. nanomsg is lighter and better designed so is a better choice but it needs bindings written. So at some point, I may do that.

Matteo Capucci (he/him) (Mar 16 2026 at 09:16):

Oh, I see now. So it is indeed a thing in the codebase, not at the codebase level: you checked that two implementations are semantically equivalent by exhibiting an explicit certificate, in the form of an isomorphism of models.