Re: [Haskell-cafe] How to make callCC more dynamic
bob zhang wrote:
I thought the right type for ContT should be newtype ContT m a = ContT {runContT :: forall r. (a-> m r) -> m r} and other control operators shift :: Monad m => (forall r . (a-> ContT m r) -> ContT m r) -> ContT m a reset :: Monad m => ContT m a -> ContT m a callCC :: ((a-> (forall r . ContT m r)) -> ContT m a) -> ContT m a unfortunately, I can not make callCC type check, and don't know how to do it.
Precisely that problem was discussed in http://okmij.org/ftp/continuations/undelimited.html#proper-contM Your ContT is CPS1 in the above article. The article shows why you cannot write callCC with the above type of ContT. The article talks about other types. BTW, if you faithfully defined the monad for undelimited control than shift/reset cannot be expressed. Undelimited continuations are strictly less expressible than delimited ones. The above page gives the pointers to the papers with the proof.
Thank you, there is also a nice link here :-) http://stackoverflow.com/questions/7178919/how-to-make-callcc-more-dynamic and for this type, ContT {runContT :: forall r1 . (forall r2 . a-> m r2) -> m r1} callCC can be defined, however, you can not run it, and reset couldn't type check 于 11-8-25 上午1:53, oleg@okmij.org 写道:
bob zhang wrote:
I thought the right type for ContT should be newtype ContT m a = ContT {runContT :: forall r. (a-> m r) -> m r} and other control operators shift :: Monad m => (forall r . (a-> ContT m r) -> ContT m r) -> ContT m a reset :: Monad m => ContT m a -> ContT m a callCC :: ((a-> (forall r . ContT m r)) -> ContT m a) -> ContT m a unfortunately, I can not make callCC type check, and don't know how to do it. Precisely that problem was discussed in http://okmij.org/ftp/continuations/undelimited.html#proper-contM
Your ContT is CPS1 in the above article. The article shows why you cannot write callCC with the above type of ContT. The article talks about other types. BTW, if you faithfully defined the monad for undelimited control than shift/reset cannot be expressed. Undelimited continuations are strictly less expressible than delimited ones. The above page gives the pointers to the papers with the proof.
ContT {runContT :: forall r1 . (forall r2 . a-> m r2) -> m r1} callCC can be defined, however, you can not run it, and reset couldn't type check
Indeed you cannot. As the articles http://okmij.org/ftp/continuations/undelimited.html explain, the answer of _undelimited_ continuation is not available to the program itself. You really cannot write runUndelimitedCont -- just as you cannot write runIO. Once you in the monad of undelimited continuations, you cannot get out of it -- just you cannot get out of IO. Since reset is the composition of runCont and return, reset is not expressible either. The article above explains that in detail (see the CPS2 attempt). The article also shows how to cheat. This exercise points out that undelimited continuations are really not useful. In fact, I don't know of any practical application of them. I'm deeply puzzled why people insist on using callCC given how useless it is by itself (without other effects such as mutation). If one uses callCC and runCont, one deals with _delimited_ continuation. Why not to use shift then, which has a bit more convenient interface. Do you have a specific code that you want to write using ContT? It is generally more productive to discuss a concrete example.
participants (2)
-
bob zhang -
oleg＠okmij.org