9

最近我读了很多关于Haskell的文章，以及它从纯粹的函数式语言中获得的好处。（我对讨论 Lisp 的 monad 不感兴趣）对我来说（至少在逻辑上）尽可能地隔离具有副作用的函数是有意义的。我已经setf大量使用了其他破坏性函数，并且我认识到在 Lisp 和（大部分）其衍生产品中对它们的需求。

开始了：

  1. 类似的东西(declare pure)可能有助于优化编译器吗？或者这是一个有争议的问题，因为它已经知道了？
  2. 该声明是否有助于证明一个函数或程序，或者至少是一个被声明为纯的子集？还是这又是不必要的，因为它对程序员、编译器和证明者来说已经很明显了？
  3. 如果没有别的，编译器对程序员使用此声明强制执行纯函数并增加 Lisp 程序的可读性/可维护性是否有用？
  4. 这有什么意义吗？还是我太累了，现在连想都不想？

我很感激这里的任何见解。欢迎提供有关编译器实现或可证明性的信息。

编辑

澄清一下，我并不打算将这个问题限制在 Common Lisp 上。它显然（我认为）不适用于某些衍生语言，但我也很好奇其他 Lisps 的某些功能是否倾向于支持（或不支持）这种设施。

4

3 回答 3

7

你有两个答案，但都没有触及真正的问题。

首先，是的，知道函数是纯函数显然是件好事。有很多编译器级别的东西想知道，还有用户级别的东西。鉴于 lisp 语言非常灵活，您可以稍微扭曲一下：与其要求编译器更努力地尝试的“纯”声明，不如让声明限制定义中的代码。这样你就可以保证函数是纯的。

您甚至可以使用额外的支持工具来做到这一点——我在对 johanbev 的回答所做的评论中提到了其中的两个：添加不可变绑定和不可变数据结构的概念。我知道在Common Lisp 中这些都是非常有问题的，尤其是不可变绑定（因为 CL 通过“副作用”将代码加载到位）。但是这些特性将有助于简化事情，而且它们并非不可想象（参见例如具有不可变对和其他数据结构的Racket实现，并具有不可变绑定。

但真正的问题是你能在这些受限的功能中做什么。即使是一个看起来很简单的问题也会充满问题。（我为此使用了类似于 Scheme 的语法。）

(define-pure (foo x)
  (cons (+ x 1) (bar)))

似乎很容易看出这个函数确实是纯粹的，它什么也没做。此外，似乎define-pure限制正文并只允许纯代码在这种情况下可以正常工作，并且将允许此定义。

现在从问题开始：

  1. 它正在调用cons，因此它假设它也被认为是纯的。另外，正如我上面提到的，它应该依赖于cons它是什么，所以假设cons绑定是不可变的。很简单，因为它是一个已知的内置函数。当然，对做同样的事情bar。

  2. 但cons 确实有一个副作用（即使你在谈论 Racket 的不可变对）：它分配了一个新的对。这似乎是一个次要且可忽略的点，但是，例如，如果您允许此类内容出现在纯函数中，那么您将无法自动记忆它们。问题在于，有人可能会依赖每次foo调用都会返回一个新的对——一个不是——eq给任何其他现有的对。似乎为了让它变得更好，您需要进一步限制纯函数不仅可以处理不可变值，还可以处理构造函数并不总是创建新值的值（例如，它可以散列而不是分配）。

  3. 但是该代码也调用bar- 所以你不需要对 做同样的假设bar：它必须被称为纯函数，具有不可变的绑定。请特别注意，它bar不接收任何参数——因此在这种情况下，编译器不仅可以要求它bar是一个纯函数，它还可以使用该信息并预先计算其值。毕竟，没有输入的纯函数可以简化为普通值。（注意顺便说一句，Haskell 没有零参数函数。）

  4. 这带来了另一个大问题。如果bar是一个输入的函数怎么办？在这种情况下，您会遇到错误，并且会抛出一些异常......这不再是纯粹的。例外是副作用。您现在需要知道bar除其他所有内容之外的 arity，并且您需要避免其他异常。现在，那个输入怎么x样 - 如果它不是一个数字会发生什么？这也会引发异常，因此您也需要避免它。这意味着您现在需要一个类型系统。

  5. 将其更改(+ x 1)为(/ 1 x)，您会发现您不仅需要一个类型系统，还需要一个足够复杂以区分 0 的类型系统。

  6. 或者，您可以重新考虑整个事情，并拥有永远不会抛出异常的新的纯算术运算 - 但由于所有其他限制，您现在离家还有很长的路要走，使用一种完全不同的语言。

  7. 最后，还有一个副作用仍然是 PITA：如果定义baris(define-pure (bar) (bar))怎么办？根据上述所有限制，它当然是纯粹的……但发散是一种副作用，所以即使这样也不再是犹太教。（例如，如果你确实让你的编译器将空函数优化为值，那么对于这个例子，编译器本身就会陷入无限循环。）（是的，Haskell 没有处理这个问题，它没有做到这一点问题不大。）

