Closed KingoftheHomeless closed 2 years ago
Seems reasonable to me. Can @ekmett weigh in here?
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).
It's possible to define a
liftCallCC
for anyMonadTrans
as follows:This satisfies the uniformity condition as long as you assume
callCC
is algebraic; that is,Which should always be true, except perhaps for
StateT
's instance ofMonadCont
, 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 genericliftCallCC
or some variant thereof should be added tomtl
(ortransformers
).