### Escaping continuations

#### by Matthias Puech

Beta had a funny joke at POPL last year; he said: “you exit a monad like you exit a building on fire: by running”. I recently got myself in the stressful situation of being trapped in a monad—the continuation monad—but without a possibility to “run”. There an exit nonetheless: just jump out! This is the (short) story of an escape.

#### A seemingly inescapable monad

Say we have a continuation monad, but its answer type `o`

is fixed in advance:

type o type 'a m = ('a -> o) -> o let ret : 'a. 'a -> 'a m = fun v k -> k v let bind : 'a 'b. 'a m -> ('a -> 'b m) -> 'b m = fun x f k -> x (fun v -> f v (fun v -> k v))

Usually, we consider `o`

, the type of final answers to CPS, to be universally quantified, so that it can be instantiated to whatever we want. Then, as usual, we can run the computation by applying the identity continuation, i.e. we can instantiate type `o`

with `'a`

:

let run : 'a. 'a m -> 'a = fun f -> f (fun x -> x)

But here, we specified explicitly that `o`

was *not* our choice but was fixed (it is abstract), so the previous line gives a typing error: the identity function is *not* a valid continuation to give to our monadic value. I have seen this situation when using delimited continuations: the answer type gets instantiated when you use a local effect somewhere in your program. For instance, one-pass transformations are of this form; their type is in the lines of `exp -> (triv -> ser) -> ser`

(`triv`

is for trivial term, `ser`

for serious term), because when they return from their final continuation, they must be in the context of a serious term.

#### Taking the Midnight Express

What to do then? how do you run a CPS computation when you cannot choose the answer type? Well, there is a way out, involving exceptions: instead of the identity continuation, pass a “trick continuation” that, when called at the end of the computation, will jump out of it (raise an exception) and return to a top-level exception handler. If the initial continuation is actually called, and in the dynamic scope of the exception handler, then we’ll have our result. Here it is:

let jump : 'a 'b. ('a -> 'b m) -> 'a -> 'b = fun (type b) f x -> let module M = struct exception E of b end in try ignore (f x (fun x -> raise (M.E x))); failwith "f was not pure" with M.E i -> i

A local exception is defined, which contains a value of the return type `b`

. This exception is eventually raised in the initial continuation, and the actual return value of function `f`

is ignored, because it is not supposed to return anymore.

So, as you see, `jump`

is turning a function defined in CPS, `f`

, into an “equivalent” direct style function, `jump f`

. Careful! It is equivalent if `f`

is applying its initial continuation, i.e. if `f`

has a pure, direct style counterpart. Otherwise, e.g. if `f`

drops its continuation at one point, then the exception might not be raised, `f`

might terminate and `jump f`

fail with my error `Failure("f was not pure")`

.

#### Examples

Let’s define the function λ*x*. (*x* + 1) = 0 in CPS and then test it on 1:

let isz x = ret (x=0) let succ x = ret (x+1) let () = assert (jump (fun x -> bind (succ x) isz) 0 = false)

I can even use `callcc`

in my programs, which proves that *some* effects are actually OK:

