随伴関手 － 米田の補題：復習

７．随伴関手

７．１　米田の補題：復習

米田の補題は次のようになっていた。

局所的に小さな圏\(\mathcal{C}\)と集合の圏\(\mathbf{Set}\)、これらによって作られる関手圏\([\mathcal{C},\mathbf{Set}]\)を考えよう。今、任意の対象\(A \in \mathcal{C}\)と任意の関手\(F: \mathcal{C} \rightarrow \mathbf{Set}\)に対して、
\begin{eqnarray}
[\mathcal{C},\mathbf{Set}](\mathcal{C}(A,-),F) \cong F(A)
\end{eqnarray}
が成り立つ。ただし、\(\mathcal{C}(A,-) : \mathcal{C} \rightarrow \mathbf{Set}\)である。すなわち、これは関手である。このため、\([\mathcal{C},\mathbf{Set}](\mathcal{C}(A,-),F)\)は、関手\(\mathcal{C}(A,-)\)から\(F\)への自然変換である。

米田の補題をHaskellでは、どのようにあらわすことができるであろうか。自然変換は、多相関数(polymorphic function)で表すことができる。従って、型シグネチャで表すと

forall x. (a -> x) -> F x ~= F a

となる。Haskellでは、\(forall \ x\)を省略することができるが、ここでは、\(\mathcal{C}(A,-)\)の部分がどのように表されるかを正確に期するために、\(forall \ x\)をわざわざ付けた。

上の型シグネチャで、\( forall \ x. (a \rightarrow x) \rightarrow F \ x \)は高次の多相関数となっている。また、\(F \ a\)はデータ型である。

それでは少し、例を挙げてみよう。

例１）リスト

リストは関手なので、これを用いると、米田の補題は次のように書き換えられる。
\begin{eqnarray}
[\mathcal{C},\mathbf{Set}](\mathcal{C}(A,-),[- ]) \cong [A]
\end{eqnarray}

また、Haskellで表すと

forall x. (a -> x) -> [x] ~= [a] 

となる。

そこで、左辺を自然変換\(\alpha\)とすると、

α :: forall x. (a -> x) -> [x]

となる。

これは、リストに対する関手と同じなので、

α f = fmap f

と考えることができる。これをクロージャと考えると、これに対する入力は\([a]\)と考えることができる。例えば、\([a1,a2,…,an]\)とすると、

fmap f [a1,a2,…,an] 
=[f(a1),f(a2),…,f(an)] 
=[x1,x2,…,xn] 

となる。

例２）\({\rm Hom}\)集合の関手

関手を\(\mathcal{C}(B,-)\)にしてみよう。この時、\(F(A)\)は\(\mathcal{C}(B,A)\)になることに注意すると、米田の補題から、
\begin{eqnarray}
[\mathcal{C},\mathbf{Set}](\mathcal{C}(A,-), \mathcal{C}(B,-)) \cong \mathcal{C}(B,A)
\end{eqnarray}
となる。これをHaskellで表すと、

forall x. (a -> x) -> (b -> x) ~= (b -> a)

となる。\((b \rightarrow x)\)はリーダーであることに注意しよう。これは、

α :: (a -> x) -> (b -> x)
g :: b -> a

とすると、

α f = f . g

となる。

例３）継続渡し

関手を\(Id\)にしてみよう。米田の補題から、
\begin{eqnarray}
[\mathcal{C},\mathbf{Set}](\mathcal{C}(A,-),Id) \cong Id(A)
\end{eqnarray}
となる。これをHaskellで表すと、

forall x. (a -> x) -> x ~= a

となる。

これも同じように、自然変換を\(\alpha\)とすると、

α :: (a -> x) -> x

α f = f

これは、前に説明した継続渡しである。継続渡しは時間的な推移を表現できることに特徴がある。