<div dir="ltr"><div>Hi.<br><br>I've read "Introduction to Programming with Shift and Reset" by Kenichi<br>Asai and Oleg Kiselyov , where shift and reset defined as<br><br>> import Control.Monad.Cont<br>><br>> shift :: ((a -> w) -> Cont w w) -> Cont w a<br>> shift f = cont (flip runCont id . f)<br>><br>> reset :: Cont a a -> Cont w a<br>> reset = return . flip runCont id<br>><br>> shiftT :: Monad m => ((a -> m w) -> ContT w m w) -> ContT w m a<br>> shiftT f = ContT (flip runContT return . f)<br>><br>> resetT :: Monad m => ContT a m a -> ContT w m a<br>> resetT = lift . flip runContT return<br><br>But why should function f return result in Cont, which i'll unwrap<br>immediately? And why should i reinsert delimited continuation's result into<br>Cont again in reset?<br><br>Wouldn't it be simpler (better?) to just define shift/reset like<br><br>> shift' :: ((a -> w) -> w) -> Cont w a<br>> shift'      = cont<br>><br>> reset' :: Cont w w -> w<br>> reset' m    = runCont m id<br>><br>> shiftT' :: ((a -> m w) -> m w) -> ContT w m a<br>> shiftT'     = ContT<br>><br>> resetT' :: Monad m => ContT w m w -> m w<br>> resetT' m   = runContT m return<br><br>Moreover, Bubble-up semantics proof of Cont bubble elimination is (literally)<br>correct only with reset' (below is my bubble implementation, may be i've<br>written it wrong?):<br><br>> data Bubble w a b   = Bubble (a -> Bubble w a b) ((a -> w) -> Bubble w a w)<br>>                     | Value b<br>><br>> instance Monad (Bubble w a) where<br>>     return x            = Value x<br>>     Value x >>= h       = h x<br>>     Bubble k f >>= h    = Bubble (\x -> k x >>= h) f<br>><br>> convBub'2 :: Bubble w a b -> Cont w b<br>> convBub'2 (Value x)     = return x<br>> convBub'2 (Bubble k f)  = cont $ \t -> runCont (fC (\x -> runCont (kC x) t)) id<br>>   where<br>>     --fC :: (a -> w) -> Cont w w<br>>     fC  = convBub'2 . f<br>>     --kC :: a -> Cont w b<br>>     kC  = convBub'2 . k<br>><br>> bubbleResetProp :: Eq w => Bubble w a w -> Bool<br>> bubbleResetProp b@(Value x)    = reset' (convBub'2 b) == x<br>> bubbleResetProp b@(Bubble k f) =<br>>     reset' (convBub'2 b) == reset' (fC (\x -> reset' (kC x)))<br>>   where<br>>     --fC :: (a -> w) -> Cont w w<br>>     fC  = convBub'2 . f<br>>     --kC :: a -> Cont w b<br>>     kC  = convBub'2 . k<br>><br>> infixl 0 ===<br>> (===) :: a -> a -> a<br>> (===) = const<br>><br>> bubbleResetProof :: Bubble w a w -> w<br>> bubbleResetProof (Bubble k f) =<br>>           reset' (cont $ \t -> runCont (fC (\x -> runCont (kC x) t)) id)<br>>       === runCont (cont $ \t -> runCont (fC (\x -> runCont (kC x) t)) id) id<br>>       === (\t -> runCont (fC (\x -> runCont (kC x) t)) id) id<br>>       === runCont (fC (\x -> runCont (kC x) id)) id<br>>       === reset' (fC (\x -> reset' (kC x)))<br>>   where<br>>     --fC :: (a -> w) -> Cont w w<br>>     fC  = convBub'2 . f<br>>     --kC :: a -> Cont w b<br>>     kC  = convBub'2 . k<br><br>--<br></div>    Dmitriy Matrosov<br></div>