圏論的コンテナ - 檜山正幸のキマイラ飼育記 (はてなBlog)

コンテナは、形状〈shape〉を持つデータに対する型理論的な概念として登場しました。よく知られたデータ型をコンテナとして説明できるので便利だなとは思っていましたが、データ型以外の用途でも使えることに気付きました。まずはこの記事でコンテナそのものについて説明します*1。

記事タイトルに「圏論的」が付いているのは、コンテナを圏論の枠組みで定義するからです。圏論的に見たコンテナとは、集合圏の自己関手で特別に扱いやすいものです。扱いやすい理由は具体的な仕様と表示を持つからです。 $\newcommand{\A}{\wedge } \newcommand{\width}{\mathrm{width} } \newcommand{\Shp}{\mathrm{Shp} } \newcommand{\Pos}{\mathrm{Pos} } \newcommand{\ShpData}{\mathrm{ShpData} } \newcommand{\Map}{\mathrm{Map} } \newcommand{\In}{\text{ in } } \newcommand{\id}{\mathrm{id}} \newcommand{\twoTo}{\Rightarrow } \newcommand{\hyp}{\text{-} } % \require{color} \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\For}{\Keyword{For } }% \newcommand{\Define}{\Keyword{Define } }% \newcommand{\Where}{\Keyword{Where } }% \newcommand{\Declare}{\Keyword{Declare } }%$

内容：

コンテナスキーマ
形状付きデータ
コンテナスキーマのその他の事例
コンテナ関手
コンテナスキーマの圏
コンテナスキーマの圏から関手圏への関手
形状付きデータのデータ変換の自然性
おわりに

コンテナスキーマ

コンテナの圏論的な定式化では、“関手を定義するデータ”と“定義される関手”を同一視してそれをコンテナと呼ぶことが多いのですが、同一視すると分かりにくいので、コンテナスキーマとコンテナ関手に分けて説明します。コンテナ関手はコンテナスキーマから定義されます。あるいは（同じことですが）、コンテナスキーマから定義される関手がコンテナ関手だ、と言えます。

コンテナスキーマから説明を始めますが、コンテナスキーマ〈container schema〉（まだ未定義だが）を $C, D$ などの英字大文字で表します。コンテナスキーマは2つの構成素を持つので、 $C = (S, P)$ のように書けます。構成素の説明も書くと次のようです。

$\quad (S, P)\\ \Where\\ \quad S \in |{\bf Set}|\\ \quad P: S \to |{\bf FinSet}|$

$S$ は任意の集合で、 $P$ は $S$ をインデックス集合とする有限集合の族〈indexed family of finite sets〉です*2。

つまらない例ですが、 ${\bf 1} = \{*\}$ を単元集合として、次はコンテナスキーマの例です。

$S = {\bf 1},\; P(*) = \emptyset$
$S = {\bf 1},\; P(*) = {\bf 1}$

一番目の例を $\mathrm{Emp}$ 、二番目の例を $\mathrm{Triv}$ という固有名で呼ぶことにします。

$\mathrm{Emp}, \mathrm{Triv}$ よりは意味のある（実用性もある）コンテナスキーマの例として二分木〈二進木〉のコンテナスキーマを挙げます。

二分木形状〈shape of binary tree〉（のテキスト表現）を以下のように定義します。詳しくは、「反ラックス・モノイド関手の一般余結合律〉の最初の2節と「BUNツリーの亜群オペラッド構造 // BUNツリー」を参照してください。

$( - \A - )$ は二分木形状である。
$s, t$ が二分木形状のとき、 $t[s/i]$ は二分木形状である。これは $t$ の $i$ 番目のプレースホルダーに $s$ を代入〈置換〉したもの。
以上により構成される記号列だけが二分木形状（のテキスト表現）である。

二分木形状の幅〈width〉を次にように定義します。

$\width( ( - \A - ) ) = 2$
$\width( t[s/i ] ) = \width(s) + \width(t) - 1$

例えば：

$\quad \width(\, ( (- \A -)\A(-\A-) ) \,)\\ = \width(\, (- \A -)[(- \A -)/1][(- \A -)/2] \,)\\ = \width(\, (- \A -)[(- \A -)/1] \,) + \width( (- \A -) ) - 1\\ = (\width( (- \A -) ) + \width ( (- \A -) ) - 1) + \width( (- \A -) ) - 1\\ = (2 + 2 - 1) + 2 - 1 = 4$

