The Coq mailing list

[David Pichardie <david.pichardie AT inria.fr>]

Here is how I would explain the difference between a  type class and a record.

Best regards,

David.


(* let's define a type class for computable equality tests *)
Class EqDec (A:Type) := {
  eq_dec: forall (x y:A), {x=y}+{x<>y}
}.

Instance EqDec_nat : EqDec nat.
constructor; decide equality.
Qed.

(* if we print EqDec, it's look like a record *)
Print EqDec.

(* but if we define the same as record, there will be a big difference when 
we use the
   field [eq_dec] (see below) *)
Record EqDec' (A : Type) : Type := Build_EqDec'
  { eq_dec' : forall x y : A, {x = y} + {x <> y} }.

Definition EqDec'_nat : EqDec' nat.
constructor; decide equality.
Qed.

(* eq_dec and eq_dec' have the same type *)
Check @eq_dec.
Check @eq_dec'.

(* but Coq uses a more powerfull mechanism to infer the second argument of 
eq_dec *)
Definition eq_nat_dec : forall (x y:nat), {x=y}+{x<>y} := @eq_dec nat _. (* 
Coq is happy *)
Definition eq_nat_dec : forall (x y:nat), {x=y}+{x<>y} := @eq_dec' nat _. (* 
here Coq complains because it can fill the hole itself *)

(* Hope this help *)



Le 1 nov. 2011 à 19:32, Victor Porton 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