Generic lifting of MonadCont
KingoftheHomeless opened this issue · 2 comments
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
).
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).