🤔

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

2022/01/15に公開約6,900字

はじめに

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

2.3

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

☆ これは 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
となる
(関数fgの同値をすべてのeについてf e == g eと定義した.)

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

2.4

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

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

(考察)これは"一般化された要素"の考え方を使えば,x_1Aの要素,x_2Bの要素,uPの要素となるので,言い換えれば
ABの直積PAの要素aBの要素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と等しいので,一意.

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

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 Bf':A'\rightarrow B'AA'の直積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}
      ABの直積をA\times Bp_1:A\times B\rightarrow Ap_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 up_2=p_2\circ uを満たすものであり,uの一意性からu=1_{A\times B}
    • f_1:A\rightarrow Bf_2:B\rightarrow Cg_1:P\rightarrow Qg_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)
      APの直積をA\times Pp_A:A\times P\rightarrow Ap_P:A\times P\rightarrow Pとする.
      BQの直積をB\times Qp_B:B\times Q\rightarrow Bp_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 なら,ProductTBifunctorのインスタンスになることに対応している.

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

  • 定理
    対象AB,およびP,射p_1:P\rightarrow Ap_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)
    この時,「PABの直積であること」は,「任意の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型変数はabの直積である必要はない.

この上で,ある型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 で言い換えると
abproductに対して,ProductC product a bであるとき,任意の型xに対してx -> productProductC product2 (x -> a) (x -> b)なる型product2の間に同型射がある.

ここでProductC product a bなる任意のproductProductT a bの間には同型射が存在するので,任意の型a, bxに対してx -> ProductT a bProductT (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 で実装したい内容があったら別記事に書きたいと思います.

GitHubで編集を提案

Discussion

ログインするとコメントできます