Type classes 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:
a
port of the Haskell prelude,
a
development of category theory
and the beginning of
order
theory.
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
[
2], [
3].
First-Class Type Classes in
TPHOLs. Matthieu Sozeau & Nicolas Oury. Otmane Ait Mohamed, César Muñoz and Sofiène Tahar (Eds). Volume 5170 of
LNCS.
Springer, August 2008, pp.278-293.
© Springer