HTTPS SSH

F-代数

そもそも圏論について

圏論は比較的新しい数学の分野であり, その手法も一風変わっている.

高校数学までは集合と関数を使っていた

明示的にしろ暗黙的にしろ, 集合と関数という言葉を使って数学をしていた. 集合とは「元 (げん)」の集まりであり, 関数とはある元からある元への対応のことだ. 「整数」とは \(0, \pm 1, \pm 2,\dots\) という数字の集合だし, 計算というのはある数字からある数字への関数と見ることができる.

「元」や個々の数字という具体的なもので関数を考えるのは, (教育の成果もあって) すごく自然な思考法として広まっている. 例えば「2 倍する」という関数を説明するとき,「1 を 2 に, 2 を 4 に, 3 を 6 にするもの」と言うのがそこそこ普通だろう. 「整数から偶数への和に関する同型写像」などと説明する人は稀だろう. (この説明で理解できる人はもっと稀だろう.)

この 2 つの説明の違いは何か. それは前者が個々の値についていちいち説明しているのに対し, 後者は「和に関する同型」という関数の性質で説明している. そこに個々の値 (元) についての言及は無い. 前者の利点は具体的で分かりやすいこと. 後者の利点は抽象的で汎用性が高いこと.

「汎用性が高い」という意味は, 整数以外の有理数, 実数, 複素数, 果てはベクトル, 行列にまで「2 倍する」という計算が考えられる. 同じ言葉を使っているだけあって, 全部の「2 倍する」という計算は似たような性質を持っている. それらをまとめて扱えた方が便利なことには違いない. 殊にプログラミングでは「同じものはまとめる」というのは普通に行われている. それならば定義域には最低限の制約のみを課して, その制約を満たすものなら何にでも「2 倍」という計算を考える方向が良いだろう.

なんで圏論なのか

そういった抽象的, 公理的な記述で概念を説明するのが現代の数学の流儀だ. それと同じく抽象的, 公理的にプログラムを記述するために使うのが圏論だ.

プログラミングにおいて型は重要である. それに異論は無いだろう. その型とは何か? 型とは値の集合である. 値の分類が型であり, 引数, 返り値に現れる値の制限を表現するのが型の役目である. (型について語り出すと長くなるので, 別の機会に書くことにします.)

型は値の集合で, 関数は値の集合と値の集合の間の関係だ. 関係を記述するのに圏論は向いている.

さらにこれは推測だが, 関数 (射) を中心に概念を記述するのが特徴の圏論は, コンパイラによるチェックに向いているのだろう.

実際に圏論をどう使うかは後に回すとして, プログラミング言語の理論として圏論を使う理由はこういったところだろう.

圏論では対象と射を使う

ある 2 つの整数 \(x, y\) を足す関数 \(add(x, y) = x + y\) を考えるときには, 個々の整数 \(\dots, -1, 0, 1,\dots\) から 2 つ選んで足し算をする計算を思い浮かべる人が多いだろう. しかし, 圏論はそういった集合 (この例では整数全体の集合) の元に着目するのではなく, それ自体の性質や他の関数との関係で, 関数を定義しようと試みる.

例えば「整数どうしは足し算ができ, その結果は整数である」という性質を記述するとき, 以下のような主張になる.

\begin{equation*} \mathbb{Z} を整数の集合とすると, 次のような射 add が存在する. \end{equation*}
\begin{equation*} \mathbb{Z} \times \mathbb{Z} \to \mathbb{Z} \end{equation*}

圏論では関数のことは「射 (morphism)」と呼ぶ. この add という例では, その定義域 (domain) は \(\mathbb{Z} \times \mathbb{Z}\) であり, 値域 (range) は \(\mathbb{Z}\) である. こういう射の定義域や値域になるものを「対象 (object)」と呼ぶ. (「値域」はその関数が出力し得る値の集合のことで, 関数が出力しない値は含まない. ただ, その制限は関数の合成にはあまり関係無いので, この文書ではやや条件を緩めて「関数が出力し得る値を含む集合」も「値域」と呼ぶことがある.)

「集合の元」はタブー

整数が対象であることから分かるかもしれないが, 対象は集合であることが多い. その集合の中身には言及せずに射の性質を語るのが圏論のやり方だ. 今まで「集合の元」を使って説明していたことと同じ内容を, 対象と射だけで説明するのが圏論だ.

