LiftCallCC

liftCallCC :: (MonadTrans t, Monad (t m), Monad m)
           => CallCC m (t m a) b -> CallCC (t m) a b
liftCallCC callCC main = join . lift . callCC $ \exit ->
  return $ main (lift . exit . return)


Must prove uniformity property:

forall main main'.
   (forall k. lift (main k) = main' (lift . k))
=> lift (callCC main) = liftCallCC callCC main'

We assume callCC satisfies the following property, which I'll call quasi-algebraicity:
forall f.
  join $ callCC (\exit -> return $ f (exit . return))
= callCC f

We also make use of the naturality condition for callCC
(when viewed as a nat. trans from `(_ -> m b) -> m _` to `m _`):

forall f g.
  fmap g (callCC f)
= callCC (\exit -> g <$> f (exit . g))

Proof for uniformity condition is as follows:

  liftCallCC callCC main'
= join . lift . callCC $ \exit -> return $ main' (lift . exit . return)
= { uniformity assumption: main' (lift . (exit . return)) = (lift . main) (exit . return) }
  join . lift . callCC $ \exit -> return $ (lift . main) (exit . return)
= { naturality of return }
  join . lift . callCC $ \exit -> lift <$> return (main (exit . return))
= { lift is a monad morphism }
  join . lift . callCC $ \exit -> lift <$> return (main (exit . lift . return))
= join . lift . callCC $ \exit ->
    lift <$> (\exit' -> return $ main (exit' . return)) (exit . lift)
= { naturality of callCC }
  join . lift . fmap lift . callCC $ \exit -> return $ main (exit . return)
= { lift is a monad morphism: join . lift . fmap lift = lift . join }
  lift . join . callCC $ \exit -> return $ main (exit . return)
= { callCC is quasi-algebraic }
  lift (callCC main)


Must also prove that "liftCallCC callCC" is quasi-algebraic. I.e.
forall f.
  join $ liftCallCC callCC (\exit -> return $ f (exit . return))
= liftCallCC callCC f

Proof:
  join $ liftCallCC callCC (\exit' -> return $ f (exit' . return))
= join $ join . lift . callCC $ \exit ->
    return $ (\exit' -> return $ f (exit' . return)) (lift . exit . return)
= join . join . lift . callCC $ \exit ->
    return $ return $ f (lift . exit . return . return)
= { naturality of return }
  join . join . lift . callCC $ \exit ->
    fmap return $ return $ f (lift . exit . return . return)
= join . join . lift . callCC $ \exit ->
    fmap return $ (\exit' -> return $ f (lift . exit' . return)) (exit . return)
= { naturality of callCC }
  join . join . lift . fmap return . callCC $ \exit ->
    return $ f (lift . exit . return) 
= { lift is a monad morphism: return = lift . return }
  join . join . lift . fmap (lift . return) . callCC $ \exit ->
    return $ f (lift . exit . return) 
= { preservation of composition }
  join . join . lift . fmap lift . fmap return . callCC $ \exit ->
    return $ f (lift . exit . return) 
= { lift is a monad morphism: join . lift . fmap lift = lift . join }
  join . lift . join . fmap return . callCC $ \exit ->
    return $ f (lift . exit . return) 
= { monad laws: join . fmap return = id }
  join . lift . callCC $ \exit ->
    return $ f (lift . exit . return) 
= liftCallCC callCC f