scala - Scala 延续插件是否支持嵌套移位？

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(+ 来自 here 的移位/重置)我会更幸运，还是嵌套移位会有相同类型的限制？我也添加了 Haskell 标签，因为我不介意切换到 Haskell 来完成本教程的其余部分。

编辑:感谢 James 发现 continuation 插件无法处理哪一行以及如何调整它，它现在可以工作了。使用他的答案中的版本和以下格式代码:

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 的事实感到困惑。返回 Term@cps[Term] ，但我们在 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 s 一般来说，如果每个嵌套的延续都具有兼容的类型，您绝对可以这样做:

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