2016年3月18日

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

こいつはやべえ、頭が完全に宇宙をエクスポートしそうだぜぇ。(???)
0
tomo🐧@learning @cocoatomo

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

2016-03-18 20:09:39
tomo🐧@learning @cocoatomo

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

2016-03-18 21:24:37
tomo🐧@learning @cocoatomo

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

2016-03-18 21:29:42
tomo🐧@learning @cocoatomo

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

2016-03-18 21:30:22
tomo🐧@learning @cocoatomo

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

2016-03-18 21:32:12
tomo🐧@learning @cocoatomo

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

2016-03-18 21:55:38
tomo🐧@learning @cocoatomo

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

2016-03-18 22:00:37
tomo🐧@learning @cocoatomo

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

2016-03-18 22:01:15
tomo🐧@learning @cocoatomo

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

2016-03-18 22:10:38
⿻あいや⿻ 技術書典11新刊🎉 数学と女の子たちの本「せつラボ」 @public_ai000ya

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

2016-03-18 22:18:47
tomo🐧@learning @cocoatomo

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

2016-03-18 22:23:59
tomo🐧@learning @cocoatomo

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

2016-03-18 22:12:38
tomo🐧@learning @cocoatomo

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

2016-03-18 22:18:46
⿻あいや⿻ 技術書典11新刊🎉 数学と女の子たちの本「せつラボ」 @public_ai000ya

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

2016-03-18 22:24:36
tomo🐧@learning @cocoatomo

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

2016-03-18 22:26:07
⿻あいや⿻ 技術書典11新刊🎉 数学と女の子たちの本「せつラボ」 @public_ai000ya

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

2016-03-18 22:34:23
tomo🐧@learning @cocoatomo

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

2016-03-18 22:39:56
tomo🐧@learning @cocoatomo

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

2016-03-18 22:41:02
⿻あいや⿻ 技術書典11新刊🎉 数学と女の子たちの本「せつラボ」 @public_ai000ya

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

2016-03-18 22:47:22
残りを読む(2)

コメント

コメントがまだありません。感想を最初に伝えてみませんか?