すべての二分木形状からなる集合を $S$ として、 $P:S \to |{\bf FinSet}|$ を次のように定義します。

$\For t \in S\\ \Define P(t) := \{1, 2, \cdots, \width(t)\} \;\in |{\bf FinSet}|$

ペア $(S, P)$ はコンテナスキーマになります。このコンテナスキーマを $\mathrm{BinTree}$ という固有名で参照します。

形状付きデータ

$C = (S, P)$ がコンテナスキーマのとき、 $\Shp^C := S,\; \Pos^C := P$ という書き方を使います。

$\quad C = (\Shp^C, \Pos^C)$

例えば：

$\quad \mathrm{Triv} = (\Shp^\mathrm{Triv}, \Pos^\mathrm{Triv})\\ \Where\\ \quad \Shp^\mathrm{Triv} = {\bf 1}\\ \quad \Pos^\mathrm{Triv} = \lambda\, x\in {\bf 1}.(\, {\bf 1} \;\in |{\bf FinSet}|\,)\\ \:\\ \quad \mathrm{BinTree} = (\Shp^\mathrm{BinTree}, \Pos^\mathrm{BinTree})\\ \Where\\ \quad \Shp^\mathrm{BinTree} = (\text{すべての二分木形状からなる集合})\\ \quad \Pos^\mathrm{BinTree} = \lambda\, t\in \Shp^\mathrm{BinTree}.(\, \{1, 2, \cdots, \width(t)\} \;\in |{\bf FinSet}| \,)$

コンテナスキーマ $C = (\Shp^C, \Pos^C)$ において、 $\Shp^C$ を形状の集合〈set of shapes〉と呼び、その要素を形状〈shape〉と呼びます。形状 $s\in \Shp^C$ に対して、 $\Pos^C(s)$ を形状 $s$ の位置の集合〈set of positions〉と呼び、その要素を形状 $s$ の位置〈positio〉と呼びます。

例えば、 $( (- \A -)\A(-\A-) )$ はコンテナスキーマ $\mathrm{BinTree}$ の形状のひとつです。この形状の位置の集合は

$\quad \Pos^\mathrm{BinTree}( ( (- \A -)\A(-\A-) ) ) = \{1, 2, 3, 4\}\;\in |{\bf FinSet}|$

なので、 $3$ は形状 $( (- \A -)\A(-\A-) )$ の位置になります。意味的には、三番目のプレースホルダーを指します。

コンテナスキーマ $C$ の形状 $s\in \Shp^C$ と任意の集合 $A$ に対して、写像 $a:\Pos^C(s) \to A$ を考えて、ペア $(s, a)$ を形状付きデータ〈shaped data〉といいます。もっと正確な呼び名は、 $s$ -形状の $A$ 値データ〈s-shaped A-valued data〉です。

写像 $a$ を、形状付きデータ $(s, a)$ の $A$ 値の値割り当て〈value assignment〉、あるいは単に割り当て〈assignment〉と呼びます。

例えば、コンテナスキーマ $\mathrm{BinTree}$ の形状 $( (- \A -)\A(-\A-) )$ に対して次の ${\bf R}$ 値割り当てを考えます。

$\quad a:\Pos^\mathrm{BinTree}( ( (- \A -)\A(-\A-) ) ) = \{1, 2, 3, 4\} \to {\bf R}\\ \Where\\ \qquad a(1) := -1\\ \qquad a(2) := 0\\ \qquad a(3) := \sqrt{2}\\ \qquad a(4) := \frac{1}{2}\\$

これは、リーフに実数値が割り当てられた次の二分木を表します。

$\quad ( (-1 \A 0)\A(\sqrt{2}\A \frac{1}{2}) )$

二分木に限らない一般的なツリー形状／値割り当てに関しては、次の記事に記述があります。

ツリーデータ型のモナド

コンテナスキーマ $C$ の形状 $s \in \Shp^C$ と任意の集合 $A$ に対して、 $s$ -形状の $A$ 値データ〈形状付きデータ〉の全体を $\ShpData^C(s, A)$ と書きます。

$\quad \ShpData^C(s, A)\\ = \{s\}\times \Map(\Pos^C(s), A)\\ \cong \Map(\Pos^C(s), A)$

集合 $A$ は固定した上で、すべての形状に関して形状付きデータを寄せ集めると次のようになります。

