导航页
何谓函数式?
函数式是一种编程范式,这里的函数是数学意义上的。函数式编程的本质就是表达式(expressions)之间的组合。表达式包括值、变量、函数。更具体的说:函数是一类表达式,应用(apply)于特定实参(argument)或输入(input),并且一旦应用,就可以被归约(reduce)或求值(evaluate)。
在 Haskell
中,函数是一等公民(first-class),可以作为值、实参、输入传递。
函数式编程都基于 lambda 演算法(lambda
calculus)。一些函数式编程语言有不能由 lambda 表达的特性。但 Haskell
没有,所以 Haskell
是纯函数式语言。在函数式中,对于纯(purity)更合适的说法是参照透明性(referential
transparency)。亦即,对于同一个函数,给定同样的值,永远会返回同样的结果,正如数学的函数。
何谓函数?
我们先把「lambda」放到一边,转而投向函数。函数人尽皆知,其自身定义并表示了,可能的输入集合和可能的输出集合间的关系。当我们将「加函数」应用于两个输入时,它将两个输入映射为一个输出——亦即它们的和。
例如,有函数 f
定义了以下关系:
f(1)=Af(2)=Bf(3)=C
输入集合为 {1,2,3} 输出集合为
{A,B,C}.
值得注意的是,我们设想的函数 f
总是在输入为 1
时返回 A,没有例外。
更精确的说,输入集合也叫定义域(domain),输出集合也叫陪域(codomain)。所有定义域和陪域都是唯一值的集合。陪域的子集,若包含与不同输入相关的可能输出,则称其为像(image)。定义域和图,或陪域的映射不必是单射的(one-to-one);多个输入在图中映射至单个输出是可能的。
作为对比,下面的关系不是函数:
f(1)=Xf(1)=Yf(2)=Z
回忆一下之前提到的参照透明性:给定相同的输入,输出应是可预测的。这里同一个输入
1 有不同的输出 X 或 Y。
下面的关系同样也是函数:
f(1)=Af(2)=Af(3)=A
这满足参照透明性。不同的输入允许有相同的输出。
上面的例子中,我们没有通过函数定义关系。现又有函数 f:
f(x)=x+1
该函数要求一个实参 x。输入、x、输出的关系由函数体定义。亦即向 x 加 1
并返回结构。当我们将此函数应用于一个具体的值,如 1,我们可以将 x 替换:
f(1)=1+1
亦即:
f(1)=2
Lambda
Lambda 演算法有三大基本构成,或称,项(lambda
terms):表达式(expressions)、变量(variables)、抽象(abstractions)。表达式是以下概念的超集:变量名、抽象、或它们的组合。此处的变量不是具有意义或值,它们只是单纯的,对函数输入的所指。
一个抽象就是一个函数。该 lambda 构成有一个头(head,亦即一个
lambda)、身(body),并且已应用于一个实参。一个实参(argument)就是一个输入值。函数的头是一个跟着变量名的
λ
(lambda)。身则是另一个表达式。所以一个简单的函数长这样:
λx.x
头中具名的变量是形参(parameter),并在函数体中绑定(bind)同一变量的所有实例。这意味着,每个在身中的
x 都将有相同的实参值。
之前,我们讨论了具名函数 f,但
lambda 抽象 λx.x
不具名,亦称匿名函数(anonymous
function)。具名函数可以被其他函数调用,而匿名函数不行。
使用点 . 分隔 lambda
的头和身。
抽象作为整体并没有名字。但我们将其称作「抽象」的原因在于,它是对具体实例的概括或抽象,名称代表了具体的值。但在应用时,实参可以是不同的值,甚至是不同的类型。在我们应用抽象于实参时,我们将名称替换为值,使其具象化。
α
等价
使用 lambda 演算法表达函数时,常常是这样:
λx.x
变量 x
在这里并没有语义作用。因此,在 lambda 项之间存在许多等价形式,称之为
α 等价。对于上面的
lambda,也可以这样表示:
λx.xλd.dλz.z
它们是完全等价的,都在表达同样的函数。
β 归约
当我们将一个函数作用于一个实参,我们将抽象中所有绑定变量的实例,替换为输入的表达式。这还消除了抽象的头部,因为头的目的就是为了绑定一个变量。该过程称为
β 归约。
仍然使用之前定义过的函数:
λx.x
不妨使用一个数字作为示例。我们将该函数应用于实参 2:
(λx.x) 22
唯一的约束变量是 x,即这是一个恒等式(identity
function),因此将该函数应用于 2
则返回 2.
我们也可以归约更复杂的函数:
(λx.x+1)
别忘了,函数也可以作为实参:
(λx.x)(λy.y)
在这个例子中,我们可将 x
替换为整个抽象。这样归约这个应用:
(λx.x)(λy.y)[x:=(λy.y)]λy.y
上面类似 [x:=z]
的这种语法表示,z 将替换所有出现的
x。结果是一个新的恒等式。我们没有更多实参,因此也不能再归约。
再看看更复杂的例子:
(λx.x)(λy.y)z 对于 lambda 的应用是左结合的(left
associative)。这意味着除非有明确的括号,它们向左分组: ((λx.x)(λy.y))z
归约:
((λx.x)(λy.y))z[x:=(λy.y)](λy.y)z[y:=z]z
自由变量
函数可能有多个头以及自由变量(free
variables,即身中没有被头绑定的变量),在下面的表达式中:
λx.xy
身中的 x
是绑定变量,因为在头中具名。但 y
是一个自由变量,因为未在头中出现。当我们应用该函数于一个实参时。y 是不可归约的。
不妨将其应用于 z 并归约:
(λx.xy)z(λ[x:=z].xy)zy
请注意,自由变量并不是 α
等价的。例如,λx.xz 和 λx.xy 并不等价,因为 z 或 y 可能并不相同。
多实参
每一个 lambda
只能有一个形参并接受一个实参。需要多个实参的函数具有多个嵌套的头。当你应用了一次函数,你就消除了第一个,亦即最左的头。这种表达最初由
Moses Schönfinkel 发现,但以 Haskell Curry 命名为
curry,亦即柯里化。
也就是对于下面的形式:
λxy.xy
可以转化为:
λx.(λy.xy)
不妨看看具体的例子:
λxy.xyλx.(λy.xy)λx.(λy.xy) 1 2[x:=1](λy.1y) 2[y:=2]1 2
以及,实参为函数的例子:
λxy.xy(λxy.xy)(λz.z) 1(λx(λy.xy))(λz.a) 1[x:=(λz.a)](λy.(λz.a)y) 1[y:=1](λz.a) 1
此处,我们仍可以继续归约,但 z
虽然在头中,身中却没有实例,所以我们仅能保留自由变量:
(λz.a) 1[z:=1]a
由于 α
等价,还能常常看到这样的表达:
(λxy.xxy)(λx.xy)(λx.xz)
由于很多形似,但实质上不同的 x
互相纠缠,在归约时可能遇到麻烦。因此,这里用一个更加清晰的例子:
(λxyz.xz(yz))(λmn.m)(λp.p)(λx.λy.λz.xz(yz))(λm.λn.m)(λp.p)
上面的步骤中,我们没有应用任何实参,仅柯里化了该表达式。接下来,我们应用实参:
(λx.λy.λz.xz(yz))(λm.λn.m)(λp.p)(λy.λz.(λm.λn.m)z(yz))(λp.p)λz.(λm.λn.m)(z)((λp.p)z)λz.(λn.z)((λp.p)z)λz.z
最后一步可能看起来有点奇怪,λn.z 接受一个参数并无条件返回 z,所以参数 ((λ.p.p)z) 会直接消失。最后归约为
λz.z.
求值即简化
Lambda 表达式有多种标准形式,但在这里,我们指 β 标准形式,亦即,该表达式不能再
β
归约。亦即,一个被完全求值的表达式,或是在编程中,一个完全执行完了的程序。
举个例子,10002000
的标准形式是 2。关键在于,如果你有一个函数,例如 /,是饱合的(所有实参都已应用),但若还没有简化(simplify)为最终结果;那么,该函数是未完全求值的,只是应用了。应用才使求值或简化可行。
类似的,下列表达式的正常形式是 600:
(10+2)×100÷2
恒等式 λx.x
是完全归约的,因为它未被应用。然而,(λx.x)z 并非 β
标准形式,因为恒等式已有实参(此处为自由变量 z)但未被应用。若对其归约,最终结果,亦即
β 标准形式,将会是 z.
组合子
一个组合子(combinator)是一个没有自由变量的 lambda
项。就如名字暗示的,组合子仅用于组合被给予的函数。
所以,下列 lambda 是组合子,因为每个项都出现在了头中:
λx.xλxy.xλxyz.xz(yz)
下列 lambda 不是组合子,因为至少有一个自由变量:
λy.xλx.xz
发散度
并非所有可归约的 lambda 项都可以整齐的归约为 β 标准形式。因为 lambda
可能出现发散(diverge)。这里的发散通常意味着归约过程还未终止或结束。通常情况下,归约项应当收敛(converge)到
β
标准形式。发散是收敛以及标准形式的反面。这里有一个 lambda 项::
(λx.xx)(λx.xx)([x:=(λx.xx)].xx)(λx.xx)(λx.xx)
当我们尝试归约,lambda
项却回到最开始的形式,并且永不停止,我们就可以说这是 ω 发散。
这在编程中很重要,因为发散意味着不会产生答案或有意义的项。
结
以上,就是 lambda 演算法的主要内容,也是 Haskell 的基石。
值得注意的是,Haskell 中的 lambda
是类型化的(typed),此处介绍的只是无类型
lambda。不过其核心仍然一样。