圏が満たさなければならない条件に結合律と単位律があった。結合律は、\(f:A \rightarrow B, g:B \rightarrow C , f:C \rightarrow D \)が存在したとき、これらを合成しての計算結果は、その結合の順番に寄らないというものである。即ち、\(h(gf))=(hg)f\)である。これをストリング・ダイアグラムで表すと図１９となる。図１９：結合律をストリング・ダイアグラムで表す。
単位律は、恒等射と合成しても変化はないというもので、\(I_B f = f = f I_A \)である。ここで、\(I_A : A \rightarrow A, I_B : B \rightarrow B\)はそれぞれ恒等射である。これをストリング・ダイアグラムで表すと図２０となる。図20：単位律をストリング・ダイアグラムで表す。
集合\(S\)とその上の二項演算\(*: S \times S \rightarrow S\)が与えられ、単位元と結合律を満たすとき、\((S,*)\)の組をモノイド(半群)という。単位元を恒等射、集合を射とすることで、上記のように圏として構成できる。対象が一つの圏(単一対象圏)で、射も集合であることから、これは小さい圏である。また、圏のときは、\(S\)の代わりに、モノイド(Monoid)の頭文字をとってモノイド\((M,*)\)あるいはモノイド\(M\)と記されることが多い。上述の自然数での加算はモノイド\((\mathbb{N},+ )\)となる。
それでは、男女が同数であったとしよう。すなわち\(m=n\)としよう。そして私が好きと思っている人は、その人も私を好きと思ってくれている類まれなケースを考えてみよう。これを式で表すと、男子生徒\(a\)が好きな女性\(b\)は、この男子生徒を好きなので、\(g \circ f (a) = a\)となる(ここで\(b=f(a)\))。そして同じ人を好きになることはないので、任意の男子生徒\(a,a'\)に対してそれぞれが好きな女子生徒を\(b,b'\)とすると、\(b \neq b'\)である。女子側から見ると\(f \circ g (b) = b\) となる。自分自身に移す恒等関数を\(i\)とすると、それぞれ\(g \circ f = i\),\(f \circ g = i\)となる。このような写像\(f,g\)は同型写像(isomorphism)と呼ばれ、\(g = f^{-1}\)と記される。同型写像は、全単射となっていることに注意しておこう。なお同型写像であるとき、ドメインとコドメインは同型(isomorphic) であるという。構造的な差異がないということである。
最後に問題です。男子と女子の生徒数が同じであったとし、男子の方も女子の方も、全員が別々の名前を書いたとする。このとき、関数\(f,g\)を何回行ったり来たりすると元に戻るでしょうか？例えば男子\(a\)は女子\(b\)を、女子\(b\)は男子\(c\)を、男子\(c\)は女子\(d\)を、女子\(d\)は男子\(a\)を書いたとすると、\(a \rightarrow b \rightarrow c \rightarrow d \rightarrow a \)となり、２往復で戻ってくる。これは巡回群へと導くがそれについてはまた後で。
この図から対応関係を詳細に検討してみると、二つの圏が随伴となっていることが分かる。詳しい説明は省くが、\(\mathcal{C}\)には、対象として\(A\)と\(A'\)と\(L(B)\)がある。また\(\mathcal{D}\)には、対象として\(B\)と\(R(A)\)と\(R(A')\)とがある。\(\mathcal{C}\)と\(\mathcal{D}\)からそれぞれ任意に一つの対象を取り出し、これを\(X\)と\(Y\)とする。このとき、\(L(Y)\)から\(X\)への射の集合と\(Y\)から\(R(X)\)への射の集合とが１対１の関係にあることを示せばよい。あるいは、\(L \circ R (X) \rightarrow I_\mathcal{C} (X)\)と \(I_\mathcal{D} (Y) \rightarrow R \circ L (Y) \)が成り立つことを示せばよい。証明は省くが成り立つので、ダイアモンド教授の提案は正しいことが分かり、Amazonでのレビューでの懸念は必要ないこととなる。
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
{-# 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
となる。これの右側\( (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が、このように重要な応用分野で利用されることはとても良いことだと思う。
