Multiple Typeclass Inheritance in Coq

Question

I've been trying to create a small typeclass hierarchy in Coq and I haven't been able to progress despite there being a few answers on stackoverflow that I thought would be the solution, particularly Building a class hierarchy in Coq?.

Here is what I have:

Class Unfoldable (C : Type -> Type) (A : Type)
  (insert : A -> C A -> C A)
  (empty : C A) : Type :=
{
  insert_neq : forall (x y : A) (h : C A),
    insert x h <> insert y h -> x <> y;
  empty_insert_eq : forall x y : A,
    insert x empty = insert y empty <-> x = y
}.

Class Foldable (C : Type -> Type) (A B : Type)
  (foldr : (A -> B -> B) -> B -> C A -> B) : Type :=
{
  (* Foldable properties??? *)
}.

Class Collection C A {B} insert empty foldr
  `{F : Foldable C A B foldr}
  `{U : Unfoldable C A insert empty} :=
{
  collection_id : forall h,
    foldr insert empty h = h
}.

Print Collection.

And here is the error message:

Error:
In environment
Collection :
forall (C : Type -> Type) (A B : Type) (insert : A -> C A -> C A)
  (empty : C A) (foldr : (A -> B -> B) -> B -> C A -> B),
Foldable C A B foldr -> Unfoldable C A insert empty -> Type
C : Type -> Type
A : Type
B : Type
insert : A -> C A -> C A
empty : C A
foldr : (A -> B -> B) -> B -> C A -> B
F : Foldable C A B foldr
U : Unfoldable C A insert empty
h : ?17
The term "insert" has type "A -> C A -> C A"
 while it is expected to have type "A -> B -> B".

Shouldn't C A have a type of Type and therefore fit as B?

Sorry about not being able to provide more information. I really don't know Coq well. Thanks for any help.

Answer 1

I don't know much about type classes myself, but doesn't B need to be variable? By separating it from foldr, you're making it fixed. I think it only makes sense to make C and A fixed.

Class Foldable (C : Type -> Type) (A : Type)
  (foldr : forall B, (A -> B -> B) -> B -> C A -> B) : Type :=
{
  (* Foldable properties??? *)
}.

Class Collection C A insert empty foldr
  `{F : Foldable C A foldr}
  `{U : Unfoldable C A insert empty} :=
{
  collection_id : forall h, foldr (C A) insert empty h = h
}.

If you really want B fixed, you have to set it to C A because that's what insert and empty return, but you shouldn't want B to always be C A.

Class Collection C A insert empty foldr
  `{F : Foldable C A (C A) foldr}
  `{U : Unfoldable C A insert empty} :=
{
  collection_id : forall h, foldr insert empty h = h
}.

By the way, insert_neq is always provable.

Axiom C : Type -> Type.
Axiom A : Type.
Axiom empty : C A.
Axiom insert : A -> C A -> C A.

Goal forall (x y : A) (h : C A), insert x h <> insert y h -> x <> y.
intros ? ? ? H1 H2.
apply H1.
rewrite H2.
apply eq_refl.
Qed.

---

Update:

In your original code, you have something similar to the following.

Axiom C : Type -> Type.
Axiom A : Type.
Axiom B : Type.
Axiom insert : A -> C A -> C A.
Axiom empty : C A.
Axiom foldr : (A -> B -> B) -> B -> C A -> B.
(* Foldable properties??? *)
Axiom insert_neq : forall (x y : A) (h : C A), insert x h <> insert y h -> x <> y.
Axiom empty_insert_eq : forall x y : A, insert x empty = insert y empty <-> x = y.

Axiom collection_id : forall h : C A, foldr insert empty h = h.

This last axiom is ill-typed because foldr returns a B, not a C A. There are no guarantees that they can be the same thing.

Unless B has any particular properties, you can just make foldr polymorphic.

Axiom C : Type -> Type.
Axiom A : Type.
Axiom insert : A -> C A -> C A.
Axiom empty : C A.
Axiom foldr : forall B : Type, (A -> B -> B) -> B -> C A -> B.
(* Foldable properties??? *)
Axiom insert_neq : forall (x y : A) (h : C A), insert x h <> insert y h -> x <> y.
Axiom empty_insert_eq : forall x y : A, insert x empty = insert y empty <-> x = y.

Axiom collection_id : forall h : C A, foldr (C A) insert empty h = h.

In this case, foldr takes an extra argument: the type it returns. The equivalent to the Haskell type (a -> b -> b) -> b -> [a] -> b, in Coq, is forall a b : Type, (a -> b -> b) -> b -> list a -> b.

The second example I gave is equivalent to the following.

Axiom C : Type -> Type.
Axiom A : Type.
Axiom insert : A -> C A -> C A.
Axiom empty : C A.
Axiom foldr : (A -> C A -> C A) -> C A -> C A -> C A.
(* Foldable properties??? *)
Axiom insert_neq : forall (x y : A) (h : C A), insert x h <> insert y h -> x <> y.
Axiom empty_insert_eq : forall x y : A, insert x empty = insert y empty <-> x = y.

Axiom collection_id : forall h : C A, foldr insert empty h = h.