interaction of "local" and "callCC"?

28 Oct 2021

      I've stumbled into a not immediately intuitive distinction when mixing
"local" and "callCC" (from the `transformers` package) with one of:

    * ReaderT e (ContT r m) a
    * ContT r (ReaderT e m) a

Specifically, this concernts the expected `Reader` environment when the
current continuation passed via callCC is invoked.

    * With ContT as the inner monad, the Reader environment of the
      current continuation is not affeced by an enclosing call to
      "local":

        flip runConT finalK $
        flip runReaderT env $ do
            ...
            x <- liftCallCC callCC $ \ k -> do
                local f (ask >>= k)  
                ...
            ask >>= cc x

      in this form, `k` (i.e. `\x -> ask >>= c x`) sees the original
      environment `env` from `runReaderT`, only the first `ask` call
      sees `f env` interposed by `local`. 

    * With ReaderT as the inner monad, the environment of the
      current continuation is affeced by an enclosing call to
      "liftLocal":

        flip runReaderT env $
        flip runConT (lift . finalK) $ do
            ...
            x <- callCC $ \ k -> do
                liftLocal ask local f (lift ask >>= k)  
                ...
            lift ask >>= cc x

      in this form, both `k` and the firt `lift ask` see the modified
      environment `f env` interposed by `liftLocal`. 

Of course in the simple example above, one could just write:

    liftLocal ask local f (lift ask) >>= k

and avoid the issue, but in more complex nesting of code, this can be
rather more difficult.

My intuition is that the behaviour when ContT is the inner monad (first
example) is closer to what one might generally hope to see.

The rationale is that a more flexible definition of `local` and
`liftLocal` might be generalised from taking `f :: env -> env` to taking
`f :: env -> newenv` for some related environment type `newenv`, and in
that case, the second example would no longer typecheck, because the
current continuation would now have to have both `env` and `newenv`
for its environment type.

It seems likely that the different behaviours are largely unavoidable,
because `liftLocal` does not know that there's a current continuation
that might need the original environment, and `callCC` does not know
that the base monad is a `ReaderT` and the current continuation needs to
see the Reader's original environment.

It seems this issue is explicitly covered in the case of StateT:

    -- | Uniform lifting of a @callCC@ operation to the new monad.
    -- This version rolls back to the original state on entering the
    -- continuation.
    liftCallCC :: CallCC m (a,s) (b,s) -> CallCC (StateT s m) a b
    liftCallCC callCC f = StateT $ \ s ->
        callCC $ \ c ->
        runStateT (f (\ a -> StateT $ \ _ -> c (a, s))) s
    {-# INLINE liftCallCC #-}

    -- | In-situ lifting of a @callCC@ operation to the new monad.
    -- This version uses the current state on entering the continuation.
    -- It does not satisfy the uniformity property (see "Control.Monad.Signatures").
    liftCallCC' :: CallCC m (a,s) (b,s) -> CallCC (StateT s m) a b
    liftCallCC' callCC f = StateT $ \ s ->
        callCC $ \ c ->
        runStateT (f (\ a -> StateT $ \ s' -> c (a, s'))) s
    {-# INLINE liftCallCC' #-}

where in the "Signatures" module we see:

    -- | Signature of the @callCC@ operation,
    -- introduced in "Control.Monad.Trans.Cont".
    -- Any lifting function @liftCallCC@ should satisfy
    --
    -- * @'lift' (f k) = f' ('lift' . k) => 'lift' (cf f) = liftCallCC cf f'@
    --
    type CallCC m a b = ((a -> m b) -> m a) -> m a

Playing with a prototype "flat" (ContT + ReaderT) monad:

    newtype RContT e r m a =
        RContT { runRContT :: (a -> e -> m r) -> e -> m r }

which directly supports both ReaderT and ContT features, I found it
natural to define a "local" that can change the environment type, and
then of course had no choice but to pass an unmodified enviroment to the
current continuation.

    local :: (e -> e')
          -> RContT e' r m a
          -> RContT e r m a
    local f m = RContT $ \k e -> runRContT m (\a _ -> k a e) (f e)

    callCC :: ((a -> RContT e' r m b)
           -> RContT e r m a)
           -> RContT e r m a
    callCC f = RContT $ \k e -> runRContT (f (\x -> RContT (\_ _ -> k x e))) k e

I don't know where it might be appropriate to document "correct" use of
callCC in transformer stacks with `ReaderT` environments.  Perhaps it
would be reasonable to document that one should generally have "ContT"
just above the base monad, and use "liftCallCC" upstairs, rather than
use "liftLocal" from ContT, unless of course one wants the current
continuation to be exposed to a modified environment in some cases.

Is there an expected "uniformity" property here that's not covered
by the "Signatures"?

-- 
    Viktor.

interaction of "local" and "callCC"?

Viktor Dukhovni