let callcc : 'a 'b. (('a -> 'b m) -> 'a m) -> 'a m = fun f k -> f (fun v x -> k v) (fun v -> k v) let () = assert (jump (fun x -> callcc (fun k -> bind (k x) (fun v -> ret (1 + v)))) 1 = 1)

What I cannot do is instantiate `o`

and bypass the initial continuation:

type o = An_inhabitant let () = ignore (jump (fun x k -> An_inhabitant) 1)

This last example raises the exception `Failure("f was not pure")`

#### Open questions

Now my questions to you, acute and knowledgeable reader, are:

- First, is this
`jump`

operator as well-behaved as I think? Precisely what kind of effects can trigger an error? Also, can we make the exception`M.E`

escape its scope? - Secondly, what does this mean, on the other side of the Curry-Howard looking glass? How can I interpret this result proof-theoretically?
`jump`

is a theorem close to, but weaker than double negation elimination it seems.

Suppose your function f has type ‘a -> (‘b -> ‘c m) m. Then jump f could very well capture the continuation containing the exception.

More generally, you account for the effect of dropping the continuation, but not that of copying the continuation. I doubt jump would work quite as advertised in that many case.

So something like f x = callcc (fun k -> fun y -> throw k x). If you jump twice, you’ll get an incorrect exception.

I don’t quite understand the usecase where this would be a good idea. But that said, it makes some sense to ask the user of such a jump function to make sure that he uses the main continuation in a linear fashion. So the bizarre behaviour exhibited in case of copy may not be too much a problem.

Hi Arnaud,

Thanks, it’s a good remark. I had actually thought about copying the continuation, but could not come up with a working counter-example, that would be well-typed, not instantiate o and make jump f fail. Your example function (fun x -> callcc (fun throw _ -> throw x)) is not well typed because it needs to instantiate o. If you can come up with such a function, you’d make my day!

Ok, the use case was the following: half a dozen mutually-recursive functions written in CPS, each of 50~ lines, doing essentially a big “map” over a complicated data structure (Beluga’s AST)… except for one rare corner case, where it was using a delimited effect. Most of the time, I knew that this rare case would not happen, so I didn’t want to duplicate the whole code, once in CPS and another in Direct Style with an (assert false) in the problematic case. So, I used only the CPS version, and this trick to turn it into DS. Does that sound legit to you?

It is actually pretty easy to come by: pretty much any use of callcc apart from compilation duplicates the continuation (because, quite frankly, why bother otherwise?).

The most obvious example is the excluded middle (it is definitely not pure). Another example is: given callcc I can give you a constant function ‘a -> ‘a for any ‘a. Full code below.

As per your use-case. As long as the type of the argument of the exception is first-order (does not offer a way to capture a continuation) you are, as Guillaume explained, quite safe indeed: exceptions carrying first-order types can be used to model Markov’s principle.

==== Coq code of the two examples ====

Parameter O : Type.

Definition T (A:Type) := (A->O)->O.

Definition ret {A} (x:A) : T A :=

fun k => k x

.

Definition bind {A B} (x:T A) (f:A->T B) : T B :=

fun k => x (fun a => f a k)

.

Definition K (A:Type) := A -> O.

Definition throw {A B} (k:K A) (x:A) : T B :=

fun _ => k x

.

Definition callcc {A} (f:K A -> T A) : T A :=

fun k => f k k

.

Definition em {A} : T(A + (A->T False)) :=

callcc (fun k => ret (inr (fun a => throw k (inl a))))

.

Definition generic_constant {A} : T(A -> T A) :=

callcc (fun (k:K (A->T A)) => ret (fun x => throw k (fun _ => ret x)))

.

Hi Matthias,

I would like to better understand your analogy between answer-type instantiation and the type of one-pass CPS transforms. But, indeed, as you imply, in the proof theory of classical logic one normally needs to be able to choose the return type.

Arnaud beat me to it: For escaping the continuation monad, the issues do not only arise when dropping the continuation but also when the continuation is used multiple times. For your implementation with jump, did you think about some f such that (f x k) calls k on an argument that itself contains k? In this way, when k is (fun x -> raise (M.E x)), then the second copy of (raise (M.E x)) included in the first exception can escape its handler. Thus (as Arnaud said) I would not say that (jump f) is equivalent to (callcc f) “if f is applying its initial continuation, i.e. if f has a pure, direct style counterpart”.

The proof-theoretic counterpart of all this (your second question) is the proof that Peano arithmetic is conservative over Heyting arithmetic for Pi^0_2 statements. These statements can be read as the types of functions from first-order value to first-order values. This notion appears in your question because when x is a first-order value, then it is safe to throw it in an exception: we know that it does not contain other copies of (fun x -> raise (M.E x)). Chet Murthy understood in the early 1990’s that passing the identity continuation was a technique for recovering intuitionistic proofs from classical ones. Before that, there was already a slightly different method by Friedman and by Dragalin that obtains the same effect by replacing the atoms X by (X \/ B). As was already noted by Coquand also in the 1990’s (see ), this technique looks very much like an implementation… of the exception monad.

Hey Guillaume!

First, one-pass transforms. Look at the code for one-pass monadic normal form transform:

let rec exp : e -> s = function

| Var x -> Ret (Var x)

| Lam f -> Ret (Lam (fun x -> exp (f x)))

| App (e1, e2) -> exp’ e1 (fun v1 -> exp’ e2 (fun v2 -> Tail (v1, v2)))

and exp’ : e -> (t -> s) -> s = function

| Lam f -> fun k -> k (Lam (fun x -> exp (f x)))

| App (e1, e2) -> fun k -> exp’ e1 (fun v1 -> exp’ e2 (fun v2 ->

Let (v1, v2, fun v -> k (Val v))))

| Var x -> fun k -> k (Var x)

Function exp’ looks like it’s in CPS, right? except for the App case which introduces a Let (and fixes the answer type to s). So I could actually turn it back in DS, using shift and reset:

let rec exp : e -> s = function

| Var x -> Ret (Var x)

| Lam f -> Ret (Lam (fun x -> exp (f x)))

| App (e1, e2) -> reset (Tail (exp’ v1, exp’ v2))

and exp’ : e -> t = function

| Lam f -> Lam (fun x -> exp (f x))

| App (e1, e2) -> shift (fun k -> Let (exp’ e1, exp’ e2, fun v -> k (Val v)))

| Var x -> Var x

The same goes for one-pass CPS (but I haven’t done it). Is it clearer?

Thanks a lot for the historical logics explanation, it is very helpful. However, you mention Pi_0^2 statements, i.e. that it works under the restriction that the type at stake is a first-order datatype, but it seems to extend to a bit more, no? Consider these two higher-order examples:

jump (fun m -> ret (fun n -> m=n)) 2 2;;

jump (fun f -> ret (f 42)) (fun x -> x);;

I also answered to Arnaud about the double application of the continuation: I have not been able to construct an example of this kind yet, at least not without instantiating the answer type at all…

First, about the second part of your message:

Sure there can be other examples. What’s important with first-order datatypes is that it’s a type-wise criterion, that works on all inhabitants of the type (unless there are other side effects).

As Arnaud said, the excluded middle is the first example that comes to mind. The following works with the code from your post:

# type (‘a,’b) sum = Inl of ‘a | Inr of ‘b

# let wem : unit -> ((‘a,’a->’b m) sum) m = fun () -> callcc (fun k -> ret(Inr(fun a -> k (Inl a))))

val wem : unit -> (‘a, ‘a -> ‘b m) sum m =

Here wem stands for weak excluded middle. Jump gives a right-hand injection:

# let r = jump wem ();;

val r : (‘_a, ‘_a -> ‘_b m) sum = Inr

Something is fishy:

# let boum = match jump wem () with Inr f -> f () | Inl _ -> assert false;;

val boum : ‘_a m =

Indeed:

# boum (fun x -> x);;

Exception: E _.

Guillaume, Arnaud, Thanks for the examples, it was fun!

About the first part: thanks for this “direct-style” one-pass transform. I had not encountered this before. I usually do not think of the “t->s” from one-pass CPS transformations as continuations like others, because they are linear to begin with. Maybe you only intend it as an implementation trick, and I am sure that your use-case is interesting.

So indeed “jump” allows one to run the continuation monad when the limitations of the type system prevents you from applying the identity continuation. Maybe with a richer type system another solution would be to express answer-type polymorphism, but I quite like jump as a pragmatic solution. One just has to ensure that it is safe to run the continuation, which is your job now :)

