Using Category Theory to Design Implicit Conversions and Generic Operators

Using Category Theory to Design Implicit Conversions and Generic Operators, John C. Reynolds, 1980. (Try this if the official link doesn't work.)

A generalization of many-sorted algebras, called category-sorted algebras, is defined and applied to the language design problem of avoiding anomalies in the interaction of implicit conversions and generic operators. The definition of a simple imperative language (without any binding mechanisms) is used as an example.

This is an old, but still cute, paper. The basic intuition is that a good design principle for a language with implicit conversions is that whatever order of conversions the language takes, you should get the same result. He then formalizes that by giving a category of types and conversions, and demanding that everything commute properly. And these give just the conditions the language designer has to check to make sure that he or she hasn't screwed anything up.

Someone could probably get a fun little paper by taking this idea and shooting some dependent types into it. (Maybe somebody already has?) If you've got an abstract type, a coercion function, and a proof that it satisfies Reynolds' conditions, now your compiler can silently insert those coercions for you as needed, but you can still be sure that it won't mess up the meaning of your program.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Inaccessible

The link is broken and it seems only available via ACM :(

I'm not sure this is related to the conversions Reynolds talk about but I have a system with coercions between particular dependent types (subsets and dependent inductives) and yes its nice once you have your commutation properties but the proof is hard to get in such systems.

Thanks

I mirrored the paper on my web site, and added another link. Let me know if this one has problems too.

Also, your system seems really interesting. What makes the commutation properties hard to prove? Is it just propositional equality being annoying to work with as usual, or is it something more fundamental?

Commutation proof

It's just hard to prove because we have dependencies in types so you actually need unicity of coercions and inverses too. This work by Reynolds seems more related to the coercion mechanisms existing in Coq where there is a notion that coercions must reduce to the identity, though.

Not only identity coercions

This system can be also used for integer widening — at least, Pierce does so in his book on category theory, where this work is used as an example.