$\quad \bigcup_{s\in \Shp^C} \ShpData^C(s, A)\\ \cong \sum_{s\in \Shp^C} \Map(\Pos^C(s), A)$

$C = \mathrm{Triv}$ の場合に形状付きデータの寄せ集めを計算すると：

$\quad \sum_{s\in \Shp^\mathrm{Triv}} \Map(\Pos^\mathrm{Triv}(s), A)\\ = \sum_{s\in \{*\}} \Map(\Pos^\mathrm{Triv}(s), A)\\ = \Map(\Pos^\mathrm{Triv}(*), A)\\ = \Map(\{*\}, A)\\ \cong A$

$\mathrm{Triv}$ の形状付きデータは値の集合 $A$ のデータ〈要素〉と同じでした。

コンテナスキーマのその他の事例

$\mathrm{Emp}, \mathrm{Triv}, \mathrm{BinTree}$ 以外によく使うコンテナスキーマを定義しておきましょう。

リスト〈配列〉データ型を記述するためのコンテナスキーマ $\mathrm{List}$ を定義しましょう。それに先立ち次の約束をしておきます。

$\quad \bar{0} = \{\}\\ \quad \bar{1} = \{1\}\\ \quad \bar{2} = \{1, 2\}\\ \quad \bar{n} = \{1, 2, \cdots, n\}$

$\mathrm{List}$ の定義は：

$\quad \mathrm{List} = (\Shp^\mathrm{List}, \Pos^\mathrm{List})\\ \Where\\ \quad \Shp^\mathrm{List} := {\bf N}\\ \quad \Pos^\mathrm{List} := \lambda\, n\in {\bf N}.(\, \bar{n} \;\in |{\bf FinSet}| \,)$

コンテナスキーマ $\mathrm{List}$ の $A$ 値の形状付きデータを寄せ集めると次のようになります。

$\quad \bigcup_{s\in \Shp^\mathrm{List}} \ShpData^\mathrm{List}(s, A)\\ \cong \sum_{s\in \Shp^\mathrm{List}} \Map(\Pos^\mathrm{List}(s), A)\\ = \sum_{n\in {\bf N}} \Map(\bar{n}, A)$

最近書いた次の記事のなかで、たまたまリストの定義をしています（その一部をこの記事にコピーしました）。

集合論と圏論がズレるとき：空リスト問題

長さ2のリストはペアですが、ペアデータ型を記述するためのコンテナスキーマ $\mathrm{Pair}$ は次のようになります*3。

$\quad \mathrm{Pair} = (\Shp^\mathrm{Pair}, \Pos^\mathrm{Pair})\\ \Where\\ \quad \Shp^\mathrm{Pair} := {\bf 1}\\ \quad \Pos^\mathrm{Piar} := \lambda\, x\in {\bf 1}.(\, \{1, 2\} \;\in |{\bf FinSet}| \,)$

コンテナスキーマ $\mathrm{Pair}$ の $A$ 値の形状付きデータを寄せ集めると次のようになります。

$\quad \bigcup_{s\in \Shp^\mathrm{Pair}} \ShpData^\mathrm{Pair}(s, A)\\ \cong \sum_{s\in \Shp^\mathrm{Pair}} \Map(\Pos^\mathrm{Pair}(s), A)\\ = \Map(\{1, 2\}, A)\\ \cong A\times A$

期待通りの結果ですね。

もうひとつ、「何かを四角形の形に並べる」ことに対応するコンテナスキーマ $\mathrm{Mat}$ （matrix から）を定義しておきます。

$\quad \mathrm{Mat} = (\Shp^\mathrm{Mat}, \Pos^\mathrm{Mat})\\ \Where\\ \quad \Shp^\mathrm{Mat} := {\bf N}\times {\bf N}\\ \quad \Pos^\mathrm{Mat} := \lambda\, (n, m)\in {\bf N}\times {\bf N}.(\, \bar{n} \times \bar{m} \;\in |{\bf FinSet}| \,)$

コンテナスキーマ $\mathrm{Mat}$ の $A$ 値の形状付きデータを寄せ集めると次のようになります。

$\quad \bigcup_{s\in \Shp^\mathrm{Mat}} \ShpData^\mathrm{Mat}(s, A)\\ \cong \sum_{s\in \Shp^\mathrm{Mat}} \Map(\Pos^\mathrm{Mat}(s), A)\\ = \sum_{(n, m)\in {\bf N}\times {\bf N}} \Map(\bar{n}\times \bar{m}, A)$

