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
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").
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")
Now my questions to you, acute and knowledgeable reader, are:
- First, is this
jumpoperator as well-behaved as I think? Precisely what kind of effects can trigger an error? Also, can we make the exception
M.Eescape 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?
jumpis a theorem close to, but weaker than double negation elimination it seems.