bitterharvest’s diary

A Bitter Harvestは小説の題名。作者は豪州のPeter Yeldham。苦闘の末に勝ちえた偏見からの解放は命との引換になったという悲しい物語

随伴関手 - 米田の補題:復習

7 随伴関手

7.1 米田の補題:復習

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

局所的に小さな圏\(\mathcal{C}\)と集合の圏\({\rm Set}\)、これらによって作られる関手圏\([\mathcal{C},{\rm Set}]\)を考えよう。今、任意の対象\(A \in \mathcal{C}\)と任意の関手\(F: \mathcal{C} \rightarrow {\rm Set}\)に対して、
\begin{eqnarray}
[\mathcal{C},{\rm Set}](\mathcal{C}(A,-),F) \simeq F(A)
\end{eqnarray}
が成り立つ。ただし、\(\mathcal{C}(A,-) : \mathcal{C} \rightarrow {\rm Set}\)である。すなわち、これは関手である。このため、\([\mathcal{C},{\rm 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\)はデータ型である。

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

例1)リスト

リストは関手なので、これを用いると、米田の補題は次のように書き換えられる。
\begin{eqnarray}
[\mathcal{C},{\rm Set}](\mathcal{C}(A,-),[- ]) \simeq [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] 

となる。

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

関手を\(\mathcal{C}(B,-)\)にしてみよう。この時、\(F(A)\)は\(\mathcal{C}(B,A)\)になることに注意すると、米田の補題から、
\begin{eqnarray}
[\mathcal{C},{\rm Set}](\mathcal{C}(A,-), \mathcal{C}(B,-)) \simeq \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

となる。

例3)継続渡し

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

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

となる。

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

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

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