[Haskell-cafe] Why does shift's function return result in Cont and reset reinsert result into Cont again?
Dmitriy Matrosov
sgf.dma at gmail.com
Mon Jan 11 10:28:39 UTC 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160111/835115b1/attachment.html>
More information about the Haskell-Cafe
mailing list