圏論をデータベースに応用する（２）

５．４　セッターとゲッターの関手を一般化する

前回の記事の中で、説明の中心となっていた\(Store \ a \)という関手は、代数的データ型を用いて、

data Store a s = (a, a -> s)

で定義した。しかしこれはデータベースでのセッターとゲッターを分かりやすくするための便宜的な方法である。すなわち、これらの操作でデータ型が変化しないように、

get :: s -> a
set :: s -> a -> s

としたためである。

しかし、セッターでは、フィールドに書き込むデータが、今までに書き込まれていたデータ型とは異なる可能性もある。その結果、レコードのデータ型も影響を受けるので、セッターとゲッターの型シグネチャは、一般的には

get :: s -> a
set :: s -> b -> t

となる。これに対応させて、代数的データ型を定義すると、

data IStore a b t = (a, b -> t)

となる。データ型の変化を許す\(IStore\)はインデックス付き\(Store\)と呼ばれる。このため、\(Store\)の前に\(I\)がついている。しかし、タプルのかたちでは使いにくいので、\(IStore\)を次のように定義しなおして、以下ではこれを利用することにしよう(とはいっても、証明に入ると元の形で用いるので、ご容赦ください)。

data IStore a b t = IStore a (b -> t)

\(Store\)は関手にして用いたが、同じように\(IStore\)も関手として用いる。そのためには関手の概念を拡張したインデックス付き関手\(IxFunctor\)が必要である。

class IxFunctor w where
  imap :: (s -> t) -> w a b s -> w a b t

図１０：インデックス付き関手での\(i map \) (射\(f\)を関手\(W\)で写像\(W(f)\))-図はHaskellでの表現

\(IStore\)は、このインスタンスとなる。

instance IxFunctor IStore where
  imap f (IStore x h) = IStore x (f . x)

インデックス付きのコモナドは、

class IxComonad w where
  iextract :: w a a t -> t
  iduplicate :: w a b t -> w a j (w j b t)

となり、このインスタンスなので、

instance IxComonad IStore where
  iextract (IStore a h) = h a
  iduplicate (IStore a h) = IStore a (\c -> IStore c h) 

となる。

さらに、F-余代数は、圏\(\mathcal{C}\)とその上の自己関手\(F\)に対して、\(\mathcal{C}\)の対象\(A\)と、\(\mathcal{C}\)の射\(β: A \rightarrow F(A) \)との組\( (A,β) \)である。これを考慮すると、F-余代数は

type ICoalg w s t a b = s -> w a b t

となる。

５．５　コモナドとF-余代数

前回の記事で説明したコモナド余代数について復習しておこう。

Haskellではコモナドを次のように定義した。

class Functor w => Comonad w where
  extract :: w a -> a
  duplicate :: w a -> w (w a)

そして満たさなければならない条件は、

extract . duplicate      = id
fmap extract . duplicate = id
duplicate . duplicate    = fmap duplicate . duplicate

である。
また、F-余代数は

type Coalgebra w a = a -> w a

とし、評価射を

coalge :: Coalgebra w a

で定義した。このとき、

extract . coalg = id
fmap (coalg) . colag = duplicate . coalg

を満足するとき、F-余代数を特別にコモナド余代数と呼んだ。可換図式では次のようになった。

図１１：コモナド余代数になるための条件

これと同じことを、インデックス付き関手に対して、考えてみよう。

1番目の条件は\(iextract\)に関連し、

icoalg_aa :: ICoalg w s t a a
iextract . icoalg__aa  = id

となる。

2番目の条件は\(iduplicate\)に関連する。F-余代数では下図が成り立つ。

図１２：F-余代数の空間-図はHaskellでの表現

図に示すように、

icoalg_ab = s -> w a b t
u = w a b t
v = w a b t'
icoalg_bc = u -> w b c v

とすると、

