In "Compiling to Categories" what he’s doing is translating lambda forms into a kind of “point-free” style and then showing how to instantiate that code over different categories to get several different kinds of program out of the same code.
I've been working with a stack-based "concatinative" language called Joy which I think makes this stuff a lot clearer. Joy code is already in "point-free" style (no vars, no lambdas) and it includes functions that do the same job as but are more elegant than the triangle operators and others in the "squiggol" tradition. ( https://wiki.haskell.org/Pointfree )
There's a little bit in "Mathematical foundations of Joy"[1] and "The Algebra of Joy"[2] by Manfred von Thun.
Here's a piece of Joy code (it's part of an ordered binary tree library):
pop swap roll< rest rest cons cons
Here's a trace of its evaluation (with a suitable value already on the stack) in the category of values resulting in a computation of an answer. The dot is the "interpreter head", the current point of evaluation: [4 5 ...] 3 2 1 . pop swap roll< rest rest cons cons
[4 5 ...] 3 2 . swap roll< rest rest cons cons
[4 5 ...] 2 3 . roll< rest rest cons cons
2 3 [4 5 ...] . rest rest cons cons
2 3 [5 ...] . rest cons cons
2 3 [...] . cons cons
2 [3 ...] . cons
[2 3 ...] .
And here's the same code evaluated in a category of composition of stack effects resulting in a description of the stack effect of the expression: (--) ∘ pop swap roll< rest rest cons cons
(a1 --) ∘ swap roll< rest rest cons cons
(a3 a2 a1 -- a2 a3) ∘ roll< rest rest cons cons
(a4 a3 a2 a1 -- a2 a3 a4) ∘ rest rest cons cons
([a4 ...1] a3 a2 a1 -- a2 a3 [...1]) ∘ rest cons cons
([a4 a5 ...1] a3 a2 a1 -- a2 a3 [...1]) ∘ cons cons
([a4 a5 ...1] a3 a2 a1 -- a2 [a3 ...1]) ∘ cons
([a4 a5 ...1] a3 a2 a1 -- [a2 a3 ...1]) ∘
If you compare the input and output of the first one you'll see that it matches the input and output stacks in the Forth-style stack effect comment computed by the second one.To repeat, that's the same code evaluated in two different domains, er, Categories, to get two different correct computations.
If I had implementations for them I could evaluate the expression in/over a category and get as output: a dataflow diagram of the program, or a hardware description of a circuit for the program, which are examples from Elliott's talk+paper.
[0] https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
[1] http://www.kevinalbrecht.com/code/joy-mirror/j02maf.html
[2] http://www.kevinalbrecht.com/code/joy-mirror/j04alg.html
Unfortunately, her insights have been largely ignored. I first heard about it twenty years ago in a book called "System Design from Provably Correct Constructs" (which, oddly enough, doesn't mention Hamilton outside of a few references in the back.)
In modern terms, programs in HOS are developed by the direct elaboration of the Abstract Syntax Tree (like Lisp code) using only a limited set of operations which each preserve the semantic correctness of the tree. In this way, you are prevented from building incorrect software.[1]
(You might build a barn instead of a pool, but it will be a fine barn.[2])
In addition to the availability of a defect-free development methodology, Category Theory provides a solid mathematical foundation for determining the most-highly-factored form(s) of a given code-base. Meaning, if you have a "categorical" programming language you can more-or-less automatically extract the most general form of your program, which can then be used "over" different categories to get different concrete programs from one piece of code, with confidence (mathematical confidence) that they are valid, correct programs. There's now a great explanation by Conal Elliott about this called "Compiling to Categories"[3].
In any event, I would say that Category Theory gives us a language-agnostic way to rigorously define the "cleanliness" or "beauty" of software.
The tools are there. We have to notice them and pick them up.
[0] https://en.wikipedia.org/wiki/Margaret_Hamilton_%28scientist...
[1] You're not editing text files and then using other tools to (try to) ensure they're not broken too badly. No linters, no formatters, no syntax errors, no type conflicts, no off-by-one errors, etc... Hamilton identified all the sources of error in program construction and designed a system that eliminated them.
[2] "'Tis a fine barn but 'tis no pool, English."
[3] "Compiling to Categories" Conal Elliott February 2017 http://conal.net/papers/compiling-to-categories/