[Haskell-cafe] Why does shift's function return result in Cont and reset reinsert result into Cont again?

11 Jan 2016

      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