问题标签 [referential-transparency]

什么是局部推理？它与参照透明性、等式推理和懒惰有什么关系？

作为对此的后续，我意识到我需要使用异质组合来为部分盒子制作盖子。在这里，我删除了所有不必要的杂物：

所以这里唯一剩下的漏洞是在 的定义中p。当然，我想用 来填充它p-faces i，因为这就是我定义它的原因。但是，这会导致 Universe 级别的错误：

检查表达式p-faces i是否具有类型时

但是，如果我内联p-facesinto的定义p，它会进行类型检查；请注意，这还包括类型检查p-faces（我不需要删除它）的定义，它只是导致这种类型错误的用法：p-faces

p-faces在 的定义中使用 有什么问题p？在我未经训练的眼睛看来，它看起来像是一个永远不会超过的正常定义Type₀

我是函数式编程和 Scala 的新手，我正在查看 Cats Effect 框架并试图了解 IO monad 的作用。到目前为止，我所理解的是，在 IO 块中编写代码只是对需要完成的操作的描述，并且在您使用unsafe提供的方法显式运行之前什么都不会发生，并且也是一种制作参考执行副作用的代码的方法实际上不运行它是透明的。

我尝试执行下面的代码片段只是为了理解它的含义：

输出是：

我不明白为什么赋值state = newState不运行，但增量和赋值表达式out += 1运行。我是否遗漏了一些关于这应该如何工作的明显内容？我真的可以使用一些帮助。我知道我可以使用这些unsafe方法来运行它。

在我读到的文档页面上boost::hana::always

always(x)是一个函数，使得

对于任何y....

这让我认为它的行为不应该与这个 lambda: 有任何不同[](auto const&...){ return false; }。

然而确实如此。例如，下面的代码打印11，但是如果我将第三个 lambda 更改为hana::always(false)，那么它会打印00，这表明它always正在吞噬任何参数。

• 这是预期的吗？
• 如果是这样，为什么？
• 无论是否预期，是什么导致了这种行为？

顺便说一句，我刚刚发现boost::hana::overload_linearly，这不是boost::hana::overload这种情况下的替代方案（因为always不会得到所有的电话，这将[](int){ return true; }是贪婪的），但很高兴知道它。

我有这个代码

正如您在我的 The Little MLersxOccurs所说的那样，我在其中有两个帮助函数，let它们是“相互引用的” ：和. 所以在 SML 中，你必须使用关键字让他们相互了解并相互“交叉引用”。顺便说一句，计算 s 列表中特定对象的数量，在我的示例中，原子是变量。slOCseOCandsxOccursAnAtomFruit

我的问题是，这是参考透明度的一个例子吗？同样，在戴维他举了这个例子

注意到 Imperative-land 中的堆栈不断地改变堆栈，而 Haskell 正在si为每个堆栈操作创建一个新变量。然后他说，这些行中的每一行都可以被打乱成不同的顺序，结果不会改变。AFAICT 这与我的基本思想相同，因为sxOccurs它不在乎我呈现子功能的顺序。那么，这又是指代透明性的更深层含义吗？如果不是，我在这里展示的是什么？

我想我知道什么是参照透明和纯粹的意思。然而，这里有一个关于这两个属性以及它们有何不同的问题。

至于如何在语言中执行引用透明度和/或纯度，我不太了解。（即使这也不能帮助我理解。）我的意思是，我可能知道（某种程度）Haskell 是如何处理 IO 的，尽管它是纯函数式的（见这个），而且我知道我不能编写不纯的函数，因为类型系统只是不让我（或者，更好的是，它确实让我以一种受控的方式，因为我必须unsafe明确地写出来）。

但是在 C++ 中，就像在许多其他语言中一样，函数通常不是纯的，也不是引用透明的。

所以一方面我有 Haskell，它被构造为一种纯语言，其中每个函数都是纯的。另一方面，我有 C++，它无法强制执行纯度（或者是吗？¹）。²

但是，在未来，C++ 语言是否有可能提供pure一个可以附加到函数的 /whatever 属性，以便编译器必须验证该函数确实是纯的（否则编译时会失败）？

[[gnu:pure]](¹) 当我第一次知道and[[gnu:const]]时，我的脑海中突然出现了这个问题。我的理解是，那些（不可移植的）属性是为了给编译器更多的保证，以便它可以优化更多的东西，而不是告诉它检查函数是否真的是纯的。毕竟这个例子似乎编译和运行得很好。

(²) 但我还记得另一种非常古老的语言，它不像 Haskell 那样纯，但给你一个PURE属性来告诉你一个函数必须是纯的，编译器检查了它：Fortran。