Steve Awodey. Category Theory を読んで PureScript を書く[第1回(？)・2章]

はじめに

この記事は Steve Awodey の Category Theory を読みつつ出てきた概念を PureScript で実装していくものです．
"第 1 回(？)"というのは，本の途中から書こうと思い立ったので最初からではないからです．(ほぼ最初ですが)
あと現在読んでる最中なので知識はありません．"わからないことはわからないと書く"精神でやりますが，間違ったことを書いてしまうかもしれません．

2.3

終対象$1$から対象$A$への射$1\rightarrow A$は points と呼ばれる．(疑問点: ほかの文献ではドメインが必ずしも$1$とはされていない．用語の違い？)
集合や半順序集合を対象とした圏の場合，射$f:A\rightarrow B$と$g:A\rightarrow B$があって，すべての points $a:1\rightarrow A$について$f\circ a = g\circ a$が成りたてば，$f$と$g$は等しい射．

☆ これは PureScript の圏(Haskell の場合$Hask$なので$Pure$？)でも成り立つのでは？

その前に$Pure$の構成をば

• 対象: kindTypeを持つ型
• 射: 関数

で良いと思うが……

https://myuon.github.io/posts/versus-hask-category/

$Hask$圏は圏にならないらしいです．なんてこった
PureScript は正格評価なのでcall-by-needの問題はないでしょうが，undefinedについてはわからないです．
でもFFIを排除した PureScript にはundefinedは無いかもしれない．ここら辺はあとで考えたいです．

☆ に戻る．$Pure$で言い換えると，
f :: A -> Bと，g :: A -> B があって，任意のa :: Unit -> Aについて(f <<< a) unit == (g <<< a) unitであるとき，任意のe :: Aについて，f e == g e．
となる
(関数fとgの同値をすべてのeについてf e == g eと定義した．)

証明)
任意のe :: Aについて，a = const eとすれば，f e == (f <<< a) unit == (g <<< a) unit === g e

2.4

対象$A$と$B$の積は$P$と$p_1:P\rightarrow A$ $p_2:P\rightarrow A$，の組であり，任意の対象$X$と射$x_1:X\rightarrow A$，$x_2:X\rightarrow B$について，唯一の射$u:X\rightarrow P$が存在して$x_1 = p_1\circ u$，$x_2 = p_2\circ u$を満たすもの

この$u$を$\langle x_1, x_2\rangle$と書く

(考察)これは"一般化された要素"の考え方を使えば，$x_1$は$A$の要素，$x_2$は$B$の要素，$u$は$P$の要素となるので，言い換えれば
「$A$と$B$の直積$P$は$A$の要素$a$と$B$の要素$b$について，唯一の$P$の要素$p$があって$a=p_1(p)$,$b=p_2(p)$となるような$P$」と集合の直積みたいな書き方になるので，お気持ちがわかりやすい(全然的外れかもしれない)

これは直積型と左右それぞれの値を取り出す関数に対応している．

data ProductT a b = Cons a b

p1 :: forall a b. ProductT a b -> a
p1 (Cons a _) = a

p2 :: forall a b. ProductT a b -> b
p2 (Cons _ b) = b

これが上の定義を満たすことは次のような感じで$u$を生成する関数が定義できて

genU :: forall x a b. (x -> a) -> (x -> b) -> x -> ProductT a b
genU x1 x2 x = Cons (x1 x) (x2 x)

これが容易に確かめられるように任意のx :: Xについて
x1 x == (p1 <<< genU x1 x2) xかつx2 x == (p2 <<< genU x1 x2) x
であることから言えるが，その前にこのような関数genUが一意であることを言わなくてはいけない．

ここである関数genU' :: forall x a b. (x -> a) -> (x -> b) -> x -> ProductT a bについて，
x1 x == (p1 <<< genU' x1 x2) xかつx2 x == (p2 <<< genU' x1 x2) x
が成り立つと，すなわち
x1 x == p1 (genU' x1 x2 x)かつx2 x == p2 (genU' x1 x2 x)
だが，p1 と p2 の定義から
genU' x1 x2 x = Cons (x1 x) (x2 x)
となり，これはgenUと等しいので，一意．

あと，クラス化してみる．$a$と$b$の任意の直積の間には同型射が存在するため，次のようなクラスを用意しておけばよい．

class ProductC product a b | product -> a b where
  toProductT :: product -> ProductT a b
  fromProductT :: ProductT a b -> product

2.6

圏$C$において任意の対象 $A$ , $A'$ について対象 $A\times A'$ が存在するとき，
$f:A\rightarrow B$と$f':A'\rightarrow B'$，$A$と$A'$の直積$A\times A', p_1:A×A'\rightarrow A, p_2:A×A'\rightarrow A'$について，$f\times f'=\langle f\circ p_1, f'\circ p_2\rangle:A\times A'\rightarrow B\times B'$
とすると
$\times :C\times C\rightarrow C$
という関手ができる．(疑問点: 二値の関手(？)ってこの本で定義されてた？)