コンテナ関手

前節で出てきた記号 $\ShpData$ をオーバーロードして使います。以下に出てくるハイフンは引数を入れる位置を示します。

$\ShpData^\hyp(\hyp, \hyp)$ : 前節で述べた、コンテナスキーマに対する形状付きデータの集合。
$\ShpData[\hyp]$ ：この節で述べる、コンテナスキーマから定義される関手。

コンテナスキーマ $C = (\Shp^C, \Pos^C)$ があると、集合圏 ${\bf Set}$ 上の自己関手を定義することができます。その関手を、

$\quad \ShpData[C] : {\bf Set} \to {\bf Set}$

とします。 $\ShpData[C]$ の定義は次のようになります。

$\For A \in |{\bf Set}|\\ \Define \ShpData[C](A) := \bigcup_{s\in \Shp^C} (\{s\} \times \Map(\Pos^C(s), A) )\\ \:\\ \For f:A \to B \In {\bf Set}\\ \Declare \ShpData[C](f) : \ShpData[C](A) \to \ShpData[C](B) \In {\bf Set}\\ \For s\in \Shp^C\\ \For a \in \Map(\Pos^C(s), A)\\ \Define \ShpData[C](f)( (s, a) ) := (s, f\circ a) \;\in (\{s\} \times \Map(\Pos^C(s), B))$

これが実際に ${\bf Set} \to {\bf Set}$ という関手になることは確認できます（練習問題）。このようにして定義される関手を、コンテナスキーマ $C = (\Shp^C, \Pos^C)$ のコンテナ関手〈container functor〉と呼びます。

例えば、コンテナスキーマ $\mathrm{Pair} = (\Shp^\mathrm{Pair}, \Pos^\mathrm{Pair})$ に関して言えば：

$\For A \in |{\bf Set}|\\ \quad \ShpData[\mathrm{Pair}](A) := (\{*\} \times \Map(\{1, 2\}, A) ) \cong A\times A\\ \For f:A \to B \In {\bf Set}\\ \quad \ShpData[\mathrm{Pair}](f) :\cong \lambda\, a\in A\times A.(\, (f(a_1), f(a_2)) \;\in B\times B \,)$

記号の乱用により、関手 $\ShpData[C]$ を単に $C$ とも書きます。例えば $\ShpData[\mathrm{Pair}] = \mathrm{Pair}$ 。慣れてしまえば、コンテナ関手とコンテナスキーマを同一視することもあります。具体例は：

$\quad \mathrm{Emp} = \ShpData[\mathrm{Emp}] : {\bf Set} \to {\bf Set}\\ \quad \mathrm{Triv} = \ShpData[\mathrm{Triv}] : {\bf Set} \to {\bf Set}\\ \quad \mathrm{BinTree} = \ShpData[\mathrm{BinTree}] : {\bf Set} \to {\bf Set}\\ \quad \mathrm{List} = \ShpData[\mathrm{List}] : {\bf Set} \to {\bf Set}\\ \quad \mathrm{Pair} = \ShpData[\mathrm{Pair}] : {\bf Set} \to {\bf Set} \\ \quad \mathrm{Mat} = \ShpData[\mathrm{Mat}] : {\bf Set} \to {\bf Set}$

既存のデータ型から新しいデータ型を作る型構成子〈type constructor〉のなかには、コンテナ関手の対象部分として記述できるものがあります。実際、上記の関手達の対象部分はよく知られた型構成子です。

コンテナスキーマの圏

$C = (\Shp^C, \Pos^C),\, D = (\Shp^D, \Shp^D)$ が2つのコンテナスキーマのとき、そのあいだの準同型射〈homomorphism〉は、写像 $j$ と写像の族 $\varphi_s$ の組で、次のような仕様を持ちます。

$\quad (j, (\varphi_s)_{s \in \Shp^C} )\\ \Where\\ \quad j:\Shp^C \to \Shp^D \In {\bf Set}\\ \quad \For s \in \Shp^C\\ \quad \quad \varphi_s: \Pos^D(j(s)) \to \Pos^C(s) \In {\bf Set}$

$f$ がコンテナスキーマ $C$ から $D$ への準同型射のとき、 $f^\Shp := j, f^\Pos := (\varphi_s)_{s \in \Shp^C}$ という書き方を使います。

