Из того, что я знаю, класс типов в Coq - это "почти" запись, с магией вокруг вывода типов.
Хотя я не знаю никого, кто бы сказал это явно, у меня есть чувство классов типовможет делать то, что могут делать записи.
Однако это чувство привело меня к некоторой проблеме с аксессорами класса type, которые кажутся стандартными для записи:
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).
Интересно, что getter_r и getter_t имеет очень похожую сигнатуру функции, и тот факт, что Foo_t действительно является записью:
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 *)
Могу ли я спросить, концептуально ли это дизайнерское решение?запретить средства доступа для класса типа?или я просто неправильно его использую?спасибо.