The Coq mailing list

[Noam Zeilberger <noam+ AT cs.cmu.edu>]

On Mon, Jul 07, 2008 at 05:36:55PM +0100, Robin Green wrote:
> What I am getting at is: can more than one category be useful in
> programming (as opposed to merely doing mathematics)?

I'm not sure if this is what you meant, but indeed, Paul Levy's theory
of call-by-push-value is all about how working in at least two
categories (forming an adjunction) can be very useful for programming.
I've played with embeddings of a very similar language in Coq and Agda
(which you can find on my webpage), but came to the language from
proof-theoretic rather than categorical principles -- so the multiple
categories are lurking in there somewhere, but they're not explicit.

Also Deepak Garg once showed me how the programming language defined
in Pfenning and Davies' "A judgmental reconstruction of modal logic"
is most naturally interpreted with (pure) "terms" living in one
category and (effectful) "expressions" living in a Kleisli category.
In general I think Frank Pfenning et al's work on "the judgmental
method" is all about how working with more than one category is very
useful in logic and programming, but most of that work has not been
explicitly related to category theory.

Noam