The Coq mailing list

[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 :)

Anyway,

The are essentially the same thing, except that they are used for something 
entirely different.

Type classes allow you to specify an abstract "interface" for which you want 
the system to *automatically* find an implementation. Hence the main 
difference: type class instances (terms of a record type) are registered in a 
special "auto" database. This database is then used to resolve the class 
requirements you specify in for example a lemma.

In fact IIRC you can add values for a record to that database yourself and 
essentially get the same thing.

It is explained much better here
http://mattam.org/research/publications/First-Class_Type_Classes-TPHOLs-200808.pdf

The basic example there is this,

(* define some class of numbers with a zero and one element and a plus 
operation. *)
Class num α :=
  { zero : α
  ; one  : α
  ; plus : α → α → α
  }.

(* we now define two different instances of num *)

Instance nat_num : num nat :=
  { zero := 0 % nat
  ; one  := 1 % nat
  ; plus := Peano.plus
  }.

Require Import ZArith.

Instance Z_num : num Z :=
  { zero := 0 % Z
  ; one  := 1 % Z
  ; plus := Zplus
  }.

(* introduce some notations *)
Notation "0" := zero.
Notation "1" := one.
Infix "+" := plus.

(* here the system automatically finds the correct instance *)
Check (λ x : nat, x + (1 + 0 + x)).
Check (λ y : Z, y + (1 + 0 + y)).

So the statement "x + (1 + 0 + x)" is implicitly parametrized by an instance 
of num, which is then automatically resolved.

Another way we use this often, is like the following (I just picked something 
random)

https://github.com/0x01/math-classes/blob/master/src/theory/groups.v#L70

Section groupmor_props.
  Context `{Group A} `{Group B} {f : A → B} `{!Monoid_Morphism f}.
  (* ^^ here we implicitly parametrize the next lemma with two groups, and 
some more stuff...
        Because these are classes, coq will automatically try to resolve the 
instances.
        
        Of course you can use @preserves_negate to specify the instances 
yourself or
        use (A := ..) to specify an otherwise implicit parameter
  *)

  Lemma preserves_negate x : f (-x) = -f x.
  Proof.
    apply (left_cancellation (&) (f x)).
    rewrite <-preserves_sg_op.
    rewrite 2!right_inverse.
    apply preserves_mon_unit.
  Qed.
End groupmor_props.


This is more or less how I understand it, but I'm happy to see better 
examples, etc.

HTH,
Jelle.