Coqの型クラスの使い方：バンドル方式とアンバンドル方式 - 檜山正幸のキマイラ飼育記 (はてなBlog)

「Coqで定理を記述してみる、型クラスとか使って」に次のような断り書きを入れました。

ミート半束のような代数構造をどう定義するのが良いのか、あんまり分かってないのですが、まーまー使える方法を紹介します。この方法には課題があることを注意しておきます。今回の目的ではうまくいきますが、より大規模な記述にはもっと効率的な方法が必要かも知れません。

代数構造を定義する別な方法である、スピターズ／ファンデル・ウィーゲンの方式をかいつまんで紹介します。

内容：

Bundling is bad
- 追記：方式の呼び名
オールインワン方式
バンドル方式
アンバンドル方式
何が違うの？
- ソースコード

Bundling is bad

「Coqで定理を記述してみる、型クラスとか使って」では、ミート半束と（最大元付き）順序集合を定義するために、「マグマのクラス」と「法則（公理系）を書いたクラス」を使いました。スピターズ／ファンデル・ウィーゲンの次の論文には、こういう方法はダメだと書いてあります。

Title: Type Classes for Mathematics in Type Theory
Authors: Bas Spitters, Eelis van der Weegen
URL: http://arxiv.org/abs/1102.1323

どこがダメかというと、構造に付随する台集合、演算、定数などをまとめ上げる（バンドルする）のがよろしくない、と。

より具体的に言うと、ミート半束を定義するとき、次のようなマグマ・クラスを定義したじゃないですか。このマグマの定義がバンドリングしたことになっているのです。そして、Bundling is bad（上記論文第3節のタイトル）だと。

Class MeetMagma := 
  {
    meet_carrier: Set;
    meet_operation: meet_carrier -> meet_carrier -> meet_carrier;
    meet_unit: meet_carrier
  }.

マグマの定義は指標（signature）の定義と言ってもいいでしょう。指標をまとめて記述するのは分かりやすいですよね。バンドリング（まとめて記述）の考え方がダメということではなくて、この方法がCoqのメカニズムや制限と相性が悪いところもある、ということなんだと思います。

Coq以外のツール（僕は知らないけど）なら、バンドリングでも問題はないのかも知れません。そうは言っても、Coqで書く限りはそのメカニズムや制限と折り合いを付けないといけないので、スピターズ／ファンデル・ウィーゲンが提唱するような手法・技法も必要なんでしょう。

追記：方式の呼び名

以下で、「オールインワン方式」と「バンドル方式」という呼び名を使っています。スピターズ／ファンデル・ウィーゲンによれば、指標の情報をクラスのフィールドに持たせるのがバンドル方式なので、オールインワン方式は当然にバンドル方式となります。本文は直しませんが、方式の呼び名は次のようにするのが適切でしょう。

オールインワン方式：すべての情報を単一クラス内にバンドルしたバンドル方式
法則分離バンドル方式：指標の情報と法則を別なクラスにしているが、指標はバンドルしている。
アンバンドル方式：指標をフィールドとしてはエンコードしない。クラスへのパラメータとして指標の情報を渡す。

オールインワン方式

例題にモノイドの定義を使います。ノーテーションによる記述の簡素化は重要な課題なのですが、話がややこしくなるので省略します。

まず、モノイドの定義に必要なモノをすべて、クラスのフィールドとして書いてみます。これもバンドル方式の一種ですが、特にオールインワン方式と呼びましょう。

(* === オールインワン方式 === *)

Class MonoidAllInOne :=
  {
    (* モノイドの指標 (A, op, u) *)
    A: Set;
    op: A -> A -> A;
    u: A;
    
    (* モノイドの法則 *)
    assoc: forall(x y z: A), op x (op y z) = op (op x y) z;
    unit_l: forall(x: A), op u x  = x;
    unit_r: forall(x: A), op x u  = x
  }.

6つのフィールドがありますが、それらは次の意味です（見ただけで分かるとは思いますが）。

モノイドの台集合 A
モノイドの二項演算 op
モノイドの単位元 u
モノイドの結合律 assoc
モノイドの左単位律 unit_l
モノイドの右単位律 unit_r

これら6つのフィールドをすべて具体化すればモノイドのインスタンスを作れます。

Require Import Bool.
(* Boolには次の定理が含まれる：
  andb_assoc
  andb_true_l 
  andb_true_r
*)

Instance andbMonoidAllInOne : MonoidAllInOne := 
  {|
    A := bool;
    op := andb;
    u := true;
    assoc := andb_assoc;
    unit_l := andb_true_l;
    unit_r := andb_true_r
  |}.

この方式でも十分なことも多いと思います。

バンドル方式

構造の指標と法則を切り離してみます。

(* === バンドル方式 === *)

