IOモナドを圏論的観点から見る
IO aの中でも特にIO Stringに限定して見る
table:対応
クライスリトリプル IOモナド
T O
η eta
(-)^* ast
code:hs
newtype 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モナドと見ている
①$ f^*\circ\eta_A=f
②$ \eta_A^*=\mathrm{id}_{TA}
③$ g^*\circ f^*=(g^*\circ f)^*
code:準備.hs
f1 :: 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"]
code:テスト.hs
test1 = 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 ]
上の圏論入門のやり方のほうが筋の良さは感じるmrsekut.icon
↓のほうがシンプルではある
$ OA=M\Sigma \times A
$ \eta_A(X)=([],x)
$ f^*(l,x)=(l\cdot m,y)
ただし$ f(x)=(m,y)
code:hs
newtype 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
code:hs
instance 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)
関数名を小文字_で表すとしよう
code:example
p_: Int -> String × Int = (IO Int)
const_ n = ([], 0)
(world_ . hello_) n = (h,e,l,l,o,w,o,r,l,d, 0) 最後の例の簡約過程
code:example
world_ (hello_ w)
→ world_ (l, x)
→ (l . m, y)
→ (h,e,l,l,o,w,o,r,l,d, 0) 参考