Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Generating Compiler Optimizations from Proofs 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?

share|improve this question
add comment

2 Answers 2

The beautiful and by now classic paper Theorems for Free! by Philip Wadler introduces —or rather, very richly elaborates— the idea that the knowledge of the type of a function can be used to discover some of its properties. In that paper, the language is that of typed lambda calculi, but in later work he and others rephrased it, in a very natural way, in the language of category theory (lax natural transformations and such things)

The properties of functions deduced from their types in that way can and are used by compilers of functional languages in the optimization process.

Later. Of course, all the «monad movement» seen in the context of functional languages is also an example, as well as the later «arrow» thing. S. Doaitse Swierstra self-optimizing parser library, which is an unequivocally categorical thing, is an extraordinary example of the abstractions of category theory put to use to deal with real life algorithmic problems.

share|improve this answer
1  
Thanks! The parser example is more in line with what I'm looking for. I'm trying to explain the merits of category theory to users of imperative, stateful, dynamically-typed programming languages; their initial impression of monads is a hard-to-understand kludge that's only necessary because of a silly insistence on functional purity. While I'm a big fan of algebraic data types, functional programming, and monads, I'd like applications outside of type theory. –  Mike Stay Feb 21 '12 at 23:12
add comment

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, 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.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.