Category Theorem for programmers
1 Category: The Essence of Composition
圏 Category
対象s, 射s
満たすべき性質
射の結合律
単位元
Types and Functions
副作用
型
ボトム型
実用的には終わらない型の推論を停止できる
これがないと停止しない型の推論がある
数学的構造
表示的意味論 (denotational semantics)
副作用があるコード -> モノイドに落とせる
なのでモノイドが重要視
3 Categories Great and Small
3.1 - 3.
Great and Small category
もっとも簡単な圏→空集合
対象と射を適当に書いたグラフ→自由圏
順序集合
半順序→圏になる
モノイド
二項演算がある集合
0元、結合則
可換でなくとも良い
射の集合 -> Hom 集合
集合論的なモノイドの証明
mempty, mappend の定義
モノイドが圏であることを示すことができる、二項演算が加算である場合を考える
射: +5 , +1
恒等射: +0
合成: +1+5
圏の対象は集合とは限らない
オブジェクトの対象が集合の場合は small category になるg$
4. クライスリ圏
C++ での合成
Writer 圏
C++ での実装
Haskell での実装
クライスリ圏
対象＝型と射＝関数からなる圏
5 product, coproduct 積、余積
射に対して逆向きの射を考えることができる
a -> b に対して b -> a
こういうのが 双対性 duality
双対な射でできたものには 余 co プレフィクスを付ける
product と coproduct 、 monad と comonad ,etc ...
積を圏論で考える
射影 p, q があることが条件になる。a と b の積が c であるとき：
p: c -> a
q: c -> b
ペアが積であるのは明らか
c は (a, b), p : (a,b) -> a, q: (a, b) -> b
次の例は積とは言えない、どういう条件をつけたらどうしてそう言えるか？
u) c は (a), p: (a) -> a, q: c -> constant value
v) c は (a, b, d), p: (a, b, d) -> a, q: (a, b, d) -> b
圏論では、任意の「2 つの対象への射影を持つ」対象からの射がある対象が積になる
u -> ペア, v -> ペア, となる射があるのは明らか。
この逆がないのも明らか
射が c <- c' とある場合は c は c' より "better"、任意の c からの射がある場合は "best" になる
余積
積の双対、射は全て逆方向になる
p: a -> c
q: b -> c
積の場合と同様に best なものが余積になる
非対称性
積と余積は対称的でない
双対なものは大体の場合非対称
関数の性質による
全単射でもない限りは対称にならない
6 代数型
前章の product, coproduct をプログラミング言語上の型に当てはめる話
C++ の場合は struct, enum、Haskell の場合はタプル, レコード, そして代数的データ型
product はタプルに当たる, coproduct は enum, 代数的データ型に当たる
型は合成可能 ex)
Pair a b は a と b の合成と言える
片方の型が singleton な場合は、もう一方の型と合成後の型は同型
Pair a Unit と a は同型。同型写像があることは明らか
singleton な型が単位元のような扱いにできる
なので型はモノイダル圏を構成する ?
モノイダル圏についてはのちの章に出てくる
pair type と sum type はそれぞれ圏をつくる (TODO pair type という名前ではなかったはず！ちゃんと調べる
型の合成は非可換かつ推移的ではない
Pair a b ≠ Pair b a
Pair a (Pair b c) ≠ Pair (Pair a b) c
準環としての型
pair と sum の組み合わせで様々な型をつくれる
これらを二項演算子としてみた時、準環になる
準環 semi ring , or , rig など
準環は二項演算、零元、単位元があって逆元がないもの
pair が加算、sum が乗算にあたる
代数的な性質を持つので代数型となる
7 functor
functor は 圏から圏への射
ただし構造は保存する = 圏の中の射を保存する
f: a -> b => F f: = F a -> F b
Haskell でいう型クラスに対する fmap
関数も一つの型クラスとみなせる
Haskell では
a -> b を二項演算の適用と考えると
(->) a は型を一つ取る型クラスになる
なので関数に対しても fmap が定義できる
8 Functriality
bifunctor
圏と圏から圏への射
Class bifunctor f
bifunctor :: (a -> b) -> (c -> d) -> f a c -> f b d
または
Class bifunctor f
first :: (a -> b) -> f a c -> f b c
second :: (c -> d) -> f a c -> f a d
bifunctor から first, second を導ける、逆も可
ここら辺から図があったほうがかなり理解しやすくなる
monoidal 圏 -> 二項演算の圏
bifunctor であることが一つの条件 -> bifunctor は重要
Functorial
C++ での場合に Bifunctor を作る場合はクラスとテンプレートで定義する
型の判断の為に dymanic_cast が必要になる
代数型は sum と product で作れる
自動的に Functor にできる (Haskell の deriving functor)
クライスリ圏
fmap は id と >=>フィッシュオペレータから導出できる
covariant , contravariant
共変と反変
ここまで出てきたのはだいたい covariant
圏を写した時に射の向きが逆になるのが contravariant
profunctor
functor だが contravariant なもの
(->) r でできる圏は contravariant になる
Hom
9 Function Types
圏論での関数は圏の中の対象
internal function -> 圏の中の関数
external function -> 圏の外側の関数
Universal construction 普遍的構成
関数について考える (射ではない)
関数 ( $ z \in Z ) には次のものがある
値($ a \in A )
結果 ( $ b \in B )
関数適用は関数と値の product から結果 への射と考えられる $ g: (z, a) \rightarrow b
product がないと 関数は考えられない
ranking
$ g: (z,a) \rightarrow b に対して $ g': (z', a) \rightarrow b があった時
もし 射 $ h が $ h: z' \rightarrow z を満たしていたら $ z は $ z' より better
product は functor なので $ h に対して $ h \times id : (z',a) \rightarrow (z,a) がある
$ g' = g \circ (h \times id)
universaly best object
$ a \Rightarrow b
任意の $ z から射を引けるオブジェクト
eval をこれに対して定義する
$ eval :: ((a \Rightarrow b) \times a) \rightarrow b
g を eval を使って考えると
$ g = eval \circ (h \times id)
なお $ h :: z \rightarrow (a \Rightarrow b)
$ a \Rightarrow b が存在する保証はないが、集合に対しては常に存在する
また $ Hom-set Set(a,b) と $ a \Rightarrow b は同型
Haskell では 関数の型 $ a \rightarrow b はcategorial function object $ a \Rightarrow b とみなす
Currying
圏論的にはペアをとる関数を、関数を返す関数にすること
カリー化
curry f (a,b) = f a b
uncarry f a b = f (a, b)
Exponential
冪集合
10 Natural Transformation
自然変換
$ a \in C ,$ Fa, Ga \in D
$ \alpha : Fa \rightarrow Ga
11 Declative Programming
12 limit, colimit
圏論における上限
13 Free Monoid
自由→生成規則(generator)以外に制限を持たない
文字列とか
Haskell での自由モノイド
class Monoid m where
mempty :: m
mappend :: m -> m -> m
13.2 Free Monoid Universal Construction
Mon は モノイドたちからなる圏
カテゴリ的な見方と、積のマップとする見方がある
forgetful functor
monoidal な構造 = 二項演算の関係を失わせるファンクタ
逆に構造を残すのは horommorphism , 同型射
生成規則お集合から の関数
$ p :: x \rightarrow U m
U はfogetful functor
m (と p) が自由モノイドであるとは
iff generators x に対してユニークな射 h が任意のモノイド n に対して存在して次の条件を満たすこと
$ h :: \rightarrow n
$ q = U h . p
ただし
$ q :: x -> U n
14 Representable Functors
$ Set は $ C(a, x) の集合]
カテゴリ $ C から集合 $ Set へ写像する = represenation
15 The Yoneda Lemma
16 The Yoneda Embedding
Part 3
17 It's All About Morphisms
ここまでのおさらい的な内容
18 Adjunctions
19 Free/Forgetful Adjunctions
20 Monads: Pogrammer's Definition
21 Monads and Effects
22 Monads Categorically
23 Comonads
24 F-Algebras
25 Algebras for Monads
26 Ends and oends
27 Kan Extensions
28 Enriched Categories
29 Topoi
30 Lawvere Theories
31 Monads, Monoids, and Categories