型クラス

Coqの型クラスについて思うことをメモしていく。

1. フィールド名が大域的なのは最低。フィールド名を局所化すれば出来る事が色々あるのに。ミクシンはその一例。
2. フィールドアクセッサの構文がない。f x の代わりに x.(f) が使えるようだが使いにくいし、そもそもfが大域的名前なのがどうしようもない、って前項と同じ愚痴だ。
3. 述語クラスというのがあって、命題の集まり（連言として解釈）をクラスの形で書いたもの。命題＝型だから、インスタンスは証明の集まりとなる。つまり、クラスは公理のような一般的な命題（パラメータを持つことが多い）で、インスタンスは定理または事実。インスタンス名は「モノの名前」ではなくて「コトの名前」。
4. 述語クラスは、スピターズ／ファンデル・ウィーゲンのアンバンドル方式に出てきた。アンバンドル方式では演算子クラスというのもあって、定数、n項演算（n=0が定数）、n項関係などの記号1個につきクラス1個を作る。Notationと組にして、汎用の記号を定義していくやり方。構造を粒度の細かい最小単位に分解して、それに名前と記号を与える、というもの。
5. 「パラメータ vs フィールド」と「バンドル vs アンバンドル」は実は独立した問題だ。パラメータにバンドルした情報を渡すこともあるし、フィールドにアンバンドル情報をセットすることもある。
6. 単一フィールドに入れ子クラスを作るなら、バンドル方式かつフィールド方式。複数フィールドをフラットに埋め込めばアンバンドル方式かつフィールド方式。いずれにしても、アンバンドル方式では、概念のくくりや境界線が判別できない。