Scala continuation插件是否支持嵌套移位？

Question

我将通过以下Shift/Reset教程:http://www.is.ocha.ac.jp/~asai/cw2011tutorial/main-e.pdf.

到目前为止,我将OchaCaml示例转换为Scala(一直到2.11节)都取得了不错的成绩.但现在我似乎已经碰壁了.来自Asai/Kiselyov的论文中的代码定义了以下递归函数(这是OchaCaml - 我认为):

(* a_normal : term_t => term_t *)
let rec a_normal term = match term with
    Var (x) -> Var (x)
  | Lam (x, t) -> Lam (x, reset (fun () -> a_normal t))
  | App (t1, t2) ->
      shift (fun k ->
        let t = gensym () in (* generate fresh variable *)
        App (Lam (t, (* let expression *)
                  k (Var (t))), (* continue with new variable *)
             App (a_normal t1, a_normal t2))) ;;

该函数应该对一个lambda表达式进行A规范化.这是我的Scala翻译:

// section 2.11
object ShiftReset extends App {

  sealed trait Term
  case class Var(x: String) extends Term
  case class Lam(x: String, t: Term) extends Term
  case class App(t1: Term, t2: Term) extends Term

  val gensym = {
    var i = 0
    () => { i += 1; "t" + i }
  }

  def a_normal(t: Term): Term@cps[Term] = t match {
    case Var(x) => Var(x)
    case Lam(x, t) => Lam(x, reset(a_normal(t)))
    case App(t1, t2) => shift{ (k:Term=>Term) =>
      val t = gensym()
      val u = Lam(t, k(Var(t)))
      val v = App(a_normal(t1), a_normal(t2))
      App(u, v): Term
    }
  }

}

我收到以下编译错误:

 found   : ShiftReset.Term @scala.util.continuations.cpsSynth 
             @scala.util.continuations.cpsParam[ShiftReset.Term,ShiftReset.Term]
 required: ShiftReset.Term
    case App(t1, t2) => shift{ (k:Term=>Term) =>
                                              ^
one error found

我认为插件告诉我它不能处理嵌套shift...有没有办法让代码编译(或者我忽略了一个基本错误或者一些解决方法)？我试图将模式匹配转换为if/else if/else并引入更多局部变量,但我得到了相同的错误.

或者,我是否会更幸运地使用Haskell和Cont monad(+从此处移位/重置)或者是否存在与嵌套移位相同类型的限制？我也添加了Haskell标记,因为我不介意切换到Haskell来完成本教程的其余部分.

编辑:感谢詹姆斯想出延续插件无法处理哪一行以及如何调整它,现在它可以工作了.使用他的答案中的版本和以下格式代码:

def format(t: Term): String = t match {
  case Var(x) => s"$x"
  case Lam(x, t) => s"\\$x.${format(t)}"
  case App(Lam(x, t1), t2) => s"let $x = ${format(t2)} in ${format(t1)}"
  case App(Var(x), Var(y)) => s"$x$y"
  case App(Var(x), t2) => s"$x (${format(t2)})"
  case App(t1, t2) => s"(${format(t1)}) (${format(t2)})"
}

我得到了论文提到的输出(虽然我还没有掌握延续实际如何管理它):

sCombinator:
\x.\y.\z.(xz) (yz)
reset{a_normal(sCombinator)}:
\x.\y.\z.let t1 = xz in let t2 = yz in let t3 = t1t2 in t3

Answer 1

问题是这一行：

val v = App(a_normal(t1), a_normal(t2))

我不确定，但我认为类型推断器对a_normal返回 a 的事实感到困惑Term@cps[Term]，但我们在 a 内部，shift所以延续没有以相同的方式注释。

如果您将该行从块中拉出，它将编译shift：

def a_normal(t: Term): Term@cps[Term] = t match {
  case Var(x) => Var(x)
  case Lam(x, t) => Lam(x, reset(a_normal(t)))
  case App(t1, t2) =>
    val v = App(a_normal(t1), a_normal(t2))
    shift{ (k:Term=>Term) =>
      val t = gensym()
      val u = Lam(t, k(Var(t)))
      App(u, v): Term
    }
}

一般来说，对于嵌套shift，如果每个嵌套延续都有兼容的类型，那么您绝对可以这样做：

object NestedShifts extends App {

  import scala.util.continuations._

  def foo(x: Int): Int@cps[Unit] = shift { k: (Int => Unit) =>   
    k(x)
  }

  reset {
    val x = foo(1)
    println("x: " + x)

    val y = foo(2)
    println("y: " + y)

    val z = foo(foo(3))
    println("z: " + z)
  }
}

该程序打印到标准输出：

x: 1
y: 2
z: 3