据我所知,“纯度”是在语义级别定义的,而“引用透明”可以在语法上和嵌入 lambda 演算替换规则中具有意义。定义其中任何一个也会带来一些挑战,因为我们需要有一个强有力的程序平等概念,这可能具有挑战性。最后,重要的是要注意自由变量的概念是完全语法的——一旦你进入一个值域,你就不能再有自由变量的表达式——它们必须被绑定,否则这是一个语法错误。
但是让我们深入研究一下,看看这是否会变得更清楚。
Quinian 参考透明度
我们可以将引用透明性非常广泛地定义为句法上下文的属性。根据原始定义,这将由类似的句子构建而成
New York is an American city.
我们已经戳了一个洞
_ is an American city.
如果给定两个都“指代”同一事物的句子片段,用这两个句子中的任何一个填充上下文不会改变其含义,则可以说这样一个空洞的句子,一个“上下文”是指称透明的。
需要明确的是,我们可以选择具有相同引用的两个片段是“纽约”和“大苹果”。注入我们编写的那些片段
New York is an American city.
The Big Apple is an American city.
建议
_ is an American city.
是参照透明的。为了演示典型的反例,我们可以写
"The Big Apple" is an apple-themed epithet referring to New York.
并考虑上下文
"_" is an apple-themed epithet referring to New York.
现在当我们注入两个引用相同的短语时,我们得到一个有效和一个无效的句子
"The Big Apple" is an apple-themed epithet referring to New York.
"New York" is an apple-themed epithet referring to New York.
换句话说,引用打破了引用的透明度。我们可以通过使句子引用一个句法结构而不是纯粹指该结构的含义来了解这是如何发生的。这个概念稍后会回来。
语法与语义
有一些令人困惑的地方在于,上面对参照透明性的定义直接适用于我们通过字面剥离单词来构建上下文的英语句子。虽然我们可以在编程语言中做到这一点,并考虑这样的上下文是否在引用上是透明的,但我们也可能认识到这种“替代”的想法对于计算机语言的概念至关重要。
所以,让我们明确一点:在 lambda 演算中我们可以考虑两种引用透明性——句法一种和语义一种。语法要求我们将“上下文”定义为用编程语言编写的文字中的孔。这让我们考虑像这样的孔
let x = 3 in _
并用“x”之类的东西填充它。我们稍后会对该替代品进行分析。在语义层面,我们使用 lambda 术语来表示上下文
\x -> x + 3 -- similar to the context "_ + 3"
并且仅限于填充漏洞而不是使用语法片段,而是仅使用有效的语义值,即由应用程序执行的操作
(\x -> x + 3) 5
==>
5 + 3
==>
8
因此,当有人提到 Haskell 中的引用透明性时,重要的是要弄清楚他们指的是哪种引用透明性。
这个问题指的是哪一种?因为它是关于包含自由变量的表达式的概念,所以我将建议它是句法的。我的推理有两个主要推力。首先,为了将语法转换为语义,需要语法有效。在 Haskell 的情况下,这意味着语法有效性和成功的类型检查。但是,我们会注意到像这样的程序片段
x + 3
实际上是一个语法错误,因为x
它是未知的,未绑定的,因此我们无法将其语义视为 Haskell 程序。其次,变量的概念,例如可以let
绑定的变量(并考虑“变量”之间的区别,因为它指的是诸如 an 之类的“槽” IORef
)完全是一种句法结构——甚至没有办法谈论它们来自 Haskell 程序的语义内部。
因此,让我们将问题细化为:
包含自由变量的表达式可以(在语法上)引用透明吗?
无趣的是,答案是否定的。引用透明度是“上下文”的属性,而不是表达式。因此,让我们来探讨一下上下文中的自由变量的概念。
自由变量上下文
上下文如何有意义地具有自由变量?它可能在洞的旁边
E1 ... x ... _ ... E2
只要我们不能在那个“超出”并影响x
语法的语法漏洞中插入一些东西,那么我们就可以了。因此,例如,如果我们用类似的东西填充那个洞
E1 ... x ... let x = 3 in E ... E2
那么我们还没有“捕获” x
,因此也许可以认为该句法漏洞是引用透明的。但是,我们对我们的语法很好。让我们考虑一个更危险的例子
do x <- foo
let x = 3
_
return x
现在我们看到我们提供的洞在某种意义上控制了后面的短语“ return x
”。事实上,如果我们注入一个像“ let x = 4
”这样的片段,那么它确实改变了整体的含义。从这个意义上说,这里的语法不是引用透明的。
引用透明度和自由变量之间的另一个有趣的交互是分配上下文的概念,例如
let x = 3 in _
其中,从外部的角度来看,“ x
”和“ y
”这两个短语都引用同一个东西,一些命名变量,但是
let x = 3 in x ==/== let x = 3 in y
围绕平等和背景从棘手的进展
现在,希望上一节解释了在各种句法上下文下打破引用透明度的几种方法。关于哪些类型的上下文是有效的以及哪些类型的表达式是等价的,值得提出更难的问题。例如,我们可能会do
在前面的示例中对我们的符号进行去糖化,并最终注意到我们不是在使用真正的上下文,而是在某种高阶上下文中工作
foo >>= \x -> (let x = 3 in ____(return x)_____)
这是一个有效的上下文概念吗?这在很大程度上取决于我们赋予程序什么样的意义。对语法进行脱糖的概念已经暗示语法必须定义得足够好以允许这种脱糖。
作为一般规则,我们必须非常小心地定义平等的上下文和概念。此外,我们要求语言片段具有的意义越多,它们可以平等的方式就越多,我们可以构建的有效上下文就越少。
最终,这将我们一路带到我之前所说的“语义参照透明性”,在这种情况下,我们只能将正确的值替换为正确的、封闭的 lambda 表达式,并且我们将由此产生的相等性视为“作为程序的相等性”。
这最终意味着,随着我们在语言中赋予越来越多的意义,随着我们开始接受越来越少的事物是有效的,我们对引用透明度的保证越来越强。
纯度
所以这最终导致了纯函数的概念。我在这里的理解(甚至)不太完整,但值得注意的是,在我们转移到一个非常丰富的语义空间之前,纯度作为一个概念并不存在——Haskell 语义作为一个超过提升的完整偏序的类别。
如果这没有多大意义,那么想象一下纯度是一个仅在将 Haskell 值作为函数和程序平等讨论时才存在的概念。特别是,我们检查了 Haskell 函数的集合
trivial :: a -> ()
trivial x = x `seq` ()
trivial
在这里,我们对 的每个选择都有一个函数a
。我们将使用下划线标注具体选择
trivial_Int :: Int -> ()
trivial_Int x = x `seq` ()
现在我们可以将(非常严格的)纯函数定义为这样的f :: a -> b
函数
trivial_b . f = trivial_a
换句话说,如果我们把计算函数的结果扔掉b
,那么我们可能一开始就没有计算过它。
同样,如果表达式包含自由变量(因为这是语法错误),没有 Haskell 值就没有纯度的概念,也没有 Haskell 值的概念。
那么答案是什么?
归根结底,答案是你不能谈论自由变量的纯洁性,而且每当你谈论语法时,你都可以通过多种方式破坏引用透明性。在某些时候,当您将句法表示转换为其语义表示时,您必须忘记自由变量的概念和名称,以便让它们表示 lambda 项的约简语义,此时我们已经开始具有引用透明性。
最后,纯度比引用透明度更严格,甚至与您的(引用透明的)lambda 项的缩减特性有关。
根据上面给出的纯度定义,大多数 Haskell 本身并不是纯粹的,因为 Haskell 可能代表不终止。然而,许多人认为这是对纯度的更好定义,因为不终止可以被认为是计算的副作用,而不是有意义的结果值。