The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Wed, 02 Nov 2011 03:32:54 +0400,
Victor Porton 
<porton AT narod.ru>
 a écrit :

> 02.11.2011, 02:16, "Jelle Herold" 
> <jelle AT defekt.nl>:
> 
> >  On Nov 1, 2011, at 10:38 PM, Victor Porton wrote:
> >>   What is the difference between type classes and dependent
> >> records?
> >  I'm am by no means an expert, but I'm pretty sure they will join
> > this discussion soon enough to correct my mistakes :)
> 
> http://coq.inria.fr/cocorico/TypeClasses :
> 
> When you define a type class using Class, all of its members will be
> declared such that the argument for the instance is implicit. If you
> would prefer that this were not the case, simply use Structure
> instead. They are identical except for this one difference.
> 
> And in Coq reference it is said:
> 
> Structure is a synonym of the keyword Record.
> 
> Thus the only difference is presence of implicit arguments. Right?
> What experts can say?
> 
> --
> Victor Porton - http://portonvictor.org

Not exactly, with the keyword "Class" comes the keyword "Instance".

Often when you use implicit arguments, that means it can be inferred in
only one way.

For instance, consider this type:

forall A (x y:A), eq_ x y -> forall (P:A->Prop), P x -> P y.
(more or less eq_ind's type)

Here, you may want to have A, x, y and P which are implicit, and only
provide "x=y" and "P x".

"x=y" cannot be implicit, from the other arguments, we cannot infer a
proof that x = y.

With the class system, if you have an instance of
"forall A (x y:A), x = y", then you won't have either to provide the
proof "x = y".

This example is not really pertinent, but is simple, for a more complex
example, consider the class of monoids.

Record Monoid (A:Type): Type := {
 law: A -> A -> A;
 assoc: forall a b c, law a (law b c) = law (law a b) c
}
(*Don't care if there is a neutral element*)

Now, law has type:
"forall A, Monoid A -> A -> A -> A"
as you can see, "Monoid A" cannot be inferred.

if you set the "Monoid A" argument as implicit,
when you write "law 7 5", you will have the
"error, cannot infer this type holder" error.

With "Class", this error will occur (under another message, such as
"cannot solve the constraints ...") if you have no instance for the
current types.

But with:

Instance NatMonoid: Monoid nat := {law:=plus}.
 (* here the proof, something like, "exact plus_assoc." *)
Defined.

then you can write "law 7 5", and it will guess that the monoid is
"NatMonoid".

Note that it is generally a bad idea to have two instances of
"Monoid nat", since you cannot tell which one is in use.

See also the Haskell language, from which Coq has some similar
mechanics.