$\quad f^\Shp : \Shp^C \to \Shp^D \In {\bf Set}\\ \quad \For s \in \Shp^C\\ \quad \quad f^\Pos_s: \Pos^D(f^\Shp(s)) \to \Pos^C(s) \In {\bf Set}$

形状のあいだの写像 $f^\Shp$ と、位置のあいだの写像 $f^\Pos_s$ で向きが逆なことに注意してください。僕はこれでハマりました。

コンテナスキーマのあいだの準同型射の結合〈合成〉と恒等射の定義は容易に想像できるでしょう。その結合／恒等射により、コンテナスキーマ達とそのあいだの準同型射達は圏 ${\bf ContSchema}$ を形成します。

圏 ${\bf ContSchema}$ の射（コンテナスキーマのあいだの準同型射）の例を幾つか挙げます。

空コンテナスキーマ $\mathrm{Emp}$ は、圏 ${\bf ContSchema}$ の終対象になっています。任意のコンテナスキーマ $C$ から終対象への唯一の射〈終射〉を $!_C$ とすると次のようです。

$\Declare !_C: C \to \mathrm{Emp} \In {\bf ContSchema}\\ \Declare (!_C)^\Shp : \Shp^C \to \Shp^\mathrm{Emp} = {\bf 1} \In {\bf Set}\\ \Define (!_C)^\Shp := \,!_{\Shp^C} = \lambda\, s\in \Shp^C.(\, *\;\in {\bf 1} \,)\\ \For s \in \Shp^C\\ \quad \Declare (!_C)^\Pos_s : \Pos^\mathrm{Emp}( (!_C)^\Shp(s)) \to \Pos^C(s) \In {\bf Set}\\ \quad \Where \Pos^\mathrm{Emp}( (!_C)^\Shp(s)) = \Pos^\mathrm{Emp}( * ) = \emptyset\\ \quad \Define (!_C)^\Pos_s := \theta_{\Pos^C(s)} : \emptyset \to \Pos^C(s)$

ここで、 $\theta_{\Pos^C(s)}$ は空集合からの唯一の写像を表します。これ以外の定義のしようがないので、確かに終射が唯一に決まります。

次に、「二分木形状のリーフだけ見るとリスト形状に見える」ことをコンテナスキーマの準同型射として記述します。 $\mathrm{T2L}$ は Tree to List からです。上線〈overline〉は、 $\bar{n} = \{1, \cdots, n\}$ の意味です。

$\Declare \mathrm{T2L}: \mathrm{BinTree} \to \mathrm{List} \In {\bf ContSchema}\\ \Declare \mathrm{T2L}^\Shp : \Shp^\mathrm{BinTree} \to \Shp^\mathrm{List} = {\bf N} \In {\bf Set}\\ \Define \mathrm{T2L}^\Shp := \lambda\, t\in \Shp^\mathrm{BinTree}.(\, \width(t) \;\in {\bf N} \,)\\ \For t \in \Shp^\mathrm{BinTree}\\ \quad \Declare \mathrm{T2L}^\Pos_t : \Pos^\mathrm{List}( \mathrm{T2L}^\Shp(t)) \to \Pos^\mathrm{BinTree}(t) \In {\bf Set}\\ \quad \Where\\ \qquad \Pos^\mathrm{List}( \mathrm{T2L}^\Shp(t)) = \overline{\width(t)} \\ \qquad \Pos^\mathrm{BinTree}(t) = \overline{\width(t)} \\ \quad \Define \mathrm{T2L}^\Pos_t := \id_{\overline{\width(t)}} : \overline{\width(t)} \to \overline{\width(t)}$

「二分木の最初〈左端〉のリーフを取り出す」ことをコンテナスキーマの準同型射として記述します。 $\mathrm{FL}$ は First Leaf からです。

$\Declare \mathrm{FL}: \mathrm{BinTree} \to \mathrm{Triv} \In {\bf ContSchema}\\ \Declare \mathrm{FL}^\Shp : \Shp^\mathrm{BinTree} \to \Shp^\mathrm{Triv} = {\bf 1} \In {\bf Set}\\ \Define \mathrm{FL}^\Shp := \lambda\, t\in \Shp^\mathrm{BinTree}.(\, * \;\in {\bf 1} \,)\\ \For t \in \Shp^\mathrm{BinTree}\\ \quad \Declare \mathrm{FL}^\Pos_t : \Pos^\mathrm{Triv}( \mathrm{FL}^\Shp(t)) \to \Pos^\mathrm{BinTree}(t) \In {\bf Set}\\ \quad \Where\\ \qquad \Pos^\mathrm{Triv}( \mathrm{FL}^\Shp(t)) = \Pos^\mathrm{Triv}( * ) = \{ * \} = {\bf 1}\\ \qquad \Pos^\mathrm{BinTree}(t) = \overline{\width{t}}\\ \quad \Define \mathrm{FL}^\Pos_t := \lambda\, x\in {\bf 1}.(\, 1 \;\in \overline{\width(t)}\,) : {\bf 1} \to \overline{\width(t)}$

