/mrsekut-p/IOモナドを圏論的観点から見る

generated at 2/21/2025, 7:09:24 PM
IOモナドを圏論的観点から見る
IOモナドを圏論的観点から見る
 IO a の中でも特に IO String に限定して見る


Kleisli Tripleとの対応
対応クライスリトリプルIOモナド
TO
ηeta
(-)^*ast
hsnewtype O a = O {unO :: String -> (a,String)}

eta :: a -> O a
eta x = O (\s -> (x, s))

ast :: (a -> O b) -> (O a -> O b)
ast f h =
    O (\st -> let
                  (y,st2) = unO h st
                  (z,st3) = unO (f y) st2
              in
                  (z,st3))
Stateモナドの型に合わせている
RealWorldを状態と捉えたStateモナドと見ている


Kleisli Tripleの満たすべき3条件のテスト
①f^*\circ\eta_A=f 
②\eta_A^*=\mathrm{id}_{TA} 
③g^*\circ f^*=(g^*\circ f)^* 
準備.hsf1 :: Integer -> O Integer
f1 x = O (\s -> (x^2,
                 s ++ "^2=" ++ show (x^2)))
f2 :: Integer -> O Float
f2 x = O (\s -> ((sqrt.fromInteger) x,
                 s ++ "sqrt: " ++ (show.sqrt.fromInteger) x))
                 
testArgs = [(v, s) | v <- [10,100],
                     s <- ["", "---", "hello"]]
テスト.hstest1 = unO ((ast f1 . eta) 10) "" == unO (f1 10) ""
test2 = unO (ast eta (f1 10)) "" ==  unO (f1 10) ""
test3 = [unO ((ast f2 . ast f1) (eta v)) s ==
         unO (ast (ast f2 . f1) (eta v)) s |
         (v,s) <- testArgs ]




















以下は、『圏論の歩き方』 p.83~を参考にしたメモ
上の圏論入門のやり方のほうが筋の良さは感じる
↓のほうがシンプルではある


Kleisli Triple(O,\eta,(-)^*)を考える
OA=M\Sigma \times A 
\eta_A(X)=([],x) 
f^*(l,x)=(l\cdot m,y) 
ただしf(x)=(m,y)
hsnewtype O a = O (String, a) deriving (Eq)

eta :: a -> O a
eta x = O ([], x)

ast :: (a -> O b) -> (O a -> O b)
ast f (O (m,x)) = O (m++n, y)
    where O (n, y) = f x
hsinstance Monad O where
	return = eta
	x >>= f = sh f x

記号の説明
Aは型
ex.  Int ,  String , ..
\Sigmaは文字の集合
Haskなら Char 
M Xで、集合Xの元の有限列全体の集合を表す
ここでは\Sigmaは文字の集合なので、M\Sigmaで文字列の集合を表す
HaskならMは [] であり、M\Sigmaは String 
Oは IO 型コンストラクタ
[x,x,x,x]は文字の列
[]は空文字

 IO Int = String × Int 
\eta_\mathrm{Int}:: \mathrm{Int} \to \mathrm{IO}\;\mathrm{Int} 


プログラム
p\_:\mathbb{N}\to M\Sigma \times \mathbb{N} = (O\mathbb{N}) 
こう書いたほうがいいか
 p_: Int -> MΣ × Int = (IO Int)  
関数名を 小文字_ で表すとしよう
examplep_: Int -> String × Int = (IO Int)

stars_ n = ([ *,...,* ], 0)
const_ n = ([], 0)

hello_ n = ([h,e,l,l,o], 0)
world_ n = ([w,o,r,l,d], 0)
(world_ . hello_) n = ([h,e,l,l,o,w,o,r,l,d], 0)

最後の例の簡約過程
exampleworld_ (hello_ w) 
→ world_ (l, x)
→ (l . m, y)
→ world_ ([h,e,l,l,o], 0)
→ ([h,e,l,l,o,w,o,r,l,d], 0)



参考
『圏論入門』 pp.185-190
『圏論の歩き方』 p.83
クライスリトリプル	IOモナド
T	O
η	eta
(-)^*	ast