The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

2010/10/12 Aaron Bohannon 
<bohannon AT cis.upenn.edu>:
> Speaking of which...if anybody is willing to elaborate on when to use
> "Superclasses" (ch. 18.4.1) as opposed to "Substructures" (ch.
> 18.4.2), I would be very interested to hear about that.  I could be
> terribly mistaken, but they seem to accomplish pretty much the same
> thing.

You're not mistaken, they accomplish pretty much the same thing but
with an important nuance nonetheless. This choice is not limited to
superclasses and substructures, but it happens also for regular
parameters.
Consider a class of Monoid, should you put the carrier domain A of the
monoid as a member of the class or as a parameter ?

Class Monoid (A : Type) := {
  op : A -> A -> A;
  neutral : A;
  op_assoc : .... ;
  op_neutral : ...
}.

vs

Class Monoid := {
  A : Type;
  op : A -> A -> A;
  neutral : A;
  op_assoc : .... ;
  op_neutral : ...
}.

Replace A by a typeclass parameter, and you get superclasses in the
first case, and substructures in the second. The latter also
corresponds to the so-called "telescope" design.

The main practical difference is that contrarily to modules, there is
no "with" constraint for typeclasses, and therefore the only way to
constrain a member of a typeclass is to have it as a parameter. This
is natural for [Monoid] above, since you may want to write functions
which take two monoids with the same carrier or something like that.
It is less intuitive wth typeclass parameters, but it certainly
happens. In the example [Ord '{EqDec A}] from the documentation, there
could be several different EqDec for the same A, and you may want to
write functions that compare two Ord for the same equality.

HTH,

Stéphane
-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06