Hi. I've read "Introduction to Programming with Shift and Reset" by Kenichi Asai and Oleg Kiselyov , where shift and reset defined as

import Control.Monad.Cont

shift :: ((a -> w) -> Cont w w) -> Cont w a shift f = cont (flip runCont id . f)

reset :: Cont a a -> Cont w a reset = return . flip runCont id

shiftT :: Monad m => ((a -> m w) -> ContT w m w) -> ContT w m a shiftT f = ContT (flip runContT return . f)

resetT :: Monad m => ContT a m a -> ContT w m a resetT = lift . flip runContT return

But why should function f return result in Cont, which i'll unwrap immediately? And why should i reinsert delimited continuation's result into Cont again in reset? Wouldn't it be simpler (better?) to just define shift/reset like

shift' :: ((a -> w) -> w) -> Cont w a shift' = cont

reset' :: Cont w w -> w reset' m = runCont m id

shiftT' :: ((a -> m w) -> m w) -> ContT w m a shiftT' = ContT

resetT' :: Monad m => ContT w m w -> m w resetT' m = runContT m return

Moreover, Bubble-up semantics proof of Cont bubble elimination is (literally) correct only with reset' (below is my bubble implementation, may be i've written it wrong?):

data Bubble w a b = Bubble (a -> Bubble w a b) ((a -> w) -> Bubble w a w) | Value b

instance Monad (Bubble w a) where return x = Value x Value x >>= h = h x Bubble k f >>= h = Bubble (\x -> k x >>= h) f

convBub'2 :: Bubble w a b -> Cont w b convBub'2 (Value x) = return x convBub'2 (Bubble k f) = cont $ \t -> runCont (fC (\x -> runCont (kC x) t)) id where --fC :: (a -> w) -> Cont w w fC = convBub'2 . f --kC :: a -> Cont w b kC = convBub'2 . k

bubbleResetProp :: Eq w => Bubble w a w -> Bool bubbleResetProp b@(Value x) = reset' (convBub'2 b) == x bubbleResetProp b@(Bubble k f) = reset' (convBub'2 b) == reset' (fC (\x -> reset' (kC x))) where --fC :: (a -> w) -> Cont w w fC = convBub'2 . f --kC :: a -> Cont w b kC = convBub'2 . k

infixl 0 === (===) :: a -> a -> a (===) = const

bubbleResetProof :: Bubble w a w -> w bubbleResetProof (Bubble k f) = reset' (cont $ \t -> runCont (fC (\x -> runCont (kC x) t)) id) === runCont (cont $ \t -> runCont (fC (\x -> runCont (kC x) t)) id) id === (\t -> runCont (fC (\x -> runCont (kC x) t)) id) id === runCont (fC (\x -> runCont (kC x) id)) id === reset' (fC (\x -> reset' (kC x))) where --fC :: (a -> w) -> Cont w w fC = convBub'2 . f --kC :: a -> Cont w b kC = convBub'2 . k

-- Dmitriy Matrosov