This does not appear to pass the criterion I gave:
> used by someone in a production software setting to solve a problem not related to category theory
If this stuff or its derivative work is used in production in a mainstream compiler (GHC, perhaps?), then I would see it differently.
Re:Applied Category Theory Course
by nextaccountic on Friday September 29, 2023 @02:24PM
(#37708232)
there was a startup that used this to compile functional programs into circuits
not sure if it went anywhere, but it even included self modifying fpga-like circuits iirc
His paper on Compiling to Categories [1] pitches programming language semantics as a cartesian closed category [2] allows for really cool stuff by mapping typical evaluation semantics to alternatives like building a computational graph visualization, a pretty printer, and imbuing the original program with automatic differentiation capabilities purely through the categorical interpretation of the same program. Essentially, if you can formulate a desired output of the program as a cartesian closed category, you can do it quite easily.
[1]: http://conal.net/papers/compiling-to-categories/
[2]: A cartesian category with is a category with an operation that lets you pair things together into a new object and get out the original parts with eliminators. Think construct a tuple and have the ability to get the first and second elements out of the tuple. A cartesian closed category adds in the ability to model (partial) function application to its arguments via "apply, curry, and uncurry." See https://en.wikipedia.org/wiki/Cartesian_closed_category