この図から対応関係を詳細に検討してみると、二つの圏が随伴となっていることが分かる。詳しい説明は省くが、\(\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が、このように重要な応用分野で利用されることはとても良いことだと思う。
都市を動物と同じような生態系と見なすことで、近年では、多くの研究者が都市でのアロメトリの研究に取り組んでいる。その中で大きな成果を上げているのがBettencourt教授だ。彼は２０１３年の論文”The Origins of Scaling in Cities”で、都市の人口とそこでの総生産高の間には、アロメトリが成り立ち、同じ生産高を上げるには大きな都市の方が少ない労力で済むことを示した。また都市には寿命があるとも言っている。
題名がとても長いのだが、説明に用いた論文は以下の通りだ。Hodaka Kawahata (2019) Climatic reconstruction at the Sannai-Maruyama site between Bond events 4 and 3—implication for the collapse of the society at 4.2 ka event. Progress in Earth and Planetary Science.
{-# 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\)の\( ( \verb|^|.) \)では、\(s\)はレコードで、最初の\(a\)はデータを取り出すフィールドで、最後の\(a\)は取り出したデータだ。\(Getting \ a \ s \ a\)は指定されたフィールドからデータを取り出すための関手(あるいは関数)だ。
\(setter\)の\( (. \verb|~|) \)では、\(s\)は入力のレコード、\(t\)は出力のレコード、\(a\)はフィールドで、\(b\)はそのフィールドに書き込む入力値だ。\(ASetter \ s \ t \ a \ b \)は指定されたフィールドを修正した新たなレコードを得るための関手(あるいは関数)だ。
Haskellの関数を簡略化し、ここではアクセスするフィールドの場所が関数の名前の中に含まれる\(getter\)と\(setter\)を、用意することにしよう。そうすると、先ほどの型シグネチャの中の\(Getting \ a \ s \ a\)と\(ASetter \ s \ t \ a \ b \)とが省かれることになるので、次のようになる。
データベースでのこのような操作(図の左側)を、関手(ここではファンクタ\(Store\ a\))で写したのが図の右側である。\(Store \ a \ ( λx \rightarrow (x,b))\)のうち\(a\)は\(get \_1\)の操作を\( ( λx \rightarrow (x,b))\)では\(set \_1\)の操作を表している。これを青色の小文字\( get \_1,set \_1 \)を明示した。カリー化を利用して、\(get \_1 : S \rightarrow A, get \_1 : S \rightarrow A \rightarrow S \)であることに注意して欲しい。
今までの説明は、\(set \_1\)を一回だけ施したものであったが、何回も繰り返した場合はどうなるだろうか。図で示すように\( (x,b)\)を\(Store \ x ( λy \rightarrow (y,b)) \)で置き換えればよい。同じように\( (y,b) \)を置き換えれば、\(set \_1\)を繰り返したときにファンクタ\(Store \ a\)に写された側を得ることができる。ここでもまた青色の小文字\( get \_1,set \_1 \)で明示し、写像された空間での操作が実際どのように表現されるかを明らかにした。
それでは\(Store \ a\)を\(Comonad\)のインスタンスにしてみよう。コモナドは\(extract: W (A) \rightarrow A\)と\(duplicate：W (A) \rightarrow W (W (A)) \)を用意しなければならない。そこで、次のようにしよう。
class (Functor w) => Comonad w where
extract :: w s -> s
duplicate :: w s -> w (w s)
instance Comonad (Store a) where
extract (Store a f) = f a
duplicate (Store a f) = Store a ( \q -> Store q f)
少し使ってみよう。図８：自己関手\(Store\)をコモナドにして利用する
上図では次のことを行っている。現在のレコードの内容を\( (a,b)\)とする。このレコードへのアクセス( \(setter, getter\)による )を、ファンクタ\(Store \ a \)で写した空間で\(Store \ a \ ( λx \rightarrow (x,b))\)と表すことができる。これに\(extract\)を施すと、元の状態の\( (a,b)\)を得る。
\( (a,b)\)に対する２度の繰り返しのアクセスを、\(Store \ a \)に写像した空間では、\(duplicate \ Store \ a \ ( λx \rightarrow (x,b))\)となる。もちろんこれに\(extract\)を２回施すと、元の状態の\( (a,b)\)を得る。
((\s' -> Store (get_1 s’) (set_1 s’)) . (set_1 s)) a1
= (\s' -> Store (get_1 s’) (set_1 s’)) (set_1 s a)
= Store (get_1 (set_1 s a1)) (set_1 (set_1 s a1))
となり、左辺は
(\y -> Store y (set_1 s)) a1
= Store a1 (set_1 s)
となる。これより、それぞれの\(Store\)の項目同士が等しいことから
get_1 (set_1 s a1) = a1
set_1 (set_1 s a1) = set_1 s
