Type inference with type classes in Coq

Question

I don't understand type classes in Coq. I tried to use them as follows. I have a type cat that is supposed to represent the type of categories and I define the type class cat_Binary_products that is supposed to represent the type of categories with binary products. I define the function conj_system that forgets some structure on categories with binary products. Finally, I define the type cat_with_FPof categories with finite products. Essentially, every category with finite products is a category with binary products, so I should be able to use my conj_system function on such categories:

Variable ℭ : cat. 

Class cat_Binary_products := {
  prod : ∀ (A B : ℭ), product A B;
}. 

Definition conj_system  (𝔇 : cat_Binary_products) : conjunction_system := ...

Record cat_with_FP := {
  binary_prod : cat_Binary_products;
  one : terminal ℭ;
}.

#[global] Instance cat_Bin_from_FP (𝔇 : cat_with_FP) : cat_Binary_products :=
  {
    prod := @prod (binary_prod 𝔇);  
  }.

Variable 𝔇 : cat_with_FP. 
Variable A : conj_system (cat_Bin_from_FP 𝔇). 

But I don't see the point to use type classes if I have to write cat_Bin_from_FP explicitly here, I thought that the point of type classes was that I should be able to write instead

Variable A : conj_system 𝔇. 

and Coq was able to infer that 𝔇 is an instance of cat_Binary_products but I get the error message

The term "𝔇" has type "cat_with_FP" while it is expected to have type "cat_Binary_products".

Answer 1

The way to use type classes is to think of them as additional structure on original structure, and not a larger structure that contains the original one.

Let's explain this with a simple example first. A pointed type is given by a carrier type A and an element a : A, called the point. We can formalize this in two ways.

The first one is display map:

Structure Pointed : Type := {
  carrier :> Type ;
  point : carrier
}.

The second one is a fibration:

Structure Pointed (A : Type) := {
  point : A
}.

(Note: the terimonology comes from category theory. In the first way we think of the structure Pointed displayed over Type by the projection carrier. In the second way we think of Pointed as a fibration that assigns to each type A the type of structures Pointed A.)

Whether one should use display maps or fibrations in a given situation depends on the situation. Type classes work well with fibrations, while display maps work better with coercions and canonical structures.

So in your case we should be using the fibered approach: a category with finite products is a category C together with a fibration FinProd : C → Type that assings to each C the type of all finite-product structures on C, and similarly for other structures of interest.

This leads to the following formalization style:

(* All definitions are incomplete, but they convey the message. *)

(* The structure of categories. *)
Structure Category : Type := {
    obj :> Type ;
    hom : obj -> obj -> Type
}.

Arguments hom {_} _ _.

(* The terminal object on a category. *)
Class Terminal (C : Category) := {
    one :> C ;
}.

(* The type class of binary-product-structures on a given category. *)
Class BinProd (C : Category) : Type := {
    prod : C -> C -> C
}.

(* Finite products structure on a category. *)
Class FinProd (C : Category) : Type := {
    list_prod : list C -> C
}.

(* Conversion from finite-product structure to binary structure. *)
(* Note the backquote mechanism, which instructs the instance       *)
(* mechanism that the argument can be filled in automatically.   *)
Instance BinProd_FinProd {C : Category} {FP : FinProd C} : BinProd C :=
  {| prod := fun x y : C => list_prod (x :: y :: nil) |}.

(* Conversion from finite-product structure to terminal object. *)
Instance Terminal_FinProd {C : Category} {FP : FinProd C} : Terminal C :=
  {| one := list_prod nil |}.


(* To test how things work, let's also imagine a third structure
   called "conjunction system" that is formalized in the "display map"
   style. *)
Class ConjunctionSystem (C : Category) := {
  carrier : Type ;
  conj : carrier -> carrier -> carrier
}.

(* Every binary product category can be converted to a conjunction system. *)
Instance ConjunctionSystem_BinProd {C : Category} {BP : BinProd C} : ConjunctionSystem C :=
  {| carrier := C ; conj := prod |}.

Section Example.
  (* Suppose we have a category C. *)
  Variable (C : Category).

  (* Suppose C has a finite product structure. *)
  Variable (FP : FinProd C).

  (* Then the category has a terminal object and binary products.
     We can simply mentioned them. *)
  Lemma cow : forall a, prod a one = one.
  Proof.
    intro a.
    (* let us verify that Coq deduced prod and one from FP. *)
    unfold one, prod, BinProd_FinProd, Terminal_FinProd.
    (* We cannot finish this proof, it's only a demo. *)
  Admitted.

  (* Conjunction system on C is derived automatically, so we can
     mention conj wherever we like. *)
  Definition dog x := conj x x.

  (* The tactic typeclasses eauto finds instances for us. *)
  Definition parrot : ConjunctionSystem C.
  Proof.
    typeclasses eauto.
  Defined.

  (* Of course, we can also use them explicitly. Note that we
     do not have to provide any arguments, they are derived. *)
  Definition eagle : ConjunctionSystem C := ConjunctionSystem_BinProd.

End Example.

The instances tell Coq things like "this is how you get BindProd C from FinProd C, and this is how you get Terminal C from FinProd C". What the instances cannot do is "if you need structure CowStomach and you have a structure Cow which contains CowStomach as a field, just project the field" (that would be a display map approach).

Answer 2

If you want to use 𝔇 to mean cat_Bin_from_FP 𝔇, the relevant feature is coercions, not type classes.

Record cat_with_FP := {
  binary_prod :> cat_Binary_products;
  (* ":>" makes binary_prod a coercion from cat_with_FP to cat_Binary_products *)
  one : terminal ℭ;
}.

For more information, see the Reference Manual:

Use :> in the field type to declare the field as a coercion from the record name to the class of the field type.