[Generating Compiler Optimizations from Proofs](http://cseweb.ucsd.edu/~rtate/publications/proofgen/) is a wonderful paper. The authors say that they were faced with the problem, got stuck, then tried reasoning about it using category theory. They took the obvious tack, isolated the new idea, designed the abstract algorithm, and applied it to their specific case.


What other examples like this do you know of, where category theory clearly had a role in producing a nontrivial algorithm?



Examples of algorithms that came from category theory?
I'm glad you liked the paper. I thought you might like to know that the algorithms for both of my PLDI papers were actually designed using a category-theoretic framework I made for existential types (half of which turned out to be opfibrations, but I didn't know about those at the time). Others have asked to see it, so I'm finally giving in and posting the work-in-progress on my page for [Inferable Object-Oriented Typed Assembly Language](http://cseweb.ucsd.edu/~rtate/publications/italx/), since that's the problem which prompted me to make the framework once I get stuck. Just look for "Inferable Existential Quantification". Hope you like it!


One thing I'll note while I'm at it is that, in my experience, "algorithmic" category theory (as opposed to "type-theoretic" and "semantic" category theory) is largely built on concrete category theory. After all, many algorithms deal with structured sets of some form. Thus the techniques available to an algorithm often depend on whether the concrete category is topological or algebraic rather than whether it is closed. There's lots of stuff showing what kind of structurings preserve things like existence of pushouts and pullbacks, but I think it would be really interesting (and helpful) to also identify what kind of structurings preserve constructability/decidability of pushouts and pullbacks. By knowing that, we could build algorithms for a domain just by showing how the domain can be built from a sequence of constructability-preserving structurings that consequently guarantee the presence of the particular structures required by the algorithm. If anyone happens to already know of such research, I'd be very interested to see it.


