前回の記事 では,モナドについて説明しました。ここでは,モナドの具体例として,計算機科学でしばしば登場する「リストモナド」と「状態モナド」について,図式を用いて紹介します。
#1:
圏の定義と具体例
#2:
関手と自然変換
#3:
垂直合成と水平合成
#4:
モノイダル圏
#5:
モナドとは自己関手の圏におけるモノイド対象のこと
#6: モナドの例(この記事)
#7:
随伴
Haskellなどの関数型プログラミング言語では,>>=のようなバインド演算がよく用いられます。この演算は各$a,b \in \cC$について実質的にホムセット$\cC(a,Tb)$からホムセット$\cC(Ta,Tb)$への写像を表しており,この写像は積$\mu$を用いて次式のように定まります。
バインド演算による写像$f \mapsto \mu_b \c Tf$
この写像を暫定的に持ち上げとよぶことにして,各$f \in \cC(a,Tb)$に対して$f^\# \coloneqq \mu_b \c Tf \in \cC(Ta,Tb)$とおきます。
まず,リストモナド$\braket{L,\mu,\eta}$(ただし$L \colon \Set \to \Set$)の定義を述べるため,関手$L$と積$\mu$と単位元$\eta$のそれぞれを定めます。
関手$L \colon \Set \to \Set$は,各集合$X \in \Set$を集合$LX \in \Set$に写すものとします。ただし,$LX$は$\braket{x_i}_{i=1}^n$ $~(n \in \Natural,~x_1,\dots,x_n \in X)$の形で表されるもの(つまり$X$の要素からなる有限長のリスト)をすべて集めた集合です。これにより,$L$の対象への作用が定まります。以降では,$\braket{x_i}_{i=1}^n$をしばしば簡略化して$\braket{x_i}_i$のように書きます。$LX$の各要素$\braket{x_i}_i$は次式のように表せます。
$\braket{x_i}_i \in LX$
$$\tag{1}\label{eq:1}$$
また,$L$は各写像$f \in \Set(X,Y)$を写像$Lf \in \Set(LX,LY)$に写します。この写像$Lf$を,「各$\braket{x_i}_i \in LX$を$\braket{f(x_i)}_i \in LY$に写すもの」として定めます。つまり,次の図式を満たすものとします。
式$Lf(\braket{x_i}_i) = \braket{f(x_i)}_i$
これにより,$L$の射への作用が定まります。
積(自然変換)$\mu \colon L \b L \nto L$の各成分$\mu_X$$~(X \in \Set)$は,集合$(L \b L)X$から集合$LX$への写像です。この写像$\mu_X$を
$$ \mu_X \colon (L \b L)X \ni \braket{\braket{x_{i,j}}_i}_j \mapsto \braket{x_{i,j}}_{i,j} \in LX $$
と定めます。$\mu_X$は次の図式で表されます。
式$\mu_X(\braket{\braket{x_{i,j}}_i}_j) = \braket{x_{i,j}}_{(i,j)}$
大ざっぱに述べると,各$\mu_X$は2重のリストを1重のリストに写すような働きをします。
単位元(自然変換)$\eta \colon 1_\Set \nto L$の各成分$\eta_X$$~(X \in \Set)$は,集合$X$から集合$LX$への写像です。この写像$\eta_X$を
$$ \eta_X \colon X \ni x \mapsto \braket{x} \in LX $$
と定めます。$\eta_X$は次の図式で表されます。
式$\eta_X(x) = \braket{x}$
各$\eta_X$は,$X$の各要素$x$を1個の要素のみからなるリスト$\braket{x}$に写します。
リストモナドがモナドである,つまり結合律と単位律を満たすことを確認しておきます。
結合律を満たすことは,各$\braket{\braket{\braket{x_{i,j,k}}_i}_j}_k \in (T \b T \b T)X$に対して次式が成り立つことからわかります。
結合律
単位律を満たすことは,各$\braket{x_i}_i \in TX$に対して次式が成り立つことからわかります。
単位律
持ち上げ$\Set(X,LY) \ni f \mapsto f^\# \in \Set(LX,LY)$を考えます。$f^\#$に各$\braket{x_i}_i \in LX$を入力したときの出力は次式で表されます。
$f^\#(\braket{x_i}_i)$
なお,各$f(x_i)$は$TY$の要素(つまりリスト)です。このため,$\braket{f(x_i)}_i$は$(T \b T)X$の要素(つまりリストのリスト)です。
状態モナド$\braket{T,\mu,\eta}$(ただし$T \colon \Set \to \Set$)の定義を述べます。
以降では,各集合$X,Y$について$\Set(X,Y)$を$Y^X$と書くことにします。集合$S$を任意に選んで固定して,$S$の要素を状態とよぶことにします。このとき,関手$T \colon \Set \to \Set$は,各集合$X \in \Set$を集合$TX \coloneqq (X \times S)^S$に写すものとします。これにより,$T$の対象への作用が定まります。
集合$TX = (X \times S)^S$の各要素$a$は,$S$から$X \times S$への写像です。つまり,$a$は各状態$s \in S$を$X$の要素$x(s)$と状態$t(s)$の組$\braket{x(s),t(s)} \in X \times S$に写します($\braket{x,t}$と書く代わりに,これらが$s$に依存することを表すために$\braket{x(s),t(s)}$と書きました)。$TX$を次の図式で表すことにします。
集合$TX$
左辺と右辺は同じ$TX$を2通りの方法で表したものです。なお,上付き文字$^S$を表す線$S$を下向きの矢印として表しています。また,この矢印と$X \times S$を表す2本の線$X$と$S$の間の境界を,念のため濃いグレーにより強調しています。このとき,$a \in TX$は次式のように表されます。
$a \in TX$の2通りの表記
また,$T$は各写像$f \in \Set(X,Y)$を写像$Tf \in \Set(TX,TY) = \Set((X \times S)^S,(Y \times S)^S)$に写します。この写像$Tf$を,「各写像$h \colon S \to X \times S$を写像$\braket{f,1_S} \c h \colon S \to Y \times S$に写すもの」として定めます。これにより,$T$の射への作用が定まります。写像$h \mapsto Tf(h)$は次の図式で表されます。
写像$h \mapsto Tf(h) \coloneqq \braket{f,1_S} \c h$
このため,$Tf$は次式のように表されます。
$Tf$の2通りの表記
左辺と右辺は同じ$f$を2通りの方法で表したものです。
積(自然変換)$\mu \colon T \b T \nto T$の各成分$\mu_X$$~(X \in \Set)$は,集合$(T \b T)X$から集合$TX$への写像です。写像$\mu_X$を$(T \b T)X = ((X \times S)^S \times S)^S$の各要素,つまり$S \ni s \mapsto \braket{\xi(s),t(s)} \in (X \times S)^S \times S$の形の写像を$TX = (X \times S)^S$の要素である写像$S \ni s \mapsto \xi(s)(t(s)) \in X \times S$に写すものとして定めます。大ざっぱに述べると,$\mu_X$は写像$\xi(s) \colon S \to X \times S$に状態$t(s) \in S$を入力するような働きをします。
写像
$$
\varepsilon_X \colon X^S \times S \ni \braket{h,s} \mapsto h(s) \in X
$$
を次の図式で表すことにします。
写像$\varepsilon_X$
このとき,$\varepsilon_X(h,s) = h(s)$は次式のように表せます。
式$\varepsilon_X(h,s) = h(s)$
直観的には,この左辺は写像$h$に$s$を入力することを表しているとみなせます。$\xi(s)(t(s)) = \varepsilon_{X \times S}(\xi(s),t(s))$を用いると,写像$\mu_X$は次の図式で表されることがわかります。
$\mu_X$の2通りの表記
この右辺が,上で述べた$\mu_X$の具体的な定義を図式で表したものです。
単位元(自然変換)$\eta \colon 1_\Set \nto T$の各成分$\eta_X$$~(X \in \Set)$は,集合$X$から集合$TX$への写像です。この写像$\eta_X$は,各$x \in X$を$TX = (X \times S)^S$の要素である写像$S \ni s \mapsto \braket{x,s} \in X \times S$に写すものとします。$\eta_X$を次の図式で表すことにします。
$\eta_X(x)$の2通りの表記
各$\eta_X$は,集合$X$と集合$S$に対してともに「何もしない」(つまり恒等写像を施す)ような写像です。右辺では,恒等写像$1_S$を表す線$S$を180度曲げたかのような表記をしています。
状態モナドがモナドである,つまり結合律と単位律を満たすことを確認しておきます。ここでは概要のみを説明します。
各集合$X$に対して次式が成り立ちます(このことは,$\{ \varepsilon_X \}_{X \in \Set}$が自然変換であることがわかれば,すぐにわかります)。
結合律
これは,$(\mu \c (1_T \b \mu))X = (\mu \c (\mu \b 1_T))X$を表しています。このため,結合律$\mu \c (1_T \b \mu) = \mu \c (\mu \b 1_T)$が成り立ちます。
各集合$X$に対して次式が成り立ちます。
単位律
このことは,直観的には「くねくねと曲がった線$S$をまっすぐに伸ばしても値は変わらない」と考えると,何となく納得できるかもしれません(随伴の知識があるとすぐに理解できるようになります)。この式は,$(\mu \c (1_T \ot \eta))X = (1_T)X = (\mu \c (\eta \b 1_T))X$を表しています。このため,単位律$\mu \c (1_T \ot \eta) = 1_T = \mu \c (\eta \b 1_T)$が成り立ちます。
持ち上げ$\Set(X,TY) \ni f \mapsto f^\# \in \Set(TX,TY)$を考えます。$f^\#$は次式で表されます。
$f^\#$
リストモナドと状態モナドを,図式を用いて説明しました。詳しい説明は省略しましたが,図式に慣れればきっとこれらのモナドを視覚的にわかりやすく理解できることと思います。