The Coq mailing list

[Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr>]

Hello,
> Are there any developments in Coq (or any other proof assistant)
> which use more than one category-theoretic category in some
> interesting way, and yield a useful program?
>   
Nothing finished that I know of, but I'm currently developping a very 
category-theoretic program. Namely a CAS for homological algebra. The 
general pattern is that I use categories as data abstractions over 
structures (additive categories are apparently sufficient to develop all 
effective homological algebra, but can be instantiated with a large 
variety of structures).

This is the most obvious use of categories for programming.
> What I am getting at is: can more than one category be useful in
> programming (as opposed to merely doing mathematics)?
>   
Depending on what you mean by "merely doing mathematics", the answer 
above can be a positive answer or not.

However there is a more specific answer, categories also allow to define 
generic notions of (finite) "products", "sum", "initial" and "terminal" 
object. Any categories which have all these contain all the recursively 
defined datatypes (vectors, option type, Chris Okasaki's binary lists 
defined recursively over binary natural numbers...), you need more 
assumptions to have the inductively defined datatypes (like lists) but 
it's also possible.

Using "categorical datatypes" of this sort allow to define generically 
many actual datatypes.

My main example (I haven't dug very far in it) is C's option type. In C, 
functions like "find the first occurence of character c in string s" 
return a positive integer. But as they can fail, they also can return -1 
as a failure case. This is generally considered bad practice when you 
can define "int option" (or even better "nat option") which gives you 
much more information. Arguably the option type has the drawback of 
being slower to use than a plain integer. However in every category 
which has all finite sums and an initial element, We can define A option 
as being A+0 . The category of all integer intervals is such a category, 
thus it has an option type (which if written properly can make "nat"+0 
be exactly [| -1, +infinity |] ). Thus you can program in the 
potentially faster C style without sacrifying type safety or genericity.

Well this is a bit theoretical at this point, but I hope to be able to 
give it more precise meaning sometimes.
> If we take a subcategory of the Set category, we can define, for
> example, monad type constructors which only obey the monad laws for
> certain arguments (those denoted by the objects of the subcategory).
> However, I am not aware of any such "partial monads" being used
> anywhere.
>   
It's most likely because it's not possible in conventional languages. 
But I can't think of an example for this particular case.



Arnaud Spiwack