4.9 Delimited continuations

The predicates reset/3 and shift/1 implement delimited continuations for Prolog. Delimited continuations for Prolog are described in Schrijvers et al., 2013 (preprint PDF). The mechanism allows for proper coroutines, two or more routines whose execution is interleaved, while they exchange data. Note that coroutines in this sense differ from coroutines realised using attributed variables as described in chapter 8.

Note that shift/1 captures the forward continuation. It notably does not capture choicepoints. Choicepoints created before the continuation is captured remain open, while choicepoints created when the continuation is executed live their normal life. Unfortunately the consequences for committing a choicepoint is complicated. In general a cut (!/0) in the continuation does not have the expected result. Negation (\+/1) and if-then(-else) (->/2) behave as expected, provided the continuation is called immediately. This works because for \+/1 and ->/2 the continuation contains a reference to the choicepoint that must be cancelled and this reference is restored when possible. If, as with tabling, the continuation is saved and called later, the commit has no effect. We illustrate the three scenarios using with the programs below.

t1 :-
    reset(gbad, ball, Cont),
    (   Cont == 0
    ->  true
    ;   writeln(resuming),
        call(Cont)
    ).

gbad :-
    n, !, fail.
gbad.

n :-
    shift(ball),
    writeln(n).

Here, the !/0 has no effect:

?- t1.
resuming
n
true.

The second example uses \+/1, which is essentially (G->fail;true).

t2 :-
    reset(gok, ball, Cont),
    (   Cont == 0
    ->  true
    ;   writeln(resuming),
        call(Cont)
    ).

gok :-
    \+ n.

In this scenario the normal semantics of \+/1 is preserved:

?- t1.
resuming
n
false.

In the last example we illustrate what happens if we assert the continuation to be executed later. We write the negation using if-then-else to make it easier to explain the behaviour.

:- dynamic cont/1.

t3 :-
    retractall(cont(_)),
    reset(gassert, ball, Cont),
    (   Cont == 0
    ->  true
    ;   asserta(cont(Cont))
    ).

c3 :-
    cont(Cont),
    writeln(resuming),
    call(Cont).

gassert :-
    (   n
    ->  fail
    ;   true
    ).

Now, t3/0 succeeds twice. This is because n/0 shifts, so the commit to the fail/0 branch is not executed and the true/0 branch is evaluated normally. Calling the continuation later using c3/0 fails because the choicepoint that realised the if-then-else does not exist in the continuation and thus the effective continuation is the remainder of n/0 and fail/0 in gassert/0 .

?- t3.
true ;
true.

?- c3.
resuming
n
false.

The suspension mechanism provided by delimited continuations is used to implement tabling Desouter et al., 2015, (available here). See section 7.

reset(:Goal, ?Ball, -Continuation)

Call Goal. If Goal calls shift/1 and the argument of shift/1 can be unified with Ball,^{74The argument order described in Schrijvers et al., 2013 is reset(Goal,Continuation,Ball). We swapped the argument order for compatibility with catch/3} shift/1 causes reset/3 to return, unifying Continuation with a goal that represents the continuation after shift/1. In other words, meta-calling Continuation completes the execution where shift left it. If Goal does not call shift/1, Continuation are unified with the integer 0 (zero).^{75Note that older versions also unify Ball with 0. Testing whether or not shift happened on Ball however is always ambiguous.}

shift(+Ball)

Abandon the execution of the current goal, returning control to just after the matching reset/3 call. This is similar to throw/1 except that (1) nothing is‘undone' and (2) the 3th argument of reset/3 is unified with the continuation, which allows the code calling reset/3 to resume the current goal.