圏論では対象が集合かどうかにはお構い無しにただの抽象的な概念「対象」であるのだが, 慣れるまでは具体的な集合を思い浮かべても良いと思う.

ここの解説では, 集合の言葉と圏論の言葉の間を頻繁に行き来しようと思う. 既に知っている何かに引き付けて考えるのが, 何かを知る方法の 1 つではあるに違いない.

圏論で使って良い言葉は

集合の言葉「元, 要素」「(ある集合に) 含まれる」には慣れているものとして解説は省く.

圏論で使う概念は

  • 圏 (category)
  • 対象 (object)
  • 射 (morphism)
  • 図式 (diagram)

だ. そして使う言葉は主に

  • (射が) ある射とある射の合成である (composite)
  • (射が) 恒等である (identity)
  • (射が) 一意である (unique)
  • (射が) 存在する (exist)
  • (図式が) 可換である (commute, commutative)

となる.

逆にこれ以外の概念や言葉は使ってはいけないことになる. (λ 計算のルールが 3 つしか無いのにも似ているかもしれない.) そんな制約条件のもと数学的対象について語ろうとするのが圏論だ. 圏論は「縛りプレイ」の数学なんだ.

これだけで全てを語ろうというのだから大それたことだとは思う. それでも色々な数学的概念が圏論で語れてしまっているので, 数学者による積み重ねは素晴しい. (3 つしか規則が無い λ 計算もチューリング完全性を有している.) 我々はそのお零れとして, いくつかの例を勉強させてもらおう.

概念の説明・その1 (圏, 対象と射)

まず圏というのは射と対象でできている. 圏についてはこれ以上言うことは無い. 大事な仕組みは射の方にある.

射というのは対象と対象を結ぶ矢印のことだ.

対象 --射--> 対象

これで説明は終わりなのだが, これだとイメージでしか語っていないので, もう少し形式的に書いていく.

対象の定義についてだが,「対象とは何か?」については深掘りせず,「そういうものがある」とだけ断って話を続ける. 対象がどんな意味を持つかはどんな圏を考えるかで変わってくるので, ここで解説しようとしてもぼんやりとした例しか出せない. 個々個別の話をするときには具体的な例を挙げるので, そこまで待っていて欲しい.

射の定義は「矢印で表されるものであり,『矢印の根本の対象』と『矢印の指す先の対象』を 1 つだけ持つもの」である. 「矢印の根本の対象」を「射の始域 (domain)」,「矢印の指す先の対象」を「射の終域 (codomain)」と呼ぶ. 「射の始域 (domain)」は「関数の定義域 (domain)」を,「射の終域 (codomain)」は「関数の値域 (range)」をそれぞれ抽象化したものである.

抽象化した定義で何が言いたいかと言うと,「射があったらその始まりの対象と終わりの対象がある」ということである. 始まりに対象の無い射は無いし, 終わりに対象が無い射も無い. 始まりの対象を複数持つ射も無いし, 終わりの対象を複数持つ射も無い. このように始まりと終わりがきっちり 1 つずつあるので, 矢印でイメージするのがピッタリくるのである.

ついでに言うと, (特に理由が無ければ) 対象は点で書かれることが多い. 関数のときに

┌ Z ┐ ┌ Z ┐
│ 1 →→→ 2 │
│   │ │   │
│ 2 →→→ 4 │
└─-─┘ └─-─┘

という図を書いたことがあるかもしれないが, これを圏で抽象的に書くときは

Z  Z
・→・

と簡素で非常に味気無くなる.

圏は射と対象の集まりなので, 全体を矢印 (= 射) と点 (= 対象) で描くと有向グラフになる.

\begin{equation*} \begin{array}{ccccc} \cdot & \rightarrow & \cdot & \rightarrow & \cdot \\ \downarrow && \downarrow && \\ \cdot & \rightarrow & \cdot && \end{array} \end{equation*}

このグラフが「図式 (diagram)」だ. この図式にある射を辿りながら図式の性質をつかむ作業を「図式追跡 (diagram chase)」と言う. (訳語は適当. diagram chase という言葉は使われているのは確か.) ちなみに始域と終域は同じでも良いので, 矢印はぐるっと回って同じ対象に戻ってくるのもアリだ.

モノとしては圏の定義は以上で終わりだが, 射にはまだ説明していない性質がある. 「合成射 (composite morphism)」と「恒等射 (identity morphism)」の存在だ.

「合成 (composition)」というのは「関数合成」と同じ意味だ. 次のような 2 つの射 \(f, g\) があったとき, 合成射 \(g \circ f\) も存在する.

