Mathematics and Computation

A blog about mathematics for computers

Delimited continuations in eff

[UPDATE 2012-03-08: since this post was written eff has changed considerably. For updated information, please visit the eff page.]

**Let's keep the blog rolling! Here are delimited continuations in eff, and a bunch of questions I do not know the answers to.

I am not going to explain what continuations and delimited continuations are, I will just show how to get them in eff. I should also warn you that delimited continuations confuse me deeply. The definition of reset and shift is simple:

effect reset:
  operation shift f: f (lambda x: yield x)

Reset is done with “with reset:“. Shift takes a function as a parameter and passes to it the continuation (delimited by the correspoding with). Here is a basic example:

>>> with reset:
...     shift (lambda k: k(k(k(7)))) * 2 + 1
...
63

Let's see if we understand this. When shift hapens its continuation is “multiply by 2 and add 1”. So k will be the function $x \mapsto 2 x + 1$. Thus $k(k(k(7)))$ is $2 \cdot (2 \cdot (2 \cdot 7 +1) + 1) + 1 = 63$, if I got my arithmetic right.

They say that continuations are the GOTO statement of functional programming:

>>> (with reset: (shift (lambda k: 10)) * 3 + 1) + 2
...
12

This time when shift happens the continuation is “multiply by 3 and add 1”, so $k$ is the map $x \mapsto 3 x + 1$. But shift ignores $k$ and just passes $10$ straight to reset (that's the GOTO), so the answer is $10 + 2 = 12$.

Let us compute the type of shift. The continuation is a function of type $A \to B$. The argument of shift is a function which accepts the continuation so it has type $(A \to B) \to C$. But this only makese sense if the result of shift is the same as the result of the continuation, therefore $C = B$. The type of shift is
$$B^{B^A} \times B^A \to B.$$
As an algebraic operation shift takes a parameter of type $B^{B^A}$, has arity $A$, and the carrier is $B$. This is a bit odd since the type of the parameter depends on the carrier and the arity. As is well known, continuations are not algebraic operations. But it seems like eff is telling us that delimited continuations are algebraic, if we look at them the right way. Indeed, consider the signature $\Sigma$ whose only operation is $\mathtt{shift}$ of type $(B^{B^A}, A)$. A $\Sigma$-algebra is a set $C$ with an operation $\mathtt{shift}_C : B^{B^A} \times C^A \to C$. Would we expect $\mathtt{shift}_C$ to satisfy any equations? By staring at the above definition of shift, we see that we should require, for all $k : A \to C$, $f : B^A \to B$ and $j : C \to B$,
$$j \circ \mathtt{shift}_C(f, k) = f( j \circ k).$$
Strictly speaking, this is not an equation in the sense of universal algebra because we used composition as well as $\mathtt{shift}_C$, whereas classical universal algebra only allows equations involving $\mathtt{shift}_C$. Nevertheless, we are still awfully close to being algebraic. Perhaps we are staring at a monad for delimited continuations? I need to think about this, or be told that someone already has. Also, what are some examples of $\Sigma$-algebras $(C, \mathtt{shift}_C)$, other than delimited continuations?

Since in eff we can have multiple instances of an effect, we get delimited continuations with multiple prompts, i.e., multiple resets. For example, try wrapping your head around the following piece of code:

>>> with io:
...     with reset as promptA:
...         print_string "Batman"
...         with reset as promptB:
...             promptB.shift (lambda k: k (k (promptA.shift (lambda l: l (k (l (k ())))))))
...             print_string "Robin"
...          print_string "Cat woman"
...
Batman
Robin
Robin
Robin
Cat woman
Robin
Robin
Robin
Cat woman
()

I have no idea what this sort of thing is good for, perhaps someone can suggest a useful program with multiple resets.

Comments

Dan Doel

Oleg Kiselyov et al. published a paper a while back that uses delimited continuations with multiple prompts to implement dynamically allocatable (similar to ST), dynamically scoped references. You can see an implementation here.

As for delimited continuation monads, the method I've typically seen of getting shift and reset into the normal Cont monad is:

newtype Cont r a = Cont ((a -> r) -> r)

runCont :: (a -> r) -> Cont r a -> r
runCont k (Cont f) = f k

instance Monad (Cont r) where
    return x = Cont ($x)
    Cont f >>= g = Cont $ \k -> f $ runCont k . g

reset :: Cont a a -> Cont r a
reset m = return (runCont id m)

shift :: ((a -> b) -> Cont b b) -> Cont b a
shift f = Cont $ \k -> runCont id $ f k

This can also be embellished upon, by using indexed monads. The advantage there is that the shift and reset operations can be put in a type class (the changing 'r' parameter in the normal Cont makes that not an option):

newtype ICont r o a = ICont ((a -> o) -> r)

runICont :: (a -> o) -> ICont r o a -> r
runICont k (ICont f) = f k

ireturn :: a -> ICont r r a
ireturn x = ICont ($x)

(>>=) :: ICont r1 r2 a -> (a -> ICont r2 r3 b) -> ICont r1 r3 b
ICont f >>= g = ICont $ \k -> f $ runICont k . g

ireset :: ICont r1 r2 r2 -> ICont r3 r3 r1
ireset m = ireturn (runICont id m)

ishift :: ((a -> b) -> ICont r1 r2 r2) -> ICont r1 b a
ishift f = ICont $ \k -> runICont id $ f k

These don't look quite like what you have above, though. Both shift and reset look like handlers of some kind.

That actually brings up another issue: delimited continuations permit you to reset anywhere for a particular prompt. I should be able to do stuff like:

reset (shift (\k -> reset (shift (\l -> 0)) + (k 5)) + 1)

All with a single prompt. With shift and reset, control effects are unable to escape the captured continuation, so combined with multiple prompts, it may not be a big deal (although you still have to keep track of which prompt you should be shifting to in which scope manually). But there are other delimited control operators where the captured continuation can itself have control effects (that may actually be true in your eff implementation, too). control/prompt is such a set, and so:

[sourcecode gutter="false"] prompt (control (\k -> k 5 + 1) + control (\l -> 0)) = 0 prompt (control (\k -> prompt (k 5) + 1) + control (\l -> 0)) = 1 </pre>

(verified using CC-delcont above; this, of course, assumes left-to-right evaluation order).

(Hopefully I haven't totally screwed up the formatting of this comment.)

Andrej Bauer

@Dan: There are definitely many possibilites regarding delimited control. Regarding resetting anywhere, is this what is supposed to happen: [sourcecode gutter="false" higlight="4,5"] >>> with reset: ... shift (lambda k: (with reset: shift (lambda l: 0)) + (k 5)) + 1 ... Warning: Implicit sequencing between L2, 22-57 and L2, 58-62 6 </pre> And yes, a continuation can definitely have its own control effects in eff.

Dan Doel
Regarding resetting anywhere, is this what is supposed to happen

Yes. The shadowing seems to work there. However,

And yes, a continuation can definitely have its own control effects in eff.

In that case, I think we need more information to decide whether this actually implements shift/reset, or some other set of operators. For instance: with reset: shift (lambda k: k 5 + 1) + shift (lambda l: 0)

For shift/reset semantics, that should be 1. For control/prompt, it's 0. Further, I wonder how the shadowing above works. What answer does: with reset: shift (lambda k: (with reset: k 5) + 1) + shift (lambda l: 0)

give? With a single prompt shift/reset, control/prompt, etc. the answer is 1. If the prompts are distinct, though, a control/prompt-alike will give 0, instead of 1, because, after a bit of munging, we get (I think this is accurate): with reset as p: (with reset as q: 5 + p.shift (lambda l: 0)) + 1

So the shift (control) captures both the (5 +) and the (+ 1), and discards them. Inner resets might actually correspond to a handler (An inner reset p M would correspond to handle M with operation p.shift: ...), but that's just a guess.

There's also, of course, another axis you can vary delimited operators along: whether the shift/control as a block is re-delimited. Operators where it isn't are called (in the only place I've seen them, at least) shift0 and control0. So (going back to something more Haskell like): reset (64 + reset (0 + shift0 (\k -> shift0 (\_ -> k 0)))) = 0 reset (64 + reset (reset (0 + shift0 (\k -> shift0 (\_ -> k 0))))) = 64

and similarly: reset (64 + reset (control0 (\k -> k 5) + control0 (\_ -> 0))) = 0 reset (64 + reset (reset (control0 (\k -> k 5) + control0 (\_ -> 0)))) = 64

but I don't expect that's how the eff works.

Dan Doel

I decided to install and do some testing, and my first result wasn't what I expected: >>> with reset: ... shift (lambda k: k 5 + 1) + shift (lambda l: 0) ... Warning: Implicit sequencing between L2, 3-30 and L2, 31-49 1

So this is indeed shift/reset. That makes the rest of my queries moot, because shift is the so-called static control operator, effectively not letting control effects escape their static scope. That means (I think) that I can't construct any examples that will show an issue with multiple resets, because the inner reset shadows the outer reset in just the right scope to produce correct behavior.

What I don't exactly understand is how this works. :) I guess yield sort of interprets the continuation into a pure function, working out all the control effects. I was actually fiddling with a term algebra for this in Agda yesterday in response to this, so I guess it probably works similarly. For some reason, I wasn't expecting it to.

Andrej Bauer

I suppose we should write a "white paper" that explains the theory. It's really quite simple, there's nothing more to it than free algebras for a given signature and unique homomorphisms from them.

Dan Doel

Here is the result of some messing with Agda based on the article.

The shift/reset monad has a constructor shft : ?{B} ? ((B ? R) ? R) ? (B ? Cont R A) ? Cont R A

which is, of course, conspicuously close to your $R^{R^B} \times C^B \to C$, renaming some variables. The fact that the captured continuation has type (B ? R) of course means that no control effects escape from it, and that the block produces a R means the same thing, although that puts the burden of enforcement on the caller of the operation, instead of the operation itself. Another possibility is ((B ? R) ? Cont R R).

I also have a monad for control/prompt. It requires a negative type definition, though. The fact that the operation has changed to ((B ? Cont R R) -> R) indicates that control effects can escape from calls to the continuation. Here we see the function passed to control taking responsibility for delimiting itself. To avoid this, we could make the change I mentioned, and then change the running functions to: ... reset (shft f k) = reset (f (? x ? reset (k x)))

... prompt (ctrl f k) = prompt (f k) </code>

Is this all close to what's happening in eff?

Presenting the continuations this way, entering and exiting the monad, is actually kind of interesting. When every operation stays in the monad, you get constructions like: data Iterator (M : Set -> Set) (A : Set) : Set where done : Iterator M A yield : A -> (? -> M (Iterator M A)) -> Iterator M A

iterate : {A : Set} -> T A -> CC (Iterator CC A) iterate t = reset (for_ t (\x -> shift (\k -> pure (yield x k))) >> pure done) </code>

for inverting the control of a traversal. With the presentation above, though, this turns into: data Iterator (A : Set) : Set where done : Iterator A yield : A -> (? -> Iterator A) -> Iterator A

iterate : {A : Set} -> T A -> Iterator A iterate t = reset (for_ t (\x -> shift (\k -> yield x k)) >> pure done) </code>

which is clearly just using the traversal to produce a (lazy) list.

How to comment on this blog: At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention andrejbauer@mathstodon.xyz, I will gladly respond. You are also welcome to contact me directly.