icoalg_bc . icoalg_ab = s -> w a b t -> w b c (w a b t')

となる。

即ち、2番目の条件は以下のようになる。

icoalg_ab :: ICoalg w s t a b = s -> w a b t
icoalg_bc :: ICoalg w s t b c = s -> w b c t
icoalg_ac :: ICoalg w s t a c = s -> w a c t
icoalg_bc . icoalg_ab = iduplicate . icoalg_ac

可換図式で示すと下図の通りである。コモナド余代数の場合には、コモナドに与えられた射で計算しても、余代数での評価射を用いて計算してもよいこととなる。

図１３：コモナド余代数となるための条件-図はHaskellでの表現

５．６　評価射と代数的データ型\(Lens\)

関手\(Istore\)はコモナドであるので、これをコモナド余代数とするような評価射\(β : s \rightarrow IStore \ a \ b \ t \)を見つけることができれば、これを用いても計算できるようになる。

ここでは、前回の記事で説明した\(Lens\)をとりあげよう。\(Lens\)を最初に定義し、そのあと\(Lens\)が評価射であることを示そう。

\(Lens\)がどのように見出されたのかは不明であるが、これを発見した人はすごいと思う。さらに、\(Lens\)が評価射であることを証明した人も素晴らしいと思う。証明は、Russel O’Connorさんの論文に示されているが、次のような逸話が残っている。実は、Bartosz Milewskiさんも同じころに気がついたそうで、証明が正しいかどうかを確認するために、そのドラフトをRussellさんに送った。そうしたら、Russellさんから同じ趣旨の論文を書いている最中だと言われたそうだ。今回の記事はBartoszさんの説明をベースにまとめたものだ。余談だが、世界は広いので、独創的な研究だと思っているときでも、複数の研究者が取り組んでいることが多い。このため、成果の公表には、戦略が必要だ。

Haskellでは、\(Lens\)は次のように定義している。

type Lens s t a b = forall (f :: * -> *). Functor f => (a -> f b) -> (s -> f t)

\(type\)で定義されているが、これは紛れもなく代数的データ型である。

\(Lens\)の使い方については、前回の記事で説明したが、そのとき用いた関数や変数の型シグネチャを確認しておこう。

車のデータベースに対して次のように定義した。車のレコードは、\(Car\)というデータ型を有し、フィールドには、製造社を示す\(maker\)と仕様を表す\(spec\)がある。仕様はデータ型\(Spec\)で定義し、そのサブフィールドには、車の名前の\(name\)と製造年の\(year\)がある。そして\(makeLenses\)を用いて、これらを\(Lens\)というデータ型にした。

{-# LANGUAGE TemplateHaskell #-}

import Control.Lens

data Car = Car {_maker :: String , _spec :: Spec} deriving Show
data Spec = Spec {_name :: String, _year :: Int} deriving Show 

makeLenses ''Car
makeLenses ''Spec

それでは型シグネチャを調べてみよう。\(Getter\)と\(Setter\)の関数である\( (^.) \) と\( (.~) \)、およびフィールドの名前について求めると次のようになる。

図１４：データ型\(Car\)で用いられているフィールド名の型シグネチャ

これから、ゲッターの\( (^.) \) とセッターの\( (.~) \)は、それぞれ引数\(Getting\)と\(ISetter\)を有し、そのデータ型はいずれも\(Lens\)である。従って、この引数によりアクセスすべき場所を得ていることが分かる。この場所を与えているのが、それぞれのフィールドを表している\(maker, spec, name, year\)だ。いずれもデータ型は\(Lens\)となっていることに気がつく。

これからの話は\(Lens\)が評価射であることを示すものだが、\(maker, spec, name, year\)がそのインスタンスであることを念頭に置いて進めよう。まずは\(Lens\)と\(IStore\)の関係をついて考えてみよう。

\(Lens\)のデータ型の定義で、\(a \rightarrow f \ b \)はフィールドの変更、\(s \rightarrow f \ s \)はレコードの変更と見なせばよい。上記の定義は、前回の説明で見慣れた\( Store \)とはだいぶ異なるように見えると思うが、式を変形すると、

forall (f :: * -> *). (a -> f b) -> (s -> f t)

は、

s -> forall (f :: * -> *). (a -> f b) ->f t

となる。

このように書き換えると

forall (f :: * -> *). (a -> f b) ->f t

と

data IStore a b t = IStore a (b -> t)

すなわち

data IStore a b t = (a, b -> t)

が等しければ、\(Lens \ s \ t \ a \ b = λ s \rightarrow IStore \ a \ b \ t \)となり、\(Lens\)が評価射であることが示される。以下ではこれを示そう。

５．７　米田の補題とグロタンディーク関手

それでは米田の補題を復習しよう。
[米田の補題]
局所的に小さな圏を\(\mathcal{C}\)とする。即ち、任意の対象\(A,B\)に対して、\(A\)から\(B\)への写像の集まりが集合となる圏について考える。このとき、全ての対象\(A\)に対して、\( {\rm Hom}_\mathcal{C} \)関手と呼ばれるものを用意することができ、これは集合の圏\( \mathbf{Set}\)への自然変換を与えるというのが米田の補題である。具体的に表してみよう。

\( {\rm Hom}_\mathcal{C} \)関手は
\begin{eqnarray}
h^A = {\rm Hom}_\mathcal{C} (A,-)
\end{eqnarray}
と表され、これは、任意の対象\(X\)に対して、射\( {\rm Hom}_\mathcal{C}(A,X) \)を与え、任意の写像\(f : X \rightarrow Y\)に対して、射\(f \circ - \)を与える。なお、任意の射\(g \in {\rm Hom}_\mathcal{C}(A,X) \)に対して、\(f \circ g \in {\rm Hom}_\mathcal{C}(A,Y) \)となる。式で表すと、
\begin{eqnarray}
h^A (f) &=& {\rm Hom}_\mathcal{C}(A,f) \\
h^A (f)(g) &=& f \circ g
\end{eqnarray}

図１５：\( {\rm Hom}_\mathcal{C} \)関手

\(F\)を\(\mathcal{C}\)から集合の圏\( \mathbf{Set}\)への関手としよう。このとき米田の補題は「\( h^A\)から\(F\)への自然変換は\(F(A)\)と1対1対応(全単射)である」となる。即ち、
\begin{eqnarray}
Nat_{[\mathcal{C},\mathbf{Set}]} (h^A,F) \cong F(A)
\end{eqnarray}
となる。ただし、\( [\mathcal{C},\mathbf{Set}] \)は、圏\(\mathcal{C}\)から、圏\(\mathbf{Set}\)への関手を射とした圏である。

ここで自然変換が出てきたので、若干の説明を加えておこう。圏\(\mathcal{C}\)からは、関手\( {\rm Hom}_\mathcal{C} (A,-) \)と、(集合の圏へと移す)任意の関手\( F \)が存在し、それぞれは集合の圏\( \mathbf{Set}\)に写像する。このとき、\( {\rm Hom}_\mathcal{C}(A,-) \)から\( F \)へ自然変換が存在し、\(A\)について自然であるというのは、図１０での\(X,Y\)を\(A,B\)に変え、任意の\(B\)に対して、\(A\)から\(B\)への任意の射\(f : A \rightarrow B \)を考えたとき、\(θ_B \circ h^A(f) = F(f) \circ θ_A \)が成り立つことと同じである。図１１にこれを示す。

図１６：米田の補題における自然変換

ところで、米田の補題は\( {\rm Hom}_\mathcal{C} (A,f) (id_A) = f \)を利用することで証明できる。証明はここでは省く。

米田の補題で、\(F\)は、集合の圏\(\mathbf{Set}\)への関手であれば、なんでもよかった。\( {\rm Hom}_\mathcal{C} (B,-) \)は、集合の圏\(\mathbf{Set}\)への関手なので、米田の補題での\(F\)を\( {\rm Hom}_\mathcal{C} (B,-) \)で置き換えると、
\begin{eqnarray}
Nat_{[\mathcal{C},\mathbf{Set}]}({\rm Hom}_\mathcal{C}(A,-),{\rm Hom}_\mathcal{C}(B,-)) \cong {\rm Hom}_\mathcal{C}(B,A)
\end{eqnarray}
を得る。そしてここでの自然変換は、グロタンディーク関手（Grothendieck functor）と呼ばれる。図で示すと次のようになる。

図１７：グロタンディーク関手

圏\(\mathbf{Set} \)の代わりに圏\( [\mathcal{C},\mathbf{Set}] \)を使って表すと下図のようになる。

図１８：グロタンディーク関手(別表現)

これをHasekllで表すと

forall c. (a -> c) -> (b -> c) ≃ (b -> a)

となる。

ここでは、\(A,B\)は局所的に小さな圏\( \mathcal{C} \)の対象であった。それでは、この圏の射を対象とした圏\( [\mathcal{C} , \mathcal{C}]\)を考えてみよう。米田の補題を適用すると
\begin{eqnarray}
Nat_{[ [\mathcal{C} , \mathcal{C}],\mathbf{Set}]} ({\rm Hom}_{[\mathcal{C} , \mathcal{C}]} (g,-), {\rm Hom}_{ [\mathcal{C} , \mathcal{C}]} (h,-)) \cong {\rm Hom}_{ [\mathcal{C} , \mathcal{C}]} (h,g)
\end{eqnarray}
となる。

これはHaskellでは

forall f. (forall c. g c ->  f c) -> (forall c’. h c’ -> f c’) ≃ (forall c. h c -> g c)

となる。

５．８　随伴

随伴の定義は、圏 \( \mathcal{C} \)と\( \mathcal{D} \)、その間の関手\(L:\mathcal{D} \rightarrow \mathcal{C}\)と\(R:\mathcal{C} \rightarrow \mathcal{D}\)において、任意の対象\(A \in \mathcal{C},B \in \mathcal{D} \)に対して\( {\rm Hom}_{\mathcal{C}} (L(B),A) \)と \( {\rm Hom}_{\mathcal{D} } (B,R(A) ) \)とが一対一対応(全単射)であること、すなわち
\begin{eqnarray}
{\rm Hom}_{\mathcal{C}} (L(B),A) \cong {\rm Hom}_{\mathcal{D} } (B,R(A) )
\end{eqnarray}
が成り立つことである。

図１９：随伴

Bartoszさんは、圏 \( \mathcal{C} \)と\( \mathcal{D} \)の代わりに、圏 \( \mathcal{C} \)から圏\( \mathcal{C} \)への関手を対象とした圏\( [\mathcal{C} , \mathcal{C}]\)を用いた場合には、随伴が成り立つことを発見した。すなわち下記の式が成り立つことを示した。
\begin{eqnarray}
{\rm Hom}_{ [\mathcal{C},\mathcal{C}]} (L(g),f) \cong {\rm Hom}_{ [\mathcal{C},\mathcal{C}]} (g,R(f) )
\end{eqnarray}
図で表すと、

図２０：圏\([\mathcal{C},\mathcal{C} ] \)での随伴

この随伴をHaskellで表すと、

forall f. (forall c. (L g) c ->  f c) ≃ (forall c. g c -> (R f) c

となる。

５．９　証明

ここまでは準備だ。ここからが証明で、グロタンディーク関手から\(Lens\)が評価射であることが導き出される。小さな圏\( \mathcal{C} \)から\( \mathcal{C} \)への関手を対象とした圏\( [\mathcal{C} , \mathcal{C}]\)に対してグロタンディーク関手を求めると次のようになる。

\begin{eqnarray}
Nat_{[ [\mathcal{C} , \mathcal{C}],\mathbf{Set}]} ({\rm Hom}_{ [\mathcal{C} , \mathcal{C}]} (g,-), {\rm Hom}_{ [\mathcal{C} , \mathcal{C}]} (h,-)) \cong {\rm Hom}_{ [\mathcal{C} , \mathcal{C}]} (h,g)
\end{eqnarray}
グロタンディーク関手を圏\( [\mathcal{C} , \mathcal{C}]\)に適応したのがミソで、左辺から\(Lens\)の代数的データ型が、右辺からコモナドの機能を有する\(IStore\)のデータ型が導き出され、\(Lens\)が評価射であることが示される。それでは式を変形してみよう。

上の式で、\(g\)を\(L(g)\)で、\(h\)を\(L'(h)\)で置き換えると、
\begin{eqnarray}
\forall f. Nat_{[ [\mathcal{C} , \mathcal{C}],\mathbf{Set}]} ( {\rm Hom}_{ [\mathcal{C} , \mathcal{C}]} (L(g),f), {\rm Hom}_{ [\mathcal{C} , \mathcal{C}]} (L'(h),f))) \cong {\rm Hom}_{ [\mathcal{C} , \mathcal{C}]} (L'(h),L(g) )
\end{eqnarray}
となる。

随伴を用いて書き換えると、
\begin{eqnarray}
\forall f. Nat_{[ [\mathcal{C} , \mathcal{C}],\mathbf{Set}]} ({\rm Hom}_{ [\mathcal{C} , \mathcal{C}]} (g,R(f)), {\rm Hom}_{ [\mathcal{C} , \mathcal{C}]} (h,R'(f))) \cong {\rm Hom}_{ [\mathcal{C} , \mathcal{C}]} (h,R'(L(g)) )
\end{eqnarray}

Haskellで表すと

forall f. (forall c. g c ->R f c) -> (forall c'. h c' -> R' f c') ≃ (forall c. (h c -> R' (L g) c)

だ。

ここで、\(g\)と\(h\)は\( {\rm Hom}_{ \mathcal{C} } \)関手なので、
\begin{eqnarray}
g &=& g^B &=& {\rm Hom}_{ \mathcal{C} } (B,-) \\
h &=& h^T &=& {\rm Hom}_{ \mathcal{C} } (T,-)
\end{eqnarray}
である。\(R(f)\)と\(R’(f)\)も\( {\rm Hom}_{ \mathcal{C} } \)関手なので、
\begin{eqnarray}
{\rm Hom}_{ [\mathcal{C} , \mathcal{C}]} (g,R(f)) & \rightarrow & Nat_{[\mathcal{C} , \mathcal{C}]} (g^B, R(f)) \\
{\rm Hom}_{ [\mathcal{C} , \mathcal{C}]} (h,R'(f)) & \rightarrow & Nat_{[\mathcal{C} , \mathcal{C}]} (h^T, R’(f)) \\
{\rm Hom}_{ [\mathcal{C} , \mathcal{C}]} (h,R'(L(g)) & \rightarrow & Nat_{[\mathcal{C} , \mathcal{C}]} (h^T,R'(L(g))
\end{eqnarray}
となり、これらに米田の補題を適応すると、
\begin{eqnarray}
\forall f. {\rm Hom}_{[ [\mathcal{C} , \mathcal{C}],\mathbf{Set}]} ( R(f(B)), R'(f(T)) ) \cong R'(L(g(T)))
\end{eqnarray}
となる。

ここで、圏論とHaskellの対応関係を示しておこう。ここまでの議論で、左側は、 \( \mathcal{C} \)から \( \mathcal{C} \)への関手を射とした圏\( [\mathcal{C}, \mathcal{C}] \)であり、右側は集合の圏\(\mathbf{Set}\)である。従って、\( (R \ f) \ B \)は出力を\( f(B) \)とする射であることが分かる。いま入力を\(A\)とすると、\( (R^A \ f) \ B \)は\(A\)から\( f(B) \)への射となる。

圏論	Haskell
\(g^B \ C = {\rm Hom}_{ \mathcal{C} } (B,C) \)	\( g \ c = (b \rightarrow c) \)
\(h^T \ C' = {\rm Hom}_{ \mathcal{C} } (T,C') \)	\( h \ c' = (t \rightarrow c') \)
\( (R^A \ f) \ B = {\rm Hom}_{ \mathcal{C} } (A, f(B)) \)	\( (Ra \ f) b = (a \rightarrow f \ b) \)
\( (R'^S \ f) \ T = {\rm Hom}_{ \mathcal{C} } (S, f(T)) \)	\( (R's \ f) t = (s \rightarrow f \ t) \)

これより、上記の左辺をHaskellで表すと、

forall f. (a -> f b) -> (s -> f t) 

となる。これは\(Lens\)の定義そのものである。

右辺を変換してみよう。\(R'\)の中を変形しよう。
\begin{eqnarray}
&& Nat_{[\mathcal{C} , \mathcal{C}]} ( L (g), f) \ where f : {\rm Hom}_{ \mathcal{C} } (A,-) \\
&=& Nat_{[\mathcal{C} , \mathcal{C}]} (g, R (f))
\end{eqnarray}

\(g \ T={\rm Hom}_{ \mathcal{C} } (B,T)\)であること、任意の\(T\)に対して\(Nat_{[\mathcal{C} , \mathcal{C}]} (g \ T, R (f) \ T) \)であることに注意を払って、上記をHaskellで表すと、

forall t. g t -> a -> f t
= (a, g t) -> f t
= (a, b -> t) -> f t

となる。これより、\( L (g) \ T\)はHaskellでは\( (a, b \rightarrow t) \)となる。

圏論	Haskell
\( L (g(T))=(A,{\rm Hom}_{ \mathcal{C}} (B,T)) \)	\( L (g) t =(a, b \rightarrow t) \)

これより、右辺は
\begin{eqnarray}
&& R'(L(g))
&=& R' (A,{\rm Hom}_{ \mathcal{C}} (B,-) )
\end{eqnarray}
となる。従ってHaskellで表すと

R (L (g)) t = s -> (a,b->t)

となる。これの右側\( (a, b \rightarrow t) \)は、コモナドとしての機能を有するセッターとゲッターのための代数的データ型として定義したものである。

data IStore a b t = (a, b -> t)

また、左辺の方は、\(Lens\)のための代数的データ型である。

type Lens s t a b = forall (f :: * -> *). Functor f => (a -> f b) -> (s -> f t)

従って、

Lens s t a b  ≃ s -> IStore a b t

となる。

これにより、\(Lens\)が評価射であることが証明され、めでたしめでたしだ。

情報処理の中で、データベースはとても重要な応用分野である。データベースが、計算についての理論的な根拠を与える圏論と、そして理論的な枠組みの中でプログラミングを可能にしてくれるHaskellとつながった意義はとても大きい。\(Lens\)の発見者は素晴らしい方だと思うし、また\(Lens\)が評価射であることを証明した方もすごいと思う。データベースと圏論の関係については、David I. Spivakがその著書"Category Theory for the Sciences"のなかでも、別の観点から説明している。圏論そしてHaskellが、このように重要な応用分野で利用されることはとても良いことだと思う。

追伸：
最後に、得られた結果を図で示そう。ここには、比較しやすくするために、圏論での表記とHaskellでの記述を合わせて載せた。

図２１：\(Lens\)が評価射であることを証明したときの結論を示したもの。