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

[Dmitriy Matrosov]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160111/835115b1/attachment.html>