11

我正在阅读实现函数式语言：教程，并在实现完全惰性 lambda 提升的浮动传递时遇到问题。

我想描述一下浮动是如何使这个问题变得清晰的，如果您熟悉它，请直接跳到下面的问题。

该概念在论文第 246 页介绍，主要在第 256-257 页实现。

在let(rec)表达的情况下，它说：

我们必须将右侧的浮动定义放在let(rec)表达式本身之前，因为右侧可能取决于它们。

例如：

\a ->
  let f = \b -> b + (let $mfe = a * a in $mfe)
  in f

该变量$mfe是一个最大自由表达式（MFE），由前一遍识别，在处理let f表达式时，我们f作为一组浮出并附加到[(1, [($mfe, a * a)])]，这是从 的右侧获得的let f。这里，第一个分量1表示该组的空闲级别。

当回溯到\a -> f抽象时，我们发现$mfe和f都受其约束，因此我们应该在这里安装它们：

\a ->
  let $mfe = a * a
  in
    let f = \b -> b + $mfe
    in f

问题

假设我们有一个这样的程序：

f = \x -> \y ->
  letrec
    a = \p -> cons p (b x)
    b = \q -> cons q (a y)
  in pair (a 1) (b 2)

和的免费级别将是 2，因为有级别 2 并且它们在同一组中。b xa yy

虽然and的免费级别为3，因此and将被标记为 MFE（我在这里犯错了吗？）。cons p (b x)cons q (a y)b xa y

使用 SPJ 给出的算法，程序将转化为：

f = \x -> \y ->
  let $ay = a y -- `a` is not defined yet!
  in
    let $bx = b x -- and `b`
    in
      letrec
        a = \p -> cons p $bx
        b = \q -> cons q $ay
      in pair (a 1) (b 2)

我认为表达式右侧的 MFE 在引用左侧时let(rec)不应逃脱范围，正确的结果可能如下所示：let(rec)

f = \x -> \y ->
  letrec
    $ay = a y
    $bx = b x
    a = \p -> cons p $bx
    b = \q -> cons q $ay
  in pair (a 1) (b 2)

纸错了吗？或者我只是误解了它。

4

0 回答 0