Mat*_*ick 15 haskell functional-programming free-variable pure-function
例如,一个没有自由变量的引用透明函数:
g op x y = x `op` y
现在是一个带有自由(从观点来看f)变量的函数op和x:
x = 1
op = (+)
f y = x `op` y
f也是参考透明的.但它是纯粹的功能吗？
如果它不是纯函数,那么引用透明的函数的名称是什么,但是使用一个或多个绑定在封闭范围内的变量？
这个问题的动机:
从维基百科的文章中我不清楚:
结果值不需要依赖于所有(或任何)参数值.但是,它必须仅依赖于参数值.
(强调我的)
也不是从谷歌搜索纯函数是否可以依赖于free(在一个封闭范围中绑定的意义上,而不是在函数范围内绑定)变量.
另外,这本书说:
如果没有自由变量的函数是纯粹的,那么闭包是不纯的吗？
功能
function (y) { return x }很有趣.它包含一个自由变量x.自由变量是未在函数内绑定的变量.到目前为止,我们只看到了一种"绑定"变量的方法,即通过传入一个具有相同名称的参数.由于该函数function (y) { return x }没有名为x的参数,因此变量x未在此函数中绑定,这使其"自由".现在我们知道函数中使用的变量是绑定的还是空闲的,我们可以将函数分为具有自由变量的函数和不具有以下函数的函数:
- 不包含自由变量的函数称为纯函数.
- 包含一个或多个自由变量的函数称为闭包.
那么"纯函数"的定义是什么？
J. *_*son 17
据我所知,"纯度"是在语义层面定义的,而"引用透明"在语法和嵌入lambda演算替换规则中都具有意义.定义任何一个也会带来一些挑战,因为我们需要有一个强大的程序平等概念,这可能具有挑战性.最后,重要的是要注意自由变量的概念完全是语法 - 一旦你进入一个值域,你就不能再拥有带有自由变量的表达式 - 它们必须被绑定,否则就是语法错误.
但是,让我们深入了解,看看这是否变得更加清晰.
我们可以非常广泛地将引用透明度定义为语法上下文的属性.根据原始定义,这可以用类似的句子构建
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绑定的变量(并考虑"变量"之间的区别,因为它指的是一个"槽",如a 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可能代表非终止.然而,许多人认为这是对纯度的更好定义,因为非终止可以被认为是计算的副作用而不是有意义的结果值.