处理程序控制堆栈框架如何在 Koka 中相对放置？

Question

我这里有一个 Koka 片段，我希望有人能解释调用处理程序时堆栈帧会发生什么。我试图通过打印值和全局计数器使处理程序堆栈帧也可见，并且我已经在表达式时脱糖。

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)
}

结果如下：

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

两个“FOO_CTRL”处理程序帧现在如何位于原始 FN() 调用和 RET 处理程序之下？

Answer 1

我不确定这是否是通常用于 Koka 的术语，但根据我对定界延续的一般知识，这里有一个答案：

第一次调用 foo() 时，它可以访问延续（称之为 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)

请注意，如果 foo() 没有调用此延续，它就会消失。就堆栈帧而言，该帧不再在调用堆栈上；它被具体化为一个函数。调用堆栈如下所示：

foo (resume=k1)
<handle frame>
main

但是第一个 foo() 实际上调用了这个延续：resume(3)。现在堆栈看起来像这样：

k1
foo (resume=k1)
<handle frame>
main

k1 最终再次调用 foo。它的参数延续（称之为 k2）以 val snd:int = HOLE 开始。但是第一个foo又建立了提示，这样调用栈就变成了：

foo (resume=k2)
foo (resume=k1)
<handle frame>
main

然后第二个 foo 调用 resume (=k2).

当第一个foo调用resume时，它首先插入一个新的效果提示，这样当效果被调用时，调用堆栈中被捕获和移除的部分结束于上面现有的 foo 框架，而不是 <handle frame>。在 foo 处理程序之前建立的不同效果的处理程序不会匹配已建立的提示，因此会捕获并删除堆栈上 foo 的每个实例。

不幸的是，尽我所能，我还没有找到明确的来源说明，在可用于多提示分隔延续的各种可能的控制操作中，Koka 的 resume 是建立在调用捕获的定界延续之前的新提示。我只能从你指出的行为中推断出来。

处理程序控制堆栈框架如何在 Koka 中相对放置？

How handler control stackframes are placed relative to each other in Koka?

delimited-continuations