型クラスの悪いお薬
昨日の 型クラスの比較 - 檜山正幸のキマイラ飼育記 メモ編 への補足説明。既存のものに後からゴチャゴチャ文句を言うのは簡単だ。だから文句言う。
コアージョン（coercion - 檜山正幸のキマイラ飼育記 メモ編）は必要悪という意味で必須だから、使うのはいい（使わざるを得ない）。だけど、切り離し可能にしておかないと、弊害が出来たときの対処が出来ない。Haskellは切り離し不可能な組み込みコアージョンを採用してしまった。
型クラスの理論は、基礎圏が固定されている状況での相対具象圏達の理論だ。登場する圏達は全体としてドクトリンまたは宇宙を形成する。基礎圏をBとする。忘却関手が広くやせた部分圏を構成する。このやせた部分圏の射（圏の圏だから実体は関手）が相対具象圏の構造を与える。基礎圏Bは、やせた部分圏の終対象である。
相対具象圏 U:D→C があるとき、Dの対象XをU(X)上の構造を呼ぶ。宇宙のなかのすべての圏は、基礎圏Bまたはその直積ベキへの忘却関手を持つとして、その忘却関手を考えた U':D→Bn は絶対具象圏と呼ぶ。つまり、宇宙内のすべての圏は絶対具象圏の構造を一意に持つ。
圏のコアージョンを、|C|→|D| という部分写像だとする。コアージョンをC⊃→Dと書くことにする。圏コアージョン C⊃→D があって、定義域が有限なら、個々の対象のあいだの対応を列挙して書くことができる。
相対具象圏の忘却関手から誘導されるコアージョンを忘却コアージョンまたは台コアージョンと呼ぶことにする。正確に言えば構造忘却コアージョン。忘却コアージョンの部分的セクションになっているコアージョン（ラウンドトリップするコアージョン）を増強コアージョン、エンハンス・コアージョン（enhancement coercion）と呼ぶ。
型クラスのオーガニックな構造は、基礎圏上の構造付き対象（structured object, https://ncatlab.org/nlab/show/structured+set）を対象とする圏をモデル圏とするインスティチューションを構成することだ。インスティチューションの指標圏を忘れて、モデル圏の集まりを適当な大きなドクトリンのなかに埋め込むと宇宙（大きなドクトリンの部分ドクトリン）が出来る。一方で、グロタンディーク平坦化により単一の圏にすることもできる。
Haskell風型クラスは、宇宙という圏（2-圏の圏骨格部分）にコアージョン構造＝コアージョングラフを導入する。問題点は：
- コアージョンが（個々のコアージョンもコアージョングラフも）、ユーザーから不可視である。
- 問答無用に増強コアージョンが作られて、それを消すことも変更することも出来ない。
- 忘却コアージョンが絶対忘却コアージョンだけで、相対忘却コアージョンが作れない。
- 同様に、相対増強コアージョンも作れない。
要するに、固定されて変更不可能で歪んだコアージョングラフが組み込みで作られて、都合が悪くてもユーザーにはどうにもならない。
通常の型コアージョン＝対象コアージョンは、コアージョン自体が曲りなりにも射になっている（グラフは部分圏にはならない！）。が、圏コアージョンのタチの悪い所は、宇宙のなかで関手になってないことだ。宇宙の圏構造上の部分コンソリデーション（コンソリデーション - 檜山正幸のキマイラ飼育記 メモ編）でさえない。
圏コアージョンの定式化は、おそらくindexed family of objects/morphismsなんだろう。
背後には、色々と明らかにしなければならない問題があると思うが、相対指標の部分的インスタンス化の繰り返しと一挙インスタンス化の関係が、グロタンディーク平坦化のフビニの定理を導くだろう、という予想をちゃんとやらないとダメかも知れない。