(A side note since it is the first time that I leave comments on this blog: it would be great if there was some mark-up instruction with the comment form, and also a way to preview. Both my previous messages ended up different from what I intended.)

The link which disappeared: http://www.cse.chalmers.se/~coquand/cor3.ps

Some very helpful context and references from Oleg Kiselyov, with his permission:

“””

Using exceptions or other effects to `escape from continuation’ has been used quite a while. One can get the impression that Strachey and Wadsworth already thought of it. Anyway, the following article makes it clear that some sort of `cheating’ is needed

http://okmij.org/ftp/continuations/undelimited.html#proper-contM

In the original Strachey and Wadsworth’s approach, the side-effect to show the result is printing it. Using mutation to get the result is quite common; see for example the implementation of delimited control in Haskell described in Dybvig, Peyton-Jones and Sabry (JFP 2007). Aborting (throwing an exception) was also used. It was the essential trick in

http://okmij.org/ftp/Computation/dynamic-binding.html#DDBinding

The same trick is needed to emulate answer-type modifying shift-reset using multi-prompt delimited control. It was mentioned in the “Functional unparsing” paper

http://okmij.org/ftp/typed-formatting/index.html#derivation

A student in the lab I am visiting now is formalizing this approach.

As to using exceptions for classical logic programming, long time ago I wrote an article about it

http://okmij.org/ftp/Computation/lem.html

I mentioned that article back in 2009 to Philip de Groote (you might know him). I have heard that he formalized this idea in some recent paper.

Cheers,

Oleg

“””