• 証明(関手則を満たす)
  • $1_A\times 1_B=1_{A\times B}$
    $A$と$B$の直積を$A\times B$，$p_1:A\times B\rightarrow A$，$p_2:A\times B\rightarrow B$とする．
    $1_A\times 1_B=\langle 1_A\circ p_1, 1_A\circ p_2\rangle=\langle p_1, p_2\rangle$
    ここで，$\langle p_1, p_2\rangle$は，ある射$u$であって$p_1=p_1\circ u$，$p_2=p_2\circ u$を満たすものであり，$u$の一意性から$u=1_{A\times B}$
  • $f_1:A\rightarrow B$，$f_2:B\rightarrow C$，$g_1:P\rightarrow Q$，$g_2:Q\rightarrow R$について$(f_2\times g_2)\circ (f_1\times g_1)=(f_2\circ f_1)\times (g_2\circ g_1)$
    $A$と$P$の直積を$A\times P$，$p_A:A\times P\rightarrow A$，$p_P:A\times P\rightarrow P$とする．
    $B$と$Q$の直積を$B\times Q$，$p_B:B\times Q\rightarrow B$，$p_Q:B\times Q\rightarrow Q$とする．
    $(f_2\times g_2)\circ (f_1\times g_1)=\langle f_2\circ p_B, g_2\circ p_Q\rangle\circ\langle f_1\circ p_A, g_1\circ p_P\rangle =\langle f_2\circ f_1\circ p_A, g_2\circ g_1\circ p_P\rangle = f_2\circ f_1\times g_2\circ g_1$(一意性から)

後者はかなり端折ってしまった．図式を書けばわかりやすいんですが，書いて埋め込むための安定した手法がいまいちわからないので……

PureScript なら，ProductTがBifunctorのインスタンスになることに対応している．

class Bifunctor f where
  bimap :: forall a b c d. (a -> b) -> (c -> d) -> f a c -> f b d

instance Bifunctor ProductT where
  bimap f g (Cons a b) = Cons (f a) (g b)

もちろん関手則を満たすが，一応確かめる

bimap identity identity
  == \(Cons a b) -> Cons a b
  == identity
bimap f1 g1 <<< bimap f2 g2
  == (\(Cons a b) -> Cons (f1 a) (g1 b)) <<< (\(Cons a b) -> Cons (f2 a) (g2 b))
  == \(Cons a b) -> Cons (f1 <<< f2 $ a) (g1 <<< g2 $ b)
  == bimap (f1 <<< f2) (g1 <<< g2)

2.7

• 定理
  対象$A$，$B$，および$P$，射$p_1:P\rightarrow A$，$p_2:P\rightarrow B$を与え，任意の$X$に対し
  $\vartheta _X:\rm{Hom}(X,P)\rightarrow \rm{Hom}(X,A)\times\rm{Hom}(X,B)$
  を次のように定義する
  $\vartheta _X(x)=(p_1\circ x, p_2\circ x)$
  この時，「$P$が$A$と$B$の直積であること」は，「任意の$X$に対し$\vartheta _X$が(集合間の写像として)同型写像であること」と同値である

$Pure$では$\rm{Hom}(X,P)$はX -> Pであり，$Pure$の対象(これは$CCC$の性質の一部らしい https://scrapbox.io/mrsekut-p/CCC)
(と思ったが，型と集合は似て非なるものだと思っているので，そう考えると$\rm{Hom}(X,P)$ってホンマにX -> Pか？という気持ちになっている)

PureScript で言い換えると次のようになる(？)

---

まず Vartheta($\vartheta$)クラスを定義する

class Vartheta product a b | product -> a b where
  vartheta
    :: forall x
     . (x -> product)
    -> ProductT (x -> a) (x -> b) --Productは集合の意味での直積として使っている
  varthetaInv
    :: forall x
     . ProductT (x -> a) (x -> b)
    -> (x -> product)

-- 条件: 型xが同じなら，vartheta <<< varthetaInv == identityかつvarthetaInv <<< vartheta == identity

任意の型$x$に対して$\vartheta _x$, および$\vartheta _x^{-1}$をがあることを表している($\vartheta _x$が同型写像であることと，逆写像が存在することは同値)

またここでのproduct型変数はaとbの直積である必要はない．

この上で，ある型productが，任意の型xに対して，Vartheta product a bインスタンスを作るときProductC product a bのインスタンスが存在する．さらに，その逆も成り立つ．

---

具体的な構成をする．

instance Vartheta product a b => ProductC product a b where
  toProductT p = Cons (a unit) (b unit)
    where
    Cons a b = vartheta (const p)
  fromProductT (Cons a b) = varthetaInv (Cons (const a) (const b)) unit

instance ProductC product a b => Vartheta product a b where
  vartheta = f
    where
    f p = Cons a b
      where
      a x = p1 $ toProductT (p x)
      b x = p2 $ toProductT (p x)
  varthetaInv = fInv
    where
    fInv (Cons a b) x = fromProductT $ Cons (a x) (b x)

• 定理
  関手$\rm{Hom}(X,-)$は直積を保存する．

PureScript で言い換えると
型a，b，productに対して，ProductC product a bであるとき，任意の型xに対してx -> productとProductC product2 (x -> a) (x -> b)なる型product2の間に同型射がある．

ここでProductC product a bなる任意のproductはProductT a bの間には同型射が存在するので，任意の型a, bとxに対してx -> ProductT a bとProductT (x -> a) (x -> b)の間に同型射がある，と言い換えることができる．

具体的な構成をする．

testHomFunctor
  :: forall a b x
   . (x -> ProductT a b)
  -> ProductT (x -> a) (x -> b)
testHomFunctor p = Cons a b
  where
  a x = p1 $ p x
  b x = p2 $ p x

testHomFunctorInv
  :: forall a b x
   . ProductT (x -> a) (x -> b) -> (x -> ProductT a b)
testHomFunctorInv (Cons a b) x = Cons (a x) (b x)

testHomFunctor <<< testHomFunctorInv == identityとなる．

感想

意外と時間がかかってしまいました．コンスタントに書き続けられるか不安です．あと，色々な具体例が載っていた 2.5 章と練習問題は飛ばしています．PureScript で実装したい内容があったら別記事に書きたいと思います．