「カン拡張のために、柱の絵を描く」にて：
特にシリーズ記事とかにしませんが、関連する幾つかの記事達が、全体としてカン拡張の説明になればいいな、というゆるい計画はあります。
というわけですが、カン拡張を知ったら何かいいことがあるんでしょうか？
内容：
圏論内部からの動機
カン拡張というと、マックレーンの有名な言葉：
- All Concepts are Kan Extensions
があります。圏論に出現するすべての概念はカン拡張で説明できる、ということです。ちょっと大げさな気がしなくもないですが、標準的・典型的な圏論の概念がカン拡張に包摂されるのは事実です。
極限／余極限は、圏論の重要な道具ですが、それぞれ右カン拡張／左カン拡張の特別な場合になります。つまり、「極限はカン拡張」（Limits are Kan extensions）です。
随伴〈adjoint | adjunction〉は圏論の中心的な概念ですが、随伴系 (η, ε): F -| G :D→C （この書き方は「随伴系の書き方」参照）はカン拡張で説明できます。「随伴はカン拡張」（Adjunctions are Kan Extensions）です。
普遍性〈universal property〉とか普遍的構成〈univesal construction〉は圏論の指導原理です（僕は余り好きじゃないけど*1）。これらは、極限や随伴に帰着できるので、結局はカン拡張で説明できます。
カン拡張までたどり着けば、（標準的学習コースで）それ以前に習った概念はカン拡張に吸収されることになります。カン拡張は、圏論における統合フレームワーク〈unifying framework〉として機能します。
以上の話は、圏論内におけるカン拡張の意義と位置付けであり、道具として圏論を使いたい下心ケンロニスト*2にはあんまりアピールしないかも、と思います。
関手データモデルとデータ移行関手
僕にとって、強く印象に残ったカン拡張の応用はスピヴァックの関手データモデルです。
文字通り衝撃的でした。このことは「データベースとカン拡張と思い出 // データベースとカン拡張」に書いてあり、そちらと重複もありますが、少し補足します。
スピヴァック理論は、現在では、プログラミング言語／型理論とデータベースの統合を目指した代数データベース理論へと発展しています。
- Title: Algebraic Databases
- Authors: Patrick Schultz, David I. Spivak, Christina Vasilakopoulou, Ryan Wisnesky
- Pages: 80p
- URL: https://arxiv.org/abs/1602.03501
代数データベース理論は、高度化・複雑化して当初のシンプルさはなくなっています。当初の関手データモデルで、何が驚いたかって、そのシンプルさです。データベース用に新しい概念を作ることは一切せずに、既存の圏論的概念だけで鮮やかな再解釈を提示したのです。
なかでも注目すべきは、データ移行関手〈data migration functor〉*3です。φ:S→T がデータベーススキーマのあいだの射のとき、S上のデータとT上のデータを変換する3種のデータ移行関手が自動的に構成できます。
- データ引き戻し関手 Δφ:Data(T)→Data(S)
- データ前送り関手(右) Πφ:Data(S)→Data(T)
- データ前送り関手(左) Σφ:Data(S)→Data(T)
Data(S)は、データベーススキーマS上のデータ状態（データインスタンスとも呼ぶ）とデータ状態遷移からなる圏です（Data(T)も同様）。
データベーススキーマを変更したとき、新しいスキーマ上に既存データを移し替える必要があります。このとき、データ（情報）の欠損や重複が生じるのは避けられないかも知れません。そうだとしても、“最良のデータ移行”をしたいのは当然の要求でしょう。さて、“最良のデータ移行”ってなに？
僕が知る限り、スピヴァック以前に“最良のデータ移行”の定義（経験や雰囲気ではなくて、明確な“良さ”の基準）はなかった気がします。スピヴァックはここでも、圏論の標準的な概念だけを使って“最良のデータ移行”を定義しています。
- 引き戻し関手〈pullback functor〉Δφは、φの前結合で誘導される関手
- 右前送り関手〈right pushforward functor〉Πφは、Δφの右随伴＝φに沿った右カン拡張
- 左前送り関手〈left pushforward functor〉Σφは、Δφの左随伴＝φに沿った左カン拡張
Δφは特殊なケースとしてテーブルの射影（カラムの制限）を含み、Πφは特殊なケースとしてテーブルのジョインを含み、Σφは特殊なケースとしてテーブルのユニオンを含みます。別な言い方をすると、よく知られたデータ操作の（極端な）一般化としてデータ移行関手が定義されています。
この定式化／ストーリーはなかなかにシビレルものがあり、これを理解するためだけでもカン拡張を学ぶ価値があると思います。
型クラスとモデル
型クラスは、関手データモデルと類似の枠組みで扱えます。おおよその対応は：
| データベース | 型クラス関連 |
|---|---|
| データベーススキーマ | 型クラス |
| データベース状態 | 実装（モデル） |
| データベース状態遷移 | 実装のあいだの模倣 |
| データ移行 | 実装の構成 |
ただし、「まともな型クラス への入門： 関数型とオブジェクト指向の垣根を越えて // 壮絶な車輪の再発明と混乱を極める用語法」で述べたように、多義語・同義語・類語が多すぎて、用語法を整理・再定義しないと誤解なしに語ることは難しいです。例えば、「実装」と言っても構文的な概念（プログラムコード）と意味論的な概念（実行系）があり、それらを区別しないとわけわからん話になります。
ちなみに、「型クラス」と同義・類義と思われる言葉は：
- 指標〈signature〉
- 仕様〈specification〉
- （形式）セオリー〈(formal) theory〉
- インターフェイス〈interface〉
- プレゼンテーション〈presentation | 表示 | 表現〉
- （構文）生成系〈(syntactic) {generators | generating set | system of generators (and relations)}〉
- コンピュータッド〈computad〉
- ポリグラフ〈polygraph〉
- などなど…
とりあえず、「型クラス」を理論的に取り扱った概念を「指標」と呼ぶことにすると、指標のあいだの射〈signature morphism〉φ:S→T があると、モデル圏のあいだの関手 Δφ:Model(T)→Model(S) が定義できます。Model(-)は、指標に対するモデル（意味論的な実装）からなる圏です。同じ記号を使っていることから分かるように、Δφはデータ引き戻し関手に相当する“モデル引き戻し関手”です*4。
さて、問題はモデル引き戻し関手Δφの右随伴（＝右カン拡張）／左随伴（＝左カン拡張）が存在するか？ です。もし存在するなら、カン拡張が“最良の実現”を与えることから、最良のモデル構成法が得られます。
プログラムの場合、データベースのスキーマ変更に対応するのは、インターフェイス（指標／仕様）変更です。インターフェイス変更に伴う最良の実装はカン拡張で実現できます。ただし、データベース（関手データモデル）の場合ほど状況が単純ではないので、強力な結果は期待できないかも知れません。また、右カン拡張と左カン拡張の二種類の“最良”があり、これらの現実的な意味や使い分けがいまひとつハッキリしません。
夢のようにオイシイ話ではありませんが、データだけでなくプログラムに対しても、“仕様変更に伴う最良の移行”をカン拡張を基準に考えることができるでしょう。
相対モナド
相対モナド〈relative monad〉は、アルテンキルヒ達により提案されたモナドの一般化です。
- Title: Monads Need Not Be Endofunctors
- Authors: Thorsten Altenkirch, James Chapman and Tarmo Uustalu
- Pages: 15p.
- URL: http://jmchapman.github.io/papers/Relative_Monads.pdf
(↑)これは2010年前後に出たものです。arXivに、40ページに増やした2014年版があります。
「普通のモナドじゃどうも痒いわー」と思っていた2011年頃、相対モナドはイケるんじゃないか、と思いました。次の記事で言及しています。
上記論文のタイトルのとおり、モナドの台関手〈underlying functor〉を F:C→C から F:C→D としてモナド概念を一般化しています。相対モナドの定義は、クライスリ拡張オペレータを使ってなされます。“とあるモノイド圏内のモノイド”という定義が難しいからです。
ところが、関手圏 [C, D] = DC に特殊なモノイド積を入れると、結局は“モノイド圏[C, D]内のモノイド”として相対モナドを再定義できます。このとき、“特殊なモノイド積”の構成に左カン拡張が使われます。
2010年頃に登場した相対モナドは、僕が期待したほどには注目・評価されませんでした。が、実用的な応用もポチポチと出ていて、モナドの変種〈バリアント〉として定着しそうです。例えば、次のスライド／動画（どちらも"Using Relative Monads for Cheap Syntax"という話題）があります。
- https://speakerdeck.com/stephanh/using-relative-monads-for-cheap-syntax
- https://www.youtube.com/watch?v=_i4TqluJNKM
相対モナドの別な話題： 「米田埋め込み、米田拡張、そして米田モナド」において、米田埋め込みを単位とするモナドについて（曖昧に）述べていますが、これは普通のモナドとして定義できません。大規模な相対モナドになるはずです。その定義には、米田埋め込みに沿ったカン拡張＝米田拡張が使われるでしょう。
相対モナドのまた別な話題： ホモトピー型理論のヴォエヴォドスキーは、相対モナドに注目していたようです。残念ながら、2017年9月30日に彼は亡くなりましたが、2016年に相対モナドの論文を書いています。
- Lawvere theories and Jf-relative monads (Submitted on 9 Jan 2016)
https://arxiv.org/abs/1601.02158 - C-system of a module over a Jf-relative monad (Submitted on 1 Feb 2016)
https://arxiv.org/abs/1602.00352
ヴォエヴォドスキーは、依存型の理論を作り直そうとしていたらしく（未完のプロジェクト）、その基本的道具のひとつに相対モナドがあったようです。
プログラム最適化
- Title: Kan Extensions for Program Optimisation Or: Art and Dan Explain an Old Trick
- Author: Ralf Hinze
- Pages: 39p
- URL: http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf
この論文については、「独身男性にもコウノトリはモナドを運んでくるのか」に次のようなメモがあります。
このラルフ・ヒンズの論文は、CPS（continuation passing style）変換によるプログラム最適化の背後にある現象をカン拡張で説明しようとするものです。このなかで、余密度モナド（codensity monad）ってのが出てくるのですが、これがなんだか面白い。
余密度モナドを絵に描こうとしていたのがコレ（「なんかのお絵描き」より）。
絵を描いているうちに、右カン拡張がラムダ計算類似の絵算で取り扱えそうだ、と気付きました。
ところで、ヒンズ論文のサブタイトル"Art and Dan Explain an Old Trick"って、最初サッパリ意味不明でした。どうやら、ArtとDanは人の名前（短縮名）らしく、
- Art ＝ アーサー・ケイリー〈Arthur Cayley〉
- Dan ＝ ダニエル・カン〈Daniel Kan〉
群に関するケイリーの表現定理（の発想）とカン拡張が、プログラム最適化技法の背後にある理屈を説明してくれるよ、という意味でしょう。
ケイリーの表現定理って、圏論的文脈に置けば米田埋め込み（米田表現）の特殊ケースなんですよ。登場人物を圏論の巨匠二人にして、
- Nob and Dan Explain an Old Trick
のほうがいいような気がしますけどね。
- Nob ＝ 米田信夫〈Nobuo Yoneda〉
おわりに
カン拡張は意外に多くの場面で登場しますね。圏論内部で統合フレームワークとして機能するということは、圏論の外の世界でも、抽象度が高く包括的な記述の道具に使えることが期待できます。
今回出した例は、いずれもデータベース／プログラムに関連していて、そのテの知識がないと理解できないことが残念な点です。特定分野の予備知識を要求しない事例があるといいんですが … 何かあったら教えてください。
