Scala延续的正式定义

在延续插件中实现的Scala分隔延续是对Danvy和Filinski引入的移位和复位控制操作符的改编.参见他们的抽象控制和代表控制：1990年和1992年CPS转型 papers的研究.在键入语言的背景下,EPFL团队的工作扩展了Asai的工作.见2007年论文 here.

这应该是充足的形式主义！我瞥了一眼那些,不幸的是他们需要流利的lambda演算符号.

另一方面,我发现以下使用Shift和Reset tutorial进行编程,感觉我在开始将示例转换为Scala以及何时进入“2.6如何提取分隔的延续”这一部分时,确实有了突破性的理解.

重置操作符分隔程序的一部分. shift用于存在值的位置(可能包括Unit).你可以把它想象成一个洞.让我们用represent代表它.

那么让我们看看以下表达式：

reset { 3 + ? - 1 }                  // (1)
reset {                              // (2)
  val s = if (?) "hello" else "hi"
  s + " world"
}
reset {                              // (3)
  val s = "x" + (?: Int).toString
  s.length
}

将重置内的程序转换为可以访问的函数(此过程称为reification)是什么转移.在上述情况中,功能是：

val f1 = (i: Int) => 3 + i - 1       // (1)
val f2 = (b: Boolean) => {
   val s = if (b) "hello" else "hi"  // (2)
   s + " world"
}
val f3 = (i: Int) => {               // (3)
   val s = "x" + i.toString
   s.length
}

该函数称为continuation,并作为其自身参数的参数提供.转移签名是：

shift[A,B,C](fun: ((A) => B) => C): A

继续将是(A => B)函数,并且在移位内写入代码的人决定用它做什么(或不做).如果你简单地归还它,你真的会感受到它能做些什么.然后重置的结果就是计算本身：

val f1 = reset { 3 + shift{ (k:Int=>Int) => k } - 1 }
val f2 = reset { 
           val s =
             if (shift{(k:Boolean=>String) => k}) "hello"
             else "hi"
           s + " world"
         }
val f3 = reset {
           val s = "x" + (shift{ (k:Int=>Int) => k}).toString
           s.length
         }

我认为具体化方面确实是理解Scala分隔延续的一个重要方面.

从类型的角度来看,如果函数k具有类型(A => B),则移位具有类型A @ cpsParam [B,C]. C型完全取决于您选择在班次内返回的内容.返回使用cpsParam或cps注释的类型的表达式在EPFL论文中被认定为不纯.这与纯表达式相反,后者没有cps注释类型.

不纯的计算转换为Shift [A,C]对象(现在称为标准库中的ControlContext [A,C]). Shift对象正在扩展continuation monad.它们的正式实现在EPFL paper第3.1节第4页中.映射方法将纯计算与Shift对象相结合. flatMap方法将不纯的计算与Shift对象相结合.

continuation插件按照EPLF paper第3.4节中给出的大纲执行代码转换.基本上,shift转换为Shift对象.之后出现的纯表达式与地图结合,不纯的表达式与flatMaps结合使用(参见更多规则图4).最后,一旦所有转换为封闭的重置,如果所有类型检查,所有map和flatMaps之后的最终Shift对象的类型应该是Shift [A,A,C]. reset函数重新生成包含的Shift,并使用identity函数作为参数调用该函数.

总之,我认为EPLF文件确实包含了对所发生情况的正式描述(第3.1和3.4节以及图4).我提到的教程有很好的选择范例,可以很好地理解分隔的延续.