are a very useful mechanism to write programs on
abstract structures and support notational abuse by
overloading. That's ample good reason to have them in a
proof-assistant like Coq. I implemented with Nicolas Oury
a port of type classes in Coq [1
and some libraries using the system:
of the Haskell prelude,
of category theory
and the beginning of order
If you would like to take any of these to the next step or have any
kind of reaction after seeing them I will gladly answer your mail.
I've also given some talks about classes and setoid rewriting
First-Class Type Classes
. Matthieu Sozeau & Nicolas Oury. Otmane Ait Mohamed, César Muñoz and Sofiène Tahar (Eds). Volume 5170 of LNCS
, August 2008, pp.278-293.