CODEWITHSUNDEEP
coqtypeclass
Zheng Cheng
Zheng Cheng

Reputation: 400

Accessors of type class?

from what I know, a type class in Coq is "almost" a record, with magic around for type inference.

Although I am not aware anybody saying it explicitly, I have the feeling of type classes can do whatever records can do.

However, this feeling lead me to some problem with accessors of type class, which seems standard with record:

Require Import List. 
Set Printing All.
Set Implicit Arguments.

(* Record version that works: *)

Record Foo_r (A_r: Type) := { getter_r : list A_r; }.   
Definition foo_r : Foo_r nat := {| getter_r := 2::nil |}.
Compute (getter_r foo_r).

(* Type class version that does not work: *)

Class Foo_t (A_t: Type) := { getter_t : list A_t; }.   
Instance foo_t : Foo_t nat := {| getter_t := 2::nil |}.
Compute (getter_t foo_t).

It is interesting that getter_r and getter_t have a very similar function signature, and the fact that Foo_t is indeed just a record:

Print getter_r.
(* fun (A_r : Type) (f : Foo_r A_r) => let (getter_r) := f in getter_r
 : forall A_r : Type, Foo_r A_r -> list A_r *)

Print getter_t.
(* fun (A_t : Type) (Foo_t0 : Foo_t A_t) => let (getter_t) := Foo_t0 in getter_t
 : forall A_t : Type, Foo_t A_t -> list A_t *)

May I ask that, conceptually, is this a design decision to disallow accessors for type class? or I just use it wrong? thanks.

Upvotes: 2

Views: 77

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15424

If you check the type of getter_t using About getter_t. you will see:

getter_t : forall (A_t : Type) (_ : Foo_t A_t), list A_t

Arguments A_t, Foo_t are implicit and maximally inserted

Foo_t is maximally inserted, meaning that if you just mention getter_t with no further information, Coq should be able to infer the argument of this type. In other words, saying

Compute getter_t foo_t.

is the same as 

Compute @getter_t _ _ foo_t.

which is not correct because @getter_t takes only two arguments (@-notation means "I'm going to list all the arguments, including the implicit ones").

You can say

Compute @getter_t _ foo_t.

Or just 

Compute getter_t.

Upvotes: 4

Related Questions