[Coq] TypeClass vs Record

CoqでClass/Instance (型クラス) と Record と何が違うの？、というのは私も明確に理解出来てなかったのですが、2011/11/01前後のCoq-Clubの"What are type classes?"というスレッドで色々解説されてます。

まず実装自体は "Type classes are a thin layer on top of dependent records (although some special type classes are actually not records but raw definitions)." らしく、Record の上に構文糖があるみたいなものらしい。

そして、"Type classes allow you to specify an abstract "interface" for which you want the system to *automatically* find an implementation. Hence the main difference: type class instances (terms of a record type) are registered in a special "auto" database. This database is then used to resolve the class requirements you specify in for example a lemma." ということで、抽象的な interface への操作に対しても色々 implicit な実装を自動で探してくれるということみたい。

違いが判りやすいサンプルコードは下記の様になります。

まず EqDec という decidability を持つ Class を定義し、次いで EqDec nat という具体的な instance を定義します。最後に EqDec の定義を見ると実体は単なる Record になっていることが判ります。

Class EqDec (A:Type) := {
 eq_dec: forall (x y:A), {x=y}+{x<>y}
}.
Instance EqDec_nat : EqDec nat.
constructor. decide equality.
Qed.
Print EqDec.
(* Record EqDec (A : Type) : Type := Build_EqDec
  { eq_dec : forall x y : A, {x = y} + {x <> y} } *)

同じことを Record で書きます。

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 と eq_dec' は実際、同じ型を持ちます。

Check @eq_dec.
(* eq_dec : forall A : Type, EqDec A -> forall x y : A, {x = y} + {x <> y} *)
Check @eq_dec'.
(* eq_dec' : forall A : Type, EqDec' A -> forall x y : A, {x = y} + {x <> y} *)

しかし実際に使うときの自動推論の能力に違いが出ます。

Definition eq_nat_dec :  forall (x y:nat), {x=y}+{x<>y} := @eq_dec nat _. 
Print eq_nat_dec.
(* eq_nat_dec = eq_dec : forall x y : nat, {x = y} + {x <> y} *)
Definition eq_nat_dec :  forall (x y:nat), {x=y}+{x<>y} := @eq_dec' nat _.
(* Error: Cannot infer this placeholder. *)

これを見る限り、使い方 (interface/implementationの分離にtype classを使う) とかを別にすると、実装的には単に便利な自動推論がついているだけ、ということみたいです。 あと、この発表資料はCoqにおけるType Classの良い説明かも。 http://mattam.org/research/publications/First-Class_Type_Classes-TPHOLs-200808.pdf