\begin{equation*} \begin{array}{ccc} \cdot & \xrightarrow{f} & \cdot \\ g \circ f & \searrow & \downarrow g \\ && \cdot \end{array} \end{equation*}

形式的に言うと次のようになる. \(f\) の終域と \(g\) の始域が同じとき, \(f\) の始域から \(g\) の終域への射 \(g \circ f\) が唯一つ存在し, これを合成射と呼ぶ.

ここからは少し大学数学的な話が続くので, そこに興味が無くプログラミングの型に関係する話を先に読みたい人は後に出てくる小節 :ref:`category-of-types` を読んでも良いと思う.

射というのはたいてい「何か良い性質を持つ写像」を抽象化したものだが, 数学で出てくる「何か良い性質を持つ写像」は合成しても, 再びその良い性質を持っていることが多い. 群, 環, 体ではこのような良い性質を持つ写像のことを「準同型」と呼ぶ. 代数を少しかじったことのある人なら「準同型の抽象化」で射を説明しても良いかもしれない. ただし, あまり具体的な準同型を思い浮かべると, イメージがそれに引っ張られる困ったことになるが.

合成射も射なので, さらに射を合成することができる. そしてそのとき結合律という性質が成り立つ. 式で書くとこんなふうになる.

\begin{equation*} (h \circ g) \circ f = h \circ (g \circ f) \end{equation*}

関数で言うと,「結合順序を変えても全体として同じ関数になる」という話なので, 至極当たり前な性質だと思う. むしろこれが成立しないと言えることが少なくなって色々辛い.

「合成射」に関してはこれくらいにして, 次の「恒等射」の話に移る. 「恒等 (identity)」とは「何も変えない」という意味で,「恒等射」は受け取ったものをそのまま返す射のことだ. 恒等射は対象ごとに必ず 1 つずつあって, 対象 \(A\) の恒等射を \(id_{A}\) と書く. この「必ず存在して」「1 つしかない (= 複数あるように見えたら実は同じもの)」というのも大事な性質だ. (この言葉の大事さについては後で触れる.)

恒等射も射なので, 他の射と合成することができる. この合成において恒等射には特別な性質があって, それはさっきの「何も変えない」という意味を表現している. 式で書くとこんなふうになる.

\begin{align*} 射 f: A \to B, g: C \to A があったとき\\ \end{align*}
\begin{align*} f \circ id_{A} = f \\ id_{A} \circ g = g \end{align*}

つまり, 合成しても何も変えない, というだけだ.

対象と射についてはこれくらいで終わる.

型の圏

さぁ, やっとプログラマにとって具体的な話だ! 気長にここまで読んでくれて, ありがとう!

「型の圏」と言うからには, もちろん「型」を「圏」で扱う話をする. あるプログラミング言語に出てくる型を集めて, それを圏と考えることができる. その圏の対象は型で, 射は (いわゆる「副作用」の無い) 関数のことだ. (「副作用」の定義はきちんとしないと面倒かつ怖いことになるのだが, ここでは詳細に踏み込まずいったん横に置いておく.)

対象となるのが個別な値 (整数だったら \(1, 2, 3\) など) ではなく整数全体であることに注意して欲しい. 整数全体は集合ではあるのだが, それを 1 つのモノとして扱うことになる. いつもの視点より抽象度を上げて話をしていると思ってもらうのが良い.

さて,「型の圏」がここまでに挙げた圏の性質を満たしているかを見ていく.

対象については特に制約も無いので, チェックべき性質は無い.

射については, 合成と恒等射について見る必要がある.

概念の説明・その2 (図式, 圏の圏, 関手)

最初に断っておくと, 自然変換については説明を割愛する. その理由は, 型の圏での自然変換については私が不勉強であることと, この文章でそこまで深入りするつもりが無いことである. 型の圏の自然変換についてはまた別に書くかもしれない.

再び型の圏

型の圏での関手と言ったら, プログラムでは何に当たるのだろうか?

概念と言葉の使い方

「圏論で使って良い言葉は」の節で並べた言葉の使い方を見ていく.

逆向きに見ると,「何かと何かが等しい」という主張をするには

  • 「ある対象からある対象へのある性質を満たす射が一意」という図式の性質を使う
  • 「ある図式が可換である」という図式の性質を使う
  • 射と射が等しいという主張をしている図式を使う

くらいしか道具が無いのが分かるだろう.