6

我正在阅读以下 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（+此处的 shift/reset ）我会更幸运，还是嵌套 shift 会有相同类型的限制？我也添加了 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
4

1 回答 1

2

问题是这条线：

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的 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
于 2013-06-21T20:13:49.937 回答