{圏の圏 -> 圏の圏}というやばい函手について

tomo🐧@learning @cocoatomo

@public_ai000ya では, 順を追って何回かに分けて説明しますね. 説明が長いためゆっくりになりますが, ご了承を.

あいや🐕 @public_ai000ya

@cocoatomo ありがとうございます！！

tomo🐧@learning @cocoatomo

@public_ai000ya 遅くなりました! まずは舞台設定から。圏は、型の圏を考えます。対象は型で、射は関数です。射のドメインは関数の引数の型で、コドメインは返り値の型です。 変数が複数のときは、引数全体を組にしたタプルの型を射のドメインとしてください。

あいや🐕 @public_ai000ya

@cocoatomo 引数が2つ以上の関数の引数をuncurryした感じのHask圏…ですね！

tomo🐧@learning @cocoatomo

@public_ai000ya 型の圏から型の圏への函手 (型の圏の自己函手) は、HaskellやScala(z)ではFunctorという名前になってます。 圏論では、函手は「対象関数」と「射関数」という2つのものからできていて、これは対象から対象への対応と、射から射への対応を

tomo🐧@learning @cocoatomo

@public_ai000ya 明確に区別するために、別の名前を付けたものです。

tomo🐧@learning @cocoatomo

@public_ai000ya ひとまずここまでは大丈夫そうですか?

あいや🐕 @public_ai000ya

@cocoatomo はい、大丈夫です。 普通のHask圏と圏論ですよね…。

tomo🐧@learning @cocoatomo

@public_ai000ya はい, 特に変わったことはしていません. 対象関数は型を型へ移し, 射関数は関数を関数を移します. これはそれぞれ, Functorのコンストラクタ, fmapに対応します.

tomo🐧@learning @cocoatomo

@public_ai000ya それぞれの型を書くと, []: a -> [a], fmap: (a -> b) -> (f a -> f b) です. 射関数の後ろの括弧は不要なのですが, こう書いておくと, a -> b 型の関数から f a -> f b 型への関数という

tomo🐧@learning @cocoatomo

@public_ai000ya 特徴が強調されます. ひとまず一区切りで, ここまでで何かあれば聞いてください.

あいや🐕 @public_ai000ya

@cocoatomo 問題ないです！

tomo🐧@learning @cocoatomo

@public_ai000ya では, 続きを. 函手にあたるものはList, Maybeとかがありますが, ListからListや, ListからMaybeへの関数が自然変換に相当します.

あいや🐕 @public_ai000ya

@cocoatomo ！！ Listが型引数を1つ持つ関手とすると 確かに圏の圏でのListからList、ListからMaybeへの射が 普通の圏での自然変換になってます！！ Haskellだと (Functor f, Functor g) => f a -> g b かな！？

tomo🐧@learning @cocoatomo

@public_ai000ya そちらが対象関数の方ですね. 射関数の方は (Functor f, Functor g) => (f a -> f b) -> (g a -> g b) となります. Haskellだと, fmapの付替だけで済むみたいですが.

あいや🐕 @public_ai000ya

@cocoatomo ああそうだ、射も写さなきゃでした！

tomo🐧@learning @cocoatomo

@public_ai000ya ちょっとここでさっきの翻訳記事の話に戻って解説します. 圏というのは対象と対象をつなぐ射でできていますが, ここで今まで圏だと思っていたものを, より大きな圏だと思うことができます! そうすると圏と圏とつなぐものは函手なので, これが射になります.

tomo🐧@learning @cocoatomo

@public_ai000ya これを圏の圏と言います. では圏の圏から圏の圏への函手は何になるでしょうか? 圏→→→圏 ↓　　　↓ ↓函手→↓函手 ↓　　　↓ 圏→→→圏 この左から右へ伸びてる矢印が「圏の圏における函手」です.

あいや🐕 @public_ai000ya

@cocoatomo 圏の圏から圏の圏への関手…！？ うーん…自然変換から自然変換への射…？？？(わからない…)

tomo🐧@learning @cocoatomo

@public_ai000ya 函手から函手への対応なので, ここが自然変換になります. どんどんメタメタしくなってきてややこしくなります.

あいや🐕 @public_ai000ya

@cocoatomo うう…。 関手圏の射が自然変換ですよね…。 圏の圏の射が関手ですよね…。 うーん！？！？ 絵にも書いてみましたがわからないです…。

tomo🐧@learning @cocoatomo

@public_ai000ya 自然変換までくると具体的な物 (インスタンス) を引数に取るわけではなくなるのでややこしくなるのは確かです. 圏がメタメタしていく様子を整理しましょうか. 対象と射を組にして並べてみます. (対象, 射), (射, 函手), (函手, 自然変換)

tomo🐧@learning @cocoatomo

@public_ai000ya 下にいくほどメタメタしていきますが, 圏という概念としては同じものです.

あいや🐕 @public_ai000ya

@cocoatomo 圏の圏から圏の圏への関手は 圏の圏から圏の圏への関手であるとしか言えない…ってことでしょうか…。

あいや🐕 @public_ai000ya

完全にやばい。 pic.twitter.com/eA7FOaqoj6

拡大