Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Generic lifting of MonadCont #77

Closed
KingoftheHomeless opened this issue Jul 12, 2020 · 2 comments
Closed

Generic lifting of MonadCont #77

KingoftheHomeless opened this issue Jul 12, 2020 · 2 comments

Comments

@KingoftheHomeless
Copy link

It's possible to define a liftCallCC for any MonadTrans as follows:

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)

This satisfies the uniformity condition as long as you assume callCC is algebraic; that is,

callCC (\exit -> f (g >=> exit) >>= g) = callCC f >>= g

Which should always be true, except perhaps for StateT's instance of MonadCont, since that doesn't satisfy the uniformity condition.

I've sketched a proof here.

This has been used in the wild by @ekmett in free.

Given its usefulness for defining MonadCont instances for novel monad transformers, I feel the generic liftCallCC or some variant thereof should be added to mtl (or transformers).

@chessai
Copy link
Member

chessai commented Jul 13, 2020

Seems reasonable to me. Can @ekmett weigh in here?

@KingoftheHomeless
Copy link
Author

Actually, my assumption that callCC is always algebraic is incorrect.

> let cont = \b -> if b then return () else throwError  "bad"
> evalCont $ runExceptT $ callCC (\c -> c False `catchError` \_ -> c True) >>= cont
Left "bad"
> evalCont $ runExceptT $ callCC (\c' -> (\c -> c False `catchError` \_ -> c True) (cont >=> c') >>= cont)
Right ()

The proof doesn't need the complete power of callCC being algebraic, however. Only this:

   join $ callCC (\exit -> return $ main (exit . return))
== callCC main

(which algebraicity implies).

I have a hard time imagining an implementation of callCC which doesn't satisfy this. ContT's callCC certainly does, and any lifting of callCC using the liftCallCC I defined does too (I've updated the gist to show this).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants