I have a following Koka snippet here and I would like for someone to explain what happens to stackframes when handlers are invoked. I've tried to make handlers stack frames also visible by printing values & global counters and I have desugared when expression.
effect foo<a> { control foo() : a }
fun main() {
var c:int := 0
val r = (handler {
return(x:int) { println("in RET ctrl: " ++ x.show); x*2 }
control foo() {
c := c + 1
val this_c:int = c
println("in FOO ctrl_1. c is: " ++ c.show)
val r1 = resume(3)
println("in FOO ctrl_2, r1: " ++ r1.show ++ " this_c is: " ++ this_c.show)
r1*3
}
})(fn(){
println("throw first foo")
val first:int = foo()
println("throw second foo, first: " ++ first.show)
val snd:int = foo()
println("got second: " ++ snd.show ++ " RET SUM: " ++ (first + snd).show)
(first + snd)
})
println(r)
}
The result is following:
throw first foo
in FOO ctrl_1. c is: 1
throw second foo, first: 3
in FOO ctrl_1. c is: 2
got second: 3 RET SUM: 6
in RET ctrl: 6
in FOO ctrl_2, r1: 12 this_c is: 2
in FOO ctrl_2, r1: 36 this_c is: 1
108
How TWO "FOO_CTRL" handler frames are now underneath the original FN() invocation as well as RET handler?
I'm not sure if this is the terminology usually used for Koka, but here's an answer based on my general knowledge of delimited continuations:
The first time foo() is invoked, it has access to the continuation (call it k1):
val first:int = HOLE
println("throw second foo, first: " ++ first.show)
val snd:int = foo()
println("got second: " ++ snd.show ++ " RET SUM: " ++ (first + snd).show)
(first + snd)
Note that if foo() did not invoke this continuation, it would just go away. In terms of stack frames, that frame is no longer on the call stack; it's been reified as a function. The call stack looks like this:
foo (resume=k1)
<handle frame>
main
But the first foo() does in fact invoke this continuation: resume(3). Now the stack looks like this:
k1
foo (resume=k1)
<handle frame>
main
k1 eventually calls foo again. Its argument continuation (call it k2) starts with val snd:int = HOLE. But the first foo has established the prompt again, so that the call stack becomes:
foo (resume=k2)
foo (resume=k1)
<handle frame>
main
Then the second foo invokes resume (=k2).
When the first foo invoked resume, it first inserted a new prompt for the effect, so that when the effect is invoked the part of the call stack which is captured and removed ends above the existing foo frame, not the <handle frame>. A handler for a different effect established before the foo handler would not have matched the established prompt, so would have captured and removed every instance of foo on the stack.
Unfortunately, try as I might I have not yet found a definitive source stating that, of the variety of possible control operations possible for use with multi-prompt delimited continuations, Koka's resume is the one which establishes a new prompt before invoking the captured delimited continuation. I can only infer it from the behavior you have pointed out.