Philosophy [Use of Type Classes]

Type classes are a mechanism to associated operations with types in a somewhat canonical way (Coq does not enforce the canonicity that people usually think about when they think about type classes). This canonicity properties allows proof-search to be used to construct values for us in a type-directed way completely automatically. This allows us to achieve a principled form of ad-hoc polymorphism, enabling us to, for example, reason about all monads using the same theorems.

Building New Classes

In Haskell, type classes are limited to being indexed by types (thus the name type classes). In Coq, this restriction is completely lifted. "Type" classes are really more like "value" classes because they can be be resolved based on arbitrary values. In general, the library takes the approach of indexing type classes by relations or functions that describe them in a canonical way. For example, the RelDec class is indexed by the relation that it decides:

Class RelDec (T : Type) (R : T -> T -> Prop) : Type :=
{ rel_dec : T -> T -> bool }.

There is no (correctness) ambiguity in this instance, if one uses rel_dec with R as string equality, it doesn't matter what instance is used as long as it is proved correct. If I come up with a faster implementation, I can add it to my code and get the benefits everywhere without changing any of my proofs.

Caution

The "automatic" programming provided by type-classes is tempting, but it is important to not think of type classes as more than they actually are. In particular, there are many potential equivalences, orderings, to_string, etc. operations on a given type and claiming that one of these is THE one and excluding others is generally a bad idea, it would make a library practically useless to you if the library writer didn't pick the right definition of any of the above properties.