継続モナドを圏論的観点から見る

table:対応

クライスリトリプル継続モナド

T C v

η eta

(-)^* ast

code:hs

newtype 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

https://gyazo.com/daef916621795be487a0780d2dd6c5b0

C v Aは敢えて一つの型引数っぽくCv Aと書いている

Kleisli Tripleの満たすべき3条件のテスト

①$ f^*\circ\eta_A=f

②$ \eta_A^*=\mathrm{id}_{TA}

③$ g^*\circ f^*=(g^*\circ f)^*

code:準備.hs

f1,f2 :: Int -> C Int Int

f1 x = C (\c -> c (x+1))

f2 x = C (\c -> c (x^2))

code:テスト.hs

test1 = 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)

参考