コンテナスキーマの圏から関手圏への関手

前々節で、コンテナスキーマ $C$ に対して集合圏の自己関手 $\ShpData[C]$ を定義しました。この節では、コンテナスキーマのあいだの準同型射 $f:C \to D$ に対して自然変換 $\ShpData[f]$ を定義します。これにより、 $\ShpData$ は次のような関手となります。

$\quad \ShpData: {\bf ContSchema} \to [{\bf Set}, {\bf Set}]$

ここで、 $[{\bf Set}, {\bf Set}]$ は、集合圏の自己関手を対象とする関手圏（射は自然変換）です。サイズの観点からは、圏 $[{\bf Set}, {\bf Set}]$ はだいぶ危ういものですが、ここでは気にしないことにします。

関手圏への関手としての $\ShpData$ を定義していきましょう。

圏 ${\bf ContSchema}$ の対象 $C$ に対する関手圏の対象 $\ShpData[C]$ は既に定義しているので、射 $f:C \to D$ に対する関手圏の射 $\ShpData[f]$ を定義します。 $\ShpData[f]$ の宣言（仕様の記述）は次のようになります。

$\For f:C \to D \In {\bf ContScheme}\\ \Declare \ShpData[f] : \ShpData[C] \to \ShpData[D] \In [{\bf Set}, {\bf Set}]$

外側に巨大な“圏の2圏” ${\bf CAT}$ を想定するなら：

$\For f:C \to D \In {\bf ContScheme}\\ \Declare \ShpData[f] :: \ShpData[C] \twoTo \ShpData[D] : {\bf Set} \to {\bf Set} \In {\bf SET}$

関手圏の射 $\ShpData[f]$ は自然変換なので、その成分達により定義されます。自然変換の成分の宣言は次のようになります。

$\For A \in |{\bf Set}|\\ \Declare \ShpData[f]_A : \ShpData[C](A) \to \ShpData[D](A) \In {\bf Set}$

集合 $\ShpData[C](A)$ は次のような無共分合併〈disjoint union〉で書けます。

$\quad \ShpData[C](A) = \bigcup_{s\in \Shp^C} \ShpData^C(s, A)$

写像 $\ShpData[f]_A$ は、この無共分合併に沿って定義します。具体的には $s\in \Shp^C$ ごとに $(\ShpData[f]_A)_s$ を定義して（下に宣言）、それらを寄せ集めることにします。

$\For s \in \Shp^C\\ \Declare (\ShpData[f]_A)_s : \ShpData^C(s, A) \to \ShpData^D(f^\Shp(s), A) \In {\bf Set}$

定義も書くと：

$\For s \in \Shp^C\\ \Declare (\ShpData[f]_A)_s : \ShpData^C(s, A) \to \ShpData^D(f^\Shp(s), A) \In {\bf Set}\\ \For (s, a) \in \ShpData^C(s, A) \:\Where a:\Pos^C(s) \to A \In {\bf Set}\\ \Define (\ShpData[f]_A)_s( (s, a) ) := (f^\Shp(s), a\circ f^\Pos_s ) \in \ShpData^D(f^\Shp(s), A)$

今までの定義をまとめてひとつにすると：

$\For f:C \to D \In {\bf ContScheme}\\ \Declare \ShpData[f] : \ShpData[C] \to \ShpData[D] \In [{\bf Set}, {\bf Set}] \\ \For A \in |{\bf Set}|\\ \Declare \ShpData[f]_A : \ShpData[C](A) \to \ShpData[D](A) \In {\bf Set}\\ \For s \in \Shp^C\\ \Declare (\ShpData[f]_A)_s : \ShpData^C(s, A) \to \ShpData^D(f^\Shp(s), A) \In {\bf Set}\\ \For (s, a) \in \ShpData^C(s, A) \:\Where a:\Pos^C(s) \to A \In {\bf Set}\\ \Define (\ShpData[f]_A)_s( (s, a) ) := (f^\Shp(s), a\circ f^\Pos_s ) \in \ShpData^D(f^\Shp(s), A)$

