丧钟为谁鸣?

函数式也不一定就无副作用阿。ml就有副作用，scheme的continuation如果没有副作用能力会差很多。觉得无副作用和引用透明主要是便于证明程序的等价和正确性。当然也有程序风格的问题。
但是lamda的表达能力并不因为存在副作用而减弱。


计算理论就太高深了。俺乡下人不懂。不过elm貌似不太厚道。

说我不厚道，是不是因为我前文的第一段话？:P:P

其实这里倒是没有不厚道的意思，我的确很想知道 Alan Kay 是否认同这个观点。因为如果是的话，我对函数式语言的理解就要翻个个了。在我的理解里面，函数式语言它的本质特点之一就是没有状态，你看见 (define x 3)，你就知道 x 和 3 是一回事，可以在任意出现 x 的地方替换成 3 。而就我所知道的 lambda 演算，也是支持这种理解的。因此，我是真的不知道该怎样理解“带有副作用的lambda抽象”。如果 ajoo 你觉得副作用和 lambda 演算可以并行不悖的话，来给我说说？

对于λ Calculus中丘奇定义了有三个基本运算：α变换，β规约和η规约。引用透明性是由η规约指定的。同时只注意的还有的α变换和β规约。我们可以看一下面这个例子：

(define f
   (let ((x 3))
      (+ x 4))

这个例子中我们可以说f代表的是:
(λx. x + 4)3

我们把这可以把这个东西看作一个λ计算式，根据β规约，我们把x+4里的x替换成3，于是得到7，这是一个简单的例子。但是通过这个简单的例子我们可以看出来，在函数式语言中，我定义一个符号，更多的情况下是一个λ抽象和对于λ抽象的计算。对于Elminster兄举的(define x 3)这个例子实际是符号定义的最简单形式而已。
我们看一个复杂一些例子，来证明我的观点：

(define f (cons 1 2))
(car f)

对于符号f实际可以简单的人为是:
(((λa.λb.λs s a b)1)2)
而(car f)实际上是
   (λl.l select-first) f
->(λl.l select-first)(((λa.λb.λs s a b)1)2)
->((((λa.λb.λs s a b)1)2)select-first)
->((λs s 1 2)select-first)
->(select-first 1 2)
->1

从这个例子里我们可以看到，f实际上并不仅仅是简单的lambda抽象，而是一个lambda抽象的计算(当然，根据不同的求值器结果会不一样，在eager的求值器里，f是(λs s 1 2)，也是一个lambda抽象，当然这个时候定义就变成了curry)。

因此回过头来看在lambda演算上发展出来的面向对象封装，“这个对象”和“那个对象”不过是对于某一个lambda抽象的不同计算或者不同的curry binding而已。因此透明引用、无状态和对象并没有冲突，你仍然可以透明的引用每一个对象。当然如果Elminster兄不认为他们是亲密无间的，也无所谓，起码也不是背道而驰的吧。

至于什么叫有副作用的lambda抽象，其实没有这个概念，一旦有了副作用，就不是lambda抽象了。因为α变换，β规约是替换模型，而Side-Effect不是替换模型，在lambda演算中没有一种变换可以让

   (λx.f)((λvalue.varibale)3)
->((λvalue.varibale)4)

我只不过借用这个词来表达从lambda抽象过渡到对象的一个中间状态而已。如果Elminster兄认为不好理解我再去想一个词好了。

用对象的观念看待lambda？

我觉得你说的不准确。

lambda 演算三个基本公理，α 变换，β 规约和 η 规约，没有哪一个是允许副作用的，你说引用透明性仅仅是由 η 规约指定的，恐怕有问题 —— 后面你自己也说了，α 变换，β 规约是替换模型，是不能有副作用的。说到底，lambda 演算被构造出来最初的目的是为了刻画数学意义上的函数，把函数相等、函数构造和函数作用这些概念公理化。无论是 α 变换、β 规约还是 η 规约，都是定义在 lambda 项之上的，而 lambda 项则是用来表示数学意义上的“变元”和“函数”的，换句话说，它们必然是无状态、无副作用、满足引用透明的。这就是为什么我认为“无状态、无副作用、满足引用透明”是 lambda 演算和由此发展而来的函数式语言本质特征之一的原因。

扯远了，回来说面向对象。

我是很奇怪，这该死的面向对象，怎么就能和 lambda 演算“配对”到一起呢？如你所说，“透明引用、无状态和对象并没有冲突”，这没错，但是不透明引用、状态变化和对象更没有冲突啊。简单地说，“对象”与否，和是否透明引用、状态变化根本可以是正交的，怎么就有“一切皆对象不过是一切皆lambda抽象的演化”这个结论了呢？（对了，我还得问问你，你这“lambda 抽象”是不是 lambda 项的概念？）

我比较认同这样一种观点：这面向对象和函数式，是看待问题的两种视角。简单的例子（来自 SICP 的第三章），比如我们要模拟一个电路系统，面向对象的视角是把它分解成一个个相对独立的对象，电容电感等等，它们各自有自己的状态，它们互相通信互相影响，状态也随时间而变化；而函数式的视角是分离这个电路系统的规律和状态，电路的运行规律是不变的，电流电压相位这些东西之间的关系总可以用一些数学公式来描述，然后电路的输入（用这个词不是很好，但我想不出更好的了）可以用一个流来刻画，那么整个系统就描述为一个可以是无限长的流经过一个无状态的函数的作用得到另一个无限长的流 ……

啊啊，不想再写了，我发现我的描述是这么拙劣 …… 大家还是去看 SICP 吧，第三章。

第一，我怀疑Elminster兄所知的λ Calculus跟我所知的λ Calculus不太一样。我所知的λ Calculus是丘奇在解决计算性问题的时候，所提出的一种计算模型。而Elminster兄所说的“为了刻画数学意义上的函数，把函数相等、函数构造和函数作用这些概念公理化。”跟这个不太搭界。而且我所知的λ Calculus，β 规约支主要的运算手段，但是β 规本身有个限制，就是如果我要带入的模型在表达式中不是自由变量的时候，不可以替换。因此α 变换就是用来把一些非自由形式的变量的变成自由形式的变量的。在概念上的相等性变换是 η 规约保证的。我们回过头来看引用透明，引用透明只指在任意时刻可以替换成一个对象，也就在η 规约保证下进行β 规约。因此不能保证引用透明性，仍然可以有替换模型，但是语义不正确了而已。所以其根本上还是违反了 η 规约。

第二，目前通行的说法是，第一个面向对象语言是Smalltalk，第二个是CLOS。当然具体史实可能有些出入。CLOS就是Common Lisp Object System。在Lisp之上构造的对象技术，就是把lambda抽象，以及一些副作用模块化的一种方式而已。因此对象和函数式也是一个正交的概念，我可以是函数式的，同是以对象为"方便接口"。所以把对象类比lambda不一定说对象就要和函数式有什么关系。

第三，在我那篇文章里，我是针对老庄所谓不能说一切皆对象而来的，因此我先说了在lambda这种计算模型中，可以把所有的东西表达为lambda抽象，有些对象也能表达为lambda抽象，有些对象可以看作lambda抽象带上一些副作用。因为lambda是图灵等价的，也就是我们可以用一切都是lambda来构造一个完备的语言系统，那么用一切皆对象也是可能可行的而已。这里估计是我中文不大好的缘故，没有写得很清楚，Elminster兄可能有一些误解。不知道这个解释清楚没有。
再有SICP作为入门的书还是不错，看过了明白了，自然有更好的书来读，死抱着的寻章摘句岂不是要把书读死了？

言多必失啊，言多必失……
λ Calculus再加个副作用，那是无所不能啊。啥模拟不出来啊。
俺也不同意把面向对象的对象认为“是”λ抽象。我只同意对象能够用λ Calculus加上副作用能力之后表示出来。不过那还是λ Calculus么……那不过是scheme等语言的做法而已。

一条条来回复吧。



你我说的应该是同一个 lambda 演算。就我所了解的，Church 最初提出无类型的 lambda 演算的时候（应该是 1930 年代初），是为了用它来辅助数理逻辑领域的研究，也就是为了刻画函数定义和函数作用。这个东西和递归函数、可计算函数联系起来要等到几年以后 Church 的学生 …… 那个谁的工作。而 lambda 演算和图灵机的等价性应该是又过了几年 Turing 证明的。这方面虽然我自己没有研究过，但我记忆里面有两个不同渠道的文献支持这种说法。什么时候我有闲了，去找原始文献来看看好了。

至于你说没有引用透明“根本上还是违反了 η 规约”，这个我觉得 ……  好像太轻描淡写了一点。有了副作用之后，这 lambda 演算里面甚至连 M=M 都没法保证，当然你还是可以做替换、做 α 变位、做 β 规约，然而这个说真的我感觉没啥意义 ……



很好啊，这个问题我们取得共识了，这“面向对象”和“函数式”是两个正交的概念。

不过让我非常非常意外的是，你其实只是“把对象类比lambda”？这真的是很让我意外。看你那篇 blog 长篇大论地讨论 lambda 演算，然后跟上一句“我们有理由说，对象其实就是一个lambda抽象，所以一切皆对象不过是一切皆lambda抽象的演化”，我一直以为你的观点是“面向对象是以 lambda 演算发展而来的”呢。



原来如此 ……

说起来，我觉得“一切都是 lambda 项”能够成立，和“一切都是对象”能否成立之间关系不大，如前所说，它们基本上是正交的。更进一步，讨论这个也未必有很大的意义。我们对面向对象不满，是因为我们在试着解决现实问题的时候，发现无法构造出足够灵活、易于理解、适应变化的程序，倒未必是那么形而上的想要研究能不能“一切都是对象”。



关于“如何读书”这个话题，太大而化之了，我不想说什么。还是实际一点吧：SICP 第三章里面所介绍的，在如何用程序“模拟”一个系统这个问题上的两种不同视角，你看过没有？如果看过的话，能不能说说你的看法？

函数式语言的本质到底是什么好象一直都没有共识吧？无副作用？lazy？first-class function？

大把的fp语言允许副作用；ml是eager的而haskell是lazy的。要说大家的共同点也就一个first-class function了。

至于说lamda演算，自然是fp的基石之一，不过，我也不知道怎么能用lamda演算来证明函数式就必须没有副作用。某些变态的lamd 组合子在强类型下还非法呢，难道就说明强类型和函数式茅盾么？

替换只要按照替换规则来，有没有副作用都照样替换。不能证明M==M，又如何？在副作用存在的情况下，只怕连"=="的定义都得仔细斟酌一下了吧？

当然，说OO就是lamda，更像是直觉化的主观经验论述，而不是精确地数学化的客观描述。lamda除了最基础的那个，还有变种呢。typed lamda calculus就复杂很多。我也看过一些试图给OO建模的u calculus什么的，惭愧地说，比较复杂，不是很明白。但是至少看出一点，就是各个calculus都有自己的适用范围。严格地设计和证明一套calculi不是一个很简单的工作，至少要装模作样地摆出一堆花里胡哨的数学公式和希腊字母才符合学术届的“礼制”。

函数式语言的本质只怕和 OO 的本质一样是个扯不清的话题。不过呢，虽然大把的函数式语言支持副作用，但人们把 fp 当作一个区别与其他程序设计范式的东西提起来的时候，总是指那种无赋值、无状态和无副作用的风格吧？所以我觉得说“无副作用”是函数式的本质特征之一，并没有什么问题。

至于 lambda 演算，自然是不能拿来证明函数式语言没有副作用，然则这里问题在于，当我们声称我们的语言里面“一切都是 lambda 项”的时候，实际上这个声称已经暗含了“我们的语言是以 lambda 演算为基础”这个前提，那自然就要来说说这 lambda 演算究竟能不能容忍副作用这个问题。

不过据说也是有人往 lambda 演算里面加副作用的，详情不得而知。带类型的 lambda 演算很早就有了吧？那个 System F 貌似和您老喜爱的 Haskell 牵连很深啊，