歯抜けリストのジップ：ラックス・モノイド関手の例 - 檜山正幸のキマイラ飼育記 (はてなBlog)

未定義値、あるいは項目の欠損を許すようなリストを歯抜けリスト〈list admitting missing values〉と呼ぶことにしましょう。2つの歯抜けリストのジップ操作を考えると、それはラックス・モノイド関手になります。ラックス・モノイド関手は、プログラミングではアプリカティブ〈applicative〉と呼ばれているものです。

ラックス・モノイド関手自体の説明はこの記事ではしません。次の記事検索などを参照してください。

「ラックス・モノイド」のブログ内検索結果

$\newcommand{\In}{\mbox{ in }}% \newcommand{\On}{\mbox{ on }}% \newcommand{\Iff}{\Leftrightarrow}% \newcommand{\To}{\Rightarrow}% \newcommand{\cat}[1]{\mathcal{#1}}% \newcommand{\Set}{ {\bf Set}}% \newcommand{\For}{\mbox{For }}% \newcommand{\Where}{\mbox{Where }}% \newcommand{\dtimes}{\stackrel{\cdot}{\times}}% \newcommand{\dunit}{\stackrel{\cdot}{ {\bf 1}}}%$ 内容：

歯抜けリスト
付点集合圏からの関手
ジップ操作

歯抜けリスト

リストは、囲み記号にブラケット〈角括弧〉区切り記号にカンマを使って [1, 2, 3] のように書くことにします。一方、ペア（長さ2のタプル）は囲み記号に丸括弧を使って (1, 2) とします。ペアのリストなら、[(1, 2), (2, 1), (3, 2)] のようです。

リストの構成要素を、ここでは項目〈item〉と呼びます。最初の項目は番号1で識別します。プログラミング言語では0始まりが多いですが、ここでは1始まりです。長さ3のリストは [a₁, a₂, a₃] となります。

一部の項目が欠けているようなリストを考えしょう。例えば、[, 2, , 4, 5] は長さ5のリストですが、第1項目と第3項目が欠けています。欠けている項目には、未定義値または欠損値が入っていると考えて、未定義値をボトム記号'⊥'で表すと：

[, 2, , 4, 5] = [⊥, 2, ⊥, 4, 5]

リストの末尾に未定義値を付け足しても同じリストです。

[⊥, 2, ⊥, 4, 5] = [⊥, 2, ⊥, 4, 5, ⊥, ⊥] = [, 2, , 4, 5, ,]

未定義値（⊥）ではない最後の項目位置から後の部分は、すべて未定義値で埋められていると考えることができます。

未定義値、あるいは項目の欠損を許すようなリストを歯抜けリスト〈list admitting missing values〉と呼び、その全体を ListAMV(A) と書きましょう。ここで、Aは項目の型です。例えば、項目の型が整数である歯抜けリストの全体は ListAMV(Z) です。

項目の型Aを集合と解釈し、歯抜けリストの全体 ListAMV(A) も集合と解釈すれば、ListAMV は関手 ListAMV:Set → Set in CAT と解釈できます。関手の射部分〈morphism part〉は次のように（マップ関数として）定義します。

$\For f:A \to B\In \Set\\ \For a = [a_1, \cdots, a_n] \in ListAMV(A)\\ ListAMV(f)(a) := [\hat{f}(a_1), \cdots, \hat{f}(a_n)] \\ \:\:\:\: \mbox{where }\hat{f}(\bot) := \bot,\, \hat{f}(x) := f(x) \mbox{ if }x \ne \bot$

関手性は容易に確認できます。

付点集合圏からの関手

PtSet を付点集合〈pointed set〉の圏とします。圏 PtSet の対象は付点集合で、それは台集合と基点からなります。

A∈|PtSet| ⇔ A = (A, ⊥_A)、A は集合かつ ⊥_A∈A

圏 PtSet の射は、基点を基点に移す写像です。

f:A → B in PtSet ⇔ f:A → B in Set、f(⊥_A) = f(⊥_B)

基点を忘却する関手 U:PtSet → Set in CAT と、基点を追加する関手 Pt:Set → PtSet in CAT は随伴関手ペアになっています。この随伴関手ペアから生成されるモナドがMaybeモナドです。また、Maybeモナドのアイレンベク／ムーア圏が PtSet です。

さて、前節の ListAMV:Set → Set in CAT は集合圏 Set 上の自己関手〈endo functor〉でした。ListAMV をわずかに変更して ListAMV':PtSet → Set in CAT を定義します。ListAMV と ListAMV' の差があまりにわずか過ぎて、識別しにくいので注意してください。

ListAMV'(A) := {x:N_≧1 → A | x(i) ≠ ⊥_A となるiは有限集合}
f:A → B in PtSet に対する ListAMV'(f) in Set の定義は省略（常識的なので）。

ここで、

Aは、圏 PtSet の対象、つまり A = (A, ⊥_A)
N_≧1 は、正の（0ではない）自然数の集合
xは、正自然数の集合から付点集合A（の台集合）への写像
i∈N_≧1 に対する x(i) は“ほとんど”⊥_A。「ほとんど」の意味は、有限個の i を除いて。

x∈ListAMV'(A) のとき、xは x:x:N_≧1 → A という関数ですが、関数値を並べて x = [x₁, x₂, ...] と書けば無限リストです。無限リストの項目の“ほとんど”（上の箇条書き内の説明参照）は⊥_Aなので、無限に続く⊥_A部分を省略すると、歯抜けリストになります。

ListAMV(A) と ListAMV'(A) の違いは、関手の引数〈argument〉であるAが、単なる集合（Set の対象）か付点集合（PtSet の対象）かの違いです。

ジップ操作

集合圏 Set は、集合の直積 $\times$ と“特定された単元集合”〈distinguished singleton set〉 ${\bf 1}$ によりモノイド圏になります。付点集合の圏 PtSet も同様に、付点集合の直積と“特定された単元付点集合”によりモノイド圏になります。付点集合における直積（モノイド積）と単位は、混乱を避けるために $\dtimes,\, \dunit$ とします。

次の等式に注意してください。

$\bot_{A\dtimes B} = (\bot_A, \bot_B)$
$\dunit = (\{\bot_\dunit\}, \bot_\dunit)$

以上の状況設定のもとで、次の同型が成立します。

$\For A, B\in |{\bf PtSet}|\\ ListAMV'(A)\times ListAMV'(B) \cong ListAMV'(A\dtimes B) \In \Set$

この同型を具体的に与える自然変換が、zip〈ジップ〉と unzip〈アンジップ〉と呼ばれる総称関数です。

$zip_{A,B}:ListAMV'(A)\times ListAMV'(B) \to ListAMV'(A\dtimes B) \In \Set\\ unzip_{A,B}:ListAMV'(A\dtimes B) \to ListAMV'(A)\times ListAMV'(B) \In \Set\\$

zip／unzip は2つの関手のあいだの自然同型を与える自然変換になっています。

x = [x₁, ..., x_n] ∈ListAMV'(A) と y = [y₁, ..., y_m] ∈ListAMV'(B) に対する zip(x, y) を定義するとき、通常のリスト（項目の欠損を許さないリスト）だと、長さが異なるケースが面倒ですが、欠損を許すと何も気にしないでジップ操作ができます。

2つの歯抜けリストの短いほうのリストの末尾に ⊥ を足せば、長さが同じと考えることができます。同じ長さの2つの歯抜けリストのジップ操作は次のようにまります。

$\For x = [x_1, \cdots, x_n] \in ListAMV'(A) \\ \For y = [y_1, \cdots, y_n] \in ListAMV'(B) \\ zip_{A,B}(x, y) := [(x_1, y_1), \cdots, (x_n, y_n)]\, \in ListAMV'(A\dtimes B)$

歯抜けリストのアンジップ操作（unzip）は、ペアを分解して2つの歯抜けリストを作ります。

歯抜けリストのジップ操作／アンジップ操作は、モノイド圏のあいだのラックス・モノイド関手〈lax monoidal functor〉、反ラックス・モノイド関手〈oplax monoidal functor | lax comonoidal functor〉、タイト・モノイド関手（ラックスかつ反ラックスなモノイド関手）の事例となります。

ι〈イオタ〉とτ〈タウ〉を次のような写像だとします。

$\iota : {\bf 1} \to ListAMV'(\dunit) \In \Set\\ \tau : ListAMV'(\dunit) \to {\bf 1} \In \Set$