Paul Govereau wrote:

Class definitions (including constraints and defaults) are essentially (syntactic) theory signatures (as in Institutions, from Goguen, Burstall, and later many others). And, as Oleg has pointed out some months back, Haskell's classes have a close relationship to Ocaml's Functor and Modules. Learning from what they have learned:

1) theory signatures form a category, and have 'natural' operations defined on them. Addition, intersection, union, subtraction are amongst them, as is renaming. They are all very useful operations on specifications, so they ought to be available on class definitions as well.

2) A recent proposal to extend the language of Modules, co-authored by a certain Paul Goverau (see http://www.eecs.harvard.edu/~nr/pubs/els-abstract.html) advocates something quite similar for ML!

I firmly believe that there is a translation of all of the proposals in the above (via Oleg's work) into equivalent proposals for Haskell. Which I would certainly like to see happen.

I would recommend making sure that all the transformations available in Specware (http://www.specware.org/) be reviewed as well. They overlap A LOT with the ones in (2) above, but I do not think the coverage is complete.

Jacques