于 2011-08-31T16:33:53.140 回答
3

给定一个 Lisp 函数，通常无法确定它是否是纯函数。当然，必要条件和充分条件可以在编译时进行测试。（如果根本没有不纯的操作，那么函数一定是纯的；如果一个不纯的操作被无条件执行，那么这个函数一定是不纯的；对于更复杂的情况，编译器可以尝试证明这个函数是纯的还是不纯的，但它不会在所有情况下都成功。）

  1. 如果用户可以手动将函数注释为纯函数，那么编译器可以（a.）更努力地证明该函数是纯函数，即。在放弃之前花更多时间，或者（b.）假设它是并添加对于不纯函数不正确的优化（例如，记忆结果）。所以，是的，如果假设注释是正确的，那么将函数注释为纯函数可以帮助编译器。

  2. 除了像上面“更努力”的想法这样的启发式方法之外，注释无助于证明东西，因为它没有向证明者提供任何信息。（换句话说，证明者可以在尝试之前假设注释始终存在。）但是，将纯函数的证明附加到纯函数上可能是有意义的。

  3. 编译器可以（a.）在编译时检查纯函数是否确实是纯函数，但这通常是不确定的，或者（b.）添加代码以尝试在运行时捕获纯函数中的副作用并将其报告为错误. (a.) 可能对简单的启发式方法有帮助（比如“一个不纯的操作被无条件地执行），(b.) 对调试很有用。

  4. 不，这似乎是有道理的。希望这个答案也可以。

于 2011-08-31T10:55:55.953 回答
1

当我们可以假设纯度和参考透明度时，通常的好处就适用。我们可以自动记忆热点。我们可以自动并行计算。我们可以处理很多竞争条件。我们还可以对我们知道不能修改的数据使用结构共享，例如（准）原语“cons()”不需要复制它所连接到的列表中的 cons-cells。这些单元格不会受到另一个指向它的 cons-cell 的影响。这个例子有点明显，但编译器在解决更复杂的结构共享方面通常表现出色。

然而，在 Common Lisp 中，实际确定一个 lambda（一个函数）是纯的还是具有引用透明性是非常棘手的。请记住，函数调用 (foo bar) 从查看 (symbol-function foo) 开始。所以在这种情况下

(defun foo (bar)
  (cons 'zot bar))

foo() 是纯粹的。

下一个 lambda 也是纯的。

(defun quux ()
 (mapcar #'foo '(zong ding flop)))

但是，稍后我们可以重新定义 foo：

(let ((accu -1))
 (defun foo (bar)
   (incf accu)))

对 quux() 的下一次调用不再是纯粹的！旧的纯 foo() 已被重新定义为不纯的 lambda。哎呀。这个例子可能有点做作，但在词法上重新定义一些函数并不少见，例如使用 let 块。在这种情况下，不可能知道编译时会发生什么。

Common Lisp 具有非常动态的语义，因此实际上能够提前确定控制流和数据流（例如在编译时）非常困难，并且在大多数有用的情况下完全无法确定。这是具有动态类型系统的语言的典型特征。如果您必须使用静态类型，那么 Lisp 中有很多常见的习惯用法是您无法使用的。主要是这些破坏了任何进行有意义的静态分析的尝试。我们可以为像 cons 和 friends 这样的原语做到这一点。但是对于涉及除原语之外的其他事物的 lambda，我们处于更深的水中，尤其是在我们需要查看函数之间复杂的相互作用的情况下。请记住，只有当它调用的所有 lambda 都是纯的时，它才是纯的。

在我的脑海中，有可能通过一些深刻的宏观学来消除重新定义的问题。从某种意义上说，每个 lambda 都有一个额外的参数，它是一个代表 lisp 图像的整个状态的 monad（我们显然可以将自己限制在函数实际查看的内容上）。但是，能够自己声明纯度可能更有用，因为我们向编译器保证这个 lambda 确实是纯净的。如果不是这样，后果是不确定的，并且可能会发生各种混乱......

于 2011-08-31T11:30:40.150 回答