型クラスはレコードである

概要

Coqの型クラスはレコード。普通の型と同様に使える。

まとめ

リファレンスマニュアル(Chapter18)では分からないことがあったのでまとめておく。
リファレンスマニュアルには、quick referenceしか載せないから参考文献を読め、と書いてある。

Matthieu Sozeau and Nicolas Oury: First-Class Type Classes. In TPHOLs '08, 2008.

この文献は2008年の論文で、型クラスはCoqにあるもので表現できるのでそう実装したよ、ということが書いてある。まとめると、

1. 型クラスとインスタンスは、dependent record型とその型をもつレコード(term)である。
2. クラスメソッドはインスタンス(レコード型のterm)を取って1つのフィールドを返す射影関数である。インスタンス(および必要なパラメータ)についてimplicitなので、インスタンスを書かずとも(implicitな引数が全て推論できれば)呼びだすことができる。
3. Instance宣言によってヒントデータベースtypeclass_instancesにインスタンスをapplyしろ、というヒントが追加される。このヒントはメソッドが呼び出されたときに自動tacticがインスタンスを探索するために使われる。

これらのことをリファレンスマニュアルの例(二項関係の反射律、推移律、前順序)で確認してみた。

知ったこと、わかったこと

• メソッドが1個の場合、型クラスをレコードではない型として定義できる。

(リファレンスマニュアルにはsingleton classと書いてある。)
インスタンスはtermで与えてもよいし、tacticでもつくることができる。

• 型クラス(レコード型)のコンストラクタは明示的に指定しない場合

Build_(typename)になる。
Instance宣言ではなぜかこのコンストラクタを使ってtermを与えることができなかった。Definitionなら通ったし、問題ないと思うのだけれど。

• あるクラスのメソッドの型が型クラスの場合、 ":"ではなく":>"を使うことで

クラスメソッドが内側インスタンス解決のためのヒントデータベースに登録される。
(この例では、Print Hint Reflexiveでapply PreOrder_Reflexive(1)が見えることから
PreOrderのクラスメソッドPreOrder_ReflexiveがReflexive解決に使われるとわかる)

• (Hintコマンドと同じく)Instance宣言でヒントデータベースに追加されたヒントは

宣言されたセクションのみで有効。
グローバルにしたい場合はGlobal Instanceコマンドを使う。

確認用ソースコード

Definition relation (A : Type) := A -> A -> Prop.

Class Reflexive (A : Type) (R : relation A) :=
  reflexivity : forall x, R x x.

Print Reflexive.
(* A singleton class is another name for 
a (parametrized) type *)
(* 
Reflexive = 
fun (A : Type) (R : relation A) => forall x : A, R x x
     : forall A : Type, relation A -> Prop
 *)

Print reflexivity.
(* A method is a instance itself for a singleton class *)
(*
reflexivity = 
fun (A : Type) (R : relation A) (Reflexive : Reflexive A R) =>
  Reflexive
     : forall (A : Type) (R : relation A),
       Reflexive A R -> forall x : A, R x x
*)

Class Transitive (A : Type) (R : relation A) :=
  transitivity : forall x y z, R x y -> R y z -> R x z.

Class PreOrder (A : Type) (R : relation A) :={
  PreOrder_Reflexive :> Reflexive A R ;
  PreOrder_Transitive :> Transitive A R }.

Print PreOrder.
(* A type class is a record type. *)
(* Record type has one constructor named Build_(typename) *)
(* Record PreOrder (A : Type) (R : relation A) : Type :=
   Build_PreOrder
  { PreOrder_Reflexive : Reflexive A R;
    PreOrder_Transitive : Transitive A R }
*)

Print PreOrder_Reflexive.
(* A method is a projection function *)
(* The method takes an instance as an implicit argument *)
(*
PreOrder_Reflexive = 
fun (A : Type) (R : relation A) (PreOrder0 : PreOrder A R) =>
let (PreOrder_Reflexive, _) := PreOrder0 in PreOrder_Reflexive
     : forall (A : Type) (R : relation A), PreOrder A R -> Reflexive A R

Arguments A, R, PreOrder are implicit and maximally inserted
*)

(* no instance *)
(*
Definition t_112 : 1 + 1 = 2 := reflexivity 2.
*)

Section eq_reflexive.
Instance eq_reflexive (A : Type) : Reflexive A (@eq A) :=
  fun x => refl_equal x.
End eq_reflexive.

(* Though an instance is a global term, *)
Print eq_reflexive.

(* The effect of the instance declaration is 
  limited to in the enclosing section.*)
(*
Definition t_112 : 1 + 1 = 2 := reflexivity 2.
*)
Existing Instance eq_reflexive.

(* Implicit arguments are resolved thanks to declared instance *)
Definition t_112 : 1 + 1 = 2 := reflexivity 2.

(* Tactic is OK *)
Instance eq_reflexive2 (A : Type) : Reflexive A (@eq A). 
unfold Reflexive; reflexivity.
Defined.

(* "Definition" doesn't register instances *)
Definition eq_reflexive3 (A : Type) : Reflexive A (@eq A) :=
  fun x => refl_equal x.
Existing Instance eq_reflexive3.

Instance eq_transitive (A : Type) : Transitive A (@eq A) :=
  fun x y z xey yez => match yez in (_ = t) return x = t with
                                    refl_equal => xey
                                  end.

Instance eq_transitive2 (A : Type) : Transitive A (@eq A).
unfold Transitive.
intros.
rewrite H.
assumption.
Defined.

Instance eq_preorder (A : Type) : PreOrder A (@eq A) :={
  PreOrder_Reflexive := eq_reflexive A;
  PreOrder_Transitive := eq_transitive A
}.

(* One cannot use constructor for instance declaration, *)
(*
Instance eq_preorder2 (A : Type) : PreOrder A (@eq A) :=
  Build_PreOrder A (@eq A) (eq_reflexive A) (eq_transitive A).
*)

(* though it is allowed for Definition command *)
Definition eq_preorder2 (A : Type) : PreOrder A (@eq A) :=
  Build_PreOrder A (@eq A) (eq_reflexive A) (eq_transitive A).
Existing Instance eq_preorder2.

Instance eq_preorder3 (A : Type) : PreOrder A (@eq A).
intro; constructor.
apply eq_reflexive.
apply eq_transitive.
Defined.

(* Thanks to substructure (:>) declaration,
one can use reflexivity and transitivity
  when there is a PreOrder instance *)
Definition preorder_test {A}{R} {pre : PreOrder A R} :=
  @reflexivity A.

Definition preorder_test2 {A}{R}{pre : PreOrder A R} :=
  @transitivity A.

(*  Instances are registered as hints
  by Instance or Existing Instance command. *)
Print Hint Reflexive.
(*
...
In the database typeclass_instances:
  apply eq_reflexive3(0)
  apply eq_reflexive2(0)
  apply eq_reflexive(0)
  apply PreOrder_Reflexive(1) 
...
*)
Print Hint PreOrder.
(*
...
In the database typeclass_instances:
  apply eq_preorder3(0)
  apply eq_preorder2(0)
  apply eq_preorder(0) 
...
*)