声明 Lisp 函数“纯”的能力是否会成为现实？有好处吗？

Question

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

我们开始吧：

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

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

编辑

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

Answer 1

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

首先，是的，知道函数是纯函数显然是件好事。有大量编译器级别的事情以及用户级别的事情想要知道。鉴于 Lisp 语言非常灵活，您可以稍微扭转一下情况：您只需将声明限制定义中的代码，而不是要求编译器更加努力的“纯粹”声明。这样你就可以保证函数是纯粹的。

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

但真正的问题是，即使是一个看起来非常简单的问题也会出现问题（我为此使用了类似方案的语法。）

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

似乎很容易分辨。这个函数确实是pure，它不会做任何事情。此外，似乎使用 define-pure 限制主体并仅允许纯代码在这种情况下可以正常工作，并且将允许此定义

现在从问题开始 。 ：

1. 它正在调用 cons，因此它假定它也是纯的。此外，正如我上面提到的，它应该依赖于 cons 。是，所以假设 cons 绑定是简单，因为它是一个已知的内置函数，当然，对 bar 执行相同的操作。

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

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

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

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

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

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

Answer 2

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

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

2. 除了上面的“更加努力”的想法之外，注释对证明东西没有帮助，因为它没有向证明者提供任何信息。 ，证明者可以在尝试之前假设注释始终存在。）但是，向纯函数附加其纯度的证明可能是有意义的。

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

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

Answer 3

当我们可以假设纯度和参考性时，通常的好处就适用
透明度。我们可以自动记住热点。我们可以
自动并行计算。我们可以处理很多事情
比赛条件。我们还可以使用与我们的数据共享结构
知道不能被修改，例如（准）原始“cons()”
不需要复制它正在使用的列表中的 cons-cells。
这些细胞不会受到另一个 cons-cell 的影响
指着它。这个例子有点明显，但是编译器经常
在解决更复杂的结构共享方面表现良好。

然而，实际确定 lambda（函数）是否是纯函数或具有
在 Common Lisp 中，引用透明性非常棘手。请记住
funcall (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 中有很多常见的习语你不能使用
如果您必须使用静态类型。犯规的主要是这些
尝试做很多有意义的静态分析。我们可以为基元做到这一点
就像缺点和朋友一样。但对于涉及其他事情的 lambda 来说
原始我们处于更深的水中，特别是在以下情况下
我们需要考虑功能之间复杂的相互作用。请记住
仅当 lambda 调用的所有 lambda 都是纯的时，它才是纯的。

在我的脑海里，有可能，通过一些深入的宏观学，
消除重新定义问题。从某种意义上说，每个 lambda 得到
一个额外的参数，它是一个代表整个状态的 monad
lisp 图像（我们显然可以限制自己的功能
实际会看）。但这可能更有用
我们自己声明纯度，即我们向编译器承诺
这个 lambda 确实是纯的。如果不这样做的话后果就是
未定义，并且可能会发生各种混乱......