Class MonoidMagma := 
  {
    (* モノイドの指標 (A', op', u') *)
    A': Set;
    op': A' -> A' -> A';
    u': A'
  }.

Class MonoidBundle (MM: MonoidMagma) :=
  {
    (* モノイドの法則 *)
    assoc': forall(x y z: A'), op' x (op' y z) = op' (op' x y) z;
    unit_l': forall(x: A'), op' u' x  = x;
    unit_r': forall(x: A'), op' x u'  = x
  }.

切り離したのにバンドルとはこれいかに？ MonoidMagmaのなかに、3つのフィールドがまとめられているのでバンドル方式なのです。まとめられた指標を持つマグマが、MonoidBundleクラスの単一のパラメータとなります。

なお、フィールド名にすべてダッシュ（プライム「'」）が付いているのは、Coqの場合、異なるクラス内であっても同じフィールド名が使えないからです。これはちょっと酷いなー、と思うし、使い勝手は非常に悪いです。メカニズム上致し方ないとは言いながら、かなりイライラする仕様。

ひとまとまりの指標と、それに付随する法則を使うこの方式は、インスティチューションとの対応がハッキリしていて、個人的には使いやすく感じます。

アンバンドル方式

アンバンドル方式で何をバラすのかというと、指標に含まれる「台集合、二項演算、単位元」を別々なパラメータとして法則を表すクラスに渡すのです。

(* === アンバンドル方式 === *)

Class MonoidUnbundle {A: Set} (op: A -> A -> A) (u: A) := 
  {
    (* モノイドの法則 *)
    assoc'': forall(x y z: A), op x (op y z) = op (op x y) z;
    unit_l'': forall(x: A), op u x  = x;
    unit_r'': forall(x: A), op x u  = x

  }.

パラメータが3つありますが、それぞれ：

台集合を表すパラメータ A
二項演算を表すパラメータ op
単位元を表すパラメータ u

{A: Set} と中括弧（ブレイス）で囲まれたパラメータは値の指定を省略するパラメータです。省略しても、Coqが推論して補ってくれます。（暗黙パラメータと呼びます。）

インスタンスは次のようにして作ります。

Instance andbMonoidUnbundle : MonoidUnbundle andb true :=
  {|
    assoc'' := andb_assoc;
    unit_l'' := andb_true_l;
    unit_r'' := andb_true_r
  |}.

何が違うの？

それぞれの方式のメリット・デメリットを書いてなかったですが、それはあんまり分かってないからです。

オールインワン方式は、複雑な構造になると定義が肥大化するし、ノーテーションも利用できないので確かに問題ありそうです。

バンドル方式の欠点は、スピターズ／ファンデル・ウィーゲンのBundling is badの節に指摘されているのですが、Coq使用経験が浅い僕にはピンときません。バンドル方式で行き詰まりを感じるほどに使ってないですからね。

とりあえずは、バンドル方式もアンバンドル方式も使ってみて、使い勝手を比較してみようと思います。

ソースコード

(* -*- coding: utf-8 -*- *)

(* === オールインワン方式 === *)

Class MonoidAllInOne :=
  {
    (* モノイドの指標 (A, op, u) *)
    A: Set;
    op: A -> A -> A;
    u: A;
    
    (* モノイドの法則 *)
    assoc: forall(x y z: A), op x (op y z) = op (op x y) z;
    unit_l: forall(x: A), op u x  = x;
    unit_r: forall(x: A), op x u  = x
  }.

Require Import Bool.
(* Boolには次の定理が含まれる：
  andb_assoc
  andb_true_l 
  andb_true_r
*)

Instance andbMonoidAllInOne : MonoidAllInOne := 
  {|
    A := bool;
    op := andb;
    u := true;
    assoc := andb_assoc;
    unit_l := andb_true_l;
    unit_r := andb_true_r
  |}.


(* === バンドル方式 === *)

Class MonoidMagma := 
  {
    (* モノイドの指標 (A', op', u') *)
    A': Set;
    op': A' -> A' -> A';
    u': A'
  }.

Class MonoidBundle (MM: MonoidMagma) :=
  {
    (* モノイドの法則 *)
    assoc': forall(x y z: A'), op' x (op' y z) = op' (op' x y) z;
    unit_l': forall(x: A'), op' u' x  = x;
    unit_r': forall(x: A'), op' x u'  = x
  }.
    
(* === アンバンドル方式 === *)

Class MonoidUnbundle {A: Set} (op: A -> A -> A) (u: A) := 
  {
    (* モノイドの法則 *)
    assoc'': forall(x y z: A), op x (op y z) = op (op x y) z;
    unit_l'': forall(x: A), op u x  = x;
    unit_r'': forall(x: A), op x u  = x

  }.
    
Instance andbMonoidUnbundle : MonoidUnbundle andb true :=
  {|
    assoc'' := andb_assoc;
    unit_l'' := andb_true_l;
    unit_r'' := andb_true_r
  |}.