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 type of ad-hoc polymorphism, enabling us to, for example, reason about all monads using the same theorems.

We, however, should 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 my library practically useless to you if I didn't pick the right definition of any of the above properties.

(GMM: Lots more things to say here)