継続モナドを圏論的観点から見る
継続モナドを圏論的観点から見る
Kleisli Tripleとの対応
対応
| クライスリトリプル | 継続モナド |
| T | C v |
| η | eta |
| (-)^* | ast |
hsnewtype C v a = C {unC :: (a -> v) -> v}
eta :: a -> C v a
eta a = C (\c -> c a)
ast :: (a -> C v b) -> (C v a -> C v b)
ast f m = C (\b -> unC m (\a -> unC (f a) b))
-- 型を入れ子の中身から見ていくと
---- unC (f a) :: (b->v)->v
---- unC (f a) b :: v
---- \a -> unC (f a) b :: a->v
---- unC m (\a -> unC (f a) b) :: v
---- \b -> unC m (\a -> unC (f a) b) :: (b->v)->v
C v A は敢えて一つの型引数っぽく Cv A と書いているKleisli Tripleの満たすべき3条件のテスト
①f^*\circ\eta_A=f
②\eta_A^*=\mathrm{id}_{TA}
③g^*\circ f^*=(g^*\circ f)^*
準備.hsf1,f2 :: Int -> C Int Int
f1 x = C (\c -> c (x+1))
f2 x = C (\c -> c (x^2))テスト.hstest1 = unC ((ast f1 . eta) 3) (^2) == unC (f1 3) (^2)
test2 = unC (ast eta (eta 3)) (+1) == unC (eta 3) (+1)
test3 =
unC ((ast f2 . ast f1) (eta 3)) (+1) ==
unC (ast (ast f2 . f1) (eta 3)) (+1)参考
『圏論入門』 pp.190-195