これで、成分が定義できました。が、自然変換であるためには自然性が必要です。次節でそれを示しましょう。

形状付きデータのデータ変換の自然性

前節の定義で、形状 $s\in \Shp^C$ ごとに写像 $\ShpData^C(s, A) \to \ShpData^D(f^\Shp(s), A)$ が得られました。この写像は、形状付きデータを形状付きデータに変換するので、形状付きデータのあいだのデータ変換と言っていいでしょう。特定の形状に対する変換ではなく、コンテナスキーマに属するすべての形状に対するデータ変換の族です。

形状付きデータは形状だけでなく値〈成分 | エントリ〉の集合にも依存しますが、値の集合のあいだの写像について自然性を持ちます。そのことは次の図式の可換性として表現されます。

$\require{AMScd} \For f:C \to D \In {\bf ContSchema} \\ \For g:A \to B \In {\bf Set} \\ \:\\ \begin{CD} \ShpData[C](A) @>{\ShpData[f]_A}>> \ShpData[D](A) \\ @V{\ShpData[C](g)}VV @VV{\ShpData[D](g)}V\\ \ShpData[C](B) @>{\ShpData[f]_B}>> \ShpData[D](B) \\ \end{CD}\\ \:\\ \text{commutative in }{\bf Set}$

$s\in \Shp^C$ に関して言えば：

$\begin{CD} \ShpData^C(s, A) @>{(\ShpData[f]_A)_s}>> \ShpData^D(f^\Shp(s), A) \\ @V{\ShpData^C(s, g)}VV @VV{\ShpData^D(f^\Pos(s), g)}V\\ \ShpData^C(s, B) @>{(\ShpData[f]_B)_s}>> \ShpData^D(f^\Shp(s), B) \\ \end{CD}\\ \:\\ \text{commutative in }{\bf Set}$

この可換性〈等式〉を、具体的な計算で示します。 $(s, a)\in \ShpData^C(s, A)$ を取ると、時計回りの計算は次のようになります。

$\begin{CD} (s, a) @>>> (f^\Shp(s), a\circ f^\Pos_s ) \\ @. @VVV\\ {} @. (f^\Shp(s), g\circ (a\circ f^\Pos_s) ) \\ \end{CD}$

反時計回りの計算は：

$\begin{CD} (s, a) @. {} \\ @VVV @.\\ (s, g\circ a) @>>> (f^\Shp(s), (g\circ a)\circ f^\Pos_s) ) \\ \end{CD}$

$(f^\Shp(s), g\circ (a\circ f^\Pos_s) ) = (f^\Shp(s), (g\circ a)\circ f^\Pos_s) )$ なので、結果は一致します。これで、 $\ShpData[f]$ が自然変換であることが分かりました。

$\ShpData[\hyp]$ が関手であるためには次の等式も必要です。

$\ShpData[f;g] = \ShpData[f]; \ShpData[g] \In [{\bf Set}, {\bf Set}]$
$\ShpData[\id_C] = \id_{\ShpData[C]} \In [{\bf Set}, {\bf Set}]$

これらも同様なやり方で示せます。

おわりに

圏 ${\bf ContSchema}$ と関手 $\ShpData: {\bf ContSchema} \to [{\bf Set}, {\bf Set}]$ が定義できました。これが、コンテナの議論をするときの基本的な道具です。

圏 ${\bf ContSchema}$ はプレーンな圏として定義しましたが、モノイド積が入ります。標準的な非対称積だけでなく、対称なハンコック・テンソル積〈Hancock's tensor product〉もあります。アルテンキルヒ／レヴィ／スタトン〈Thorsten Altenkirch, Paul Levy, Sam Staton〉の"Higher-Order Containers"によると、デカルト閉圏に出来るようです。

冒頭で触れたように、型理論以外でもコンテナを利用できそうです。コンテナはけっこう汎用的に使える概念のようです。

*1:データ型以外の用途でのコンテナの利用は、いずれそのうち。

*2:有限性の条件を落としてもかまいませんが、実際に出会う多くのコンテナスキーマでは位置の集合は有限集合です。

*3:このペアデータ型は、要素として“同じ型〈集合〉からのペア”しか許しません