函数式编程是近年来的热门话题，但其中一些概念和理论经过层层转述，往往难以辨识真伪，这导致函数式编程成为计算机民科的重灾区，本文试图梳理一些函数式编程理论的历史与大师级人物，也提供一些原始论文链接，希望帮助大家明辨。

最初的lambda演算：Alonzo Church

谈到函数式，首先当然要说到Alonzo Church（阿隆佐·邱奇），lambda演算的发明人。

Alonzo Church本人生活的年代决定了他与计算机关系不大。Alonzo Church是一位纯粹的数学家，他发明的lambda演算的初衷是为数学创造一个统一的理论基础。

最早发明lambda的时间甚至早于图灵的研究，后世的研究表明，lambda演算是图灵机等价的。

对数学爱好者来说，仅仅包含一个$\lambda$符号的lambda演算毫无疑问比又是纸带又是命令的图灵机更为优美。

后世基于lambda演算的编程语言多数也继承了这样的特点，它们多数崇尚统一的抽象，以简洁的语法和运行时机制为美。这也形成了函数式编程对其它编程范式的鄙视链。

lambda的可计算性：John Barkley Rosser

John Barkley Rosser是Church的学生，他沿袭了导师的学术流派，致力于发展和研究lambda演算。

他与导师Church合作证明了Church-Rosser定理，这个定理是lambda体系中“可计算”的重要基石，后世还引出函数式计算优越的并行特性。

作为图灵机的等效理论，试图为数学奠定基石的lambda演算也受到lambda版停机问题和一阶逻辑不完备性的困扰，他发现并证明了Kleene–Rosser悖论，Rosser在这个领域做了大量的研究工作。

组合子逻辑：Haskell Brooks Curry

Haskell Brooks Curry 也是函数式编程历史上不得不提到的人物，他的名字的三个部分，分别成为三门颇具有影响力的计算机语言的名字。

Haskell Brooks Curry 师从数学大家希尔伯特，他在lambda演算的基础上，提出了组合子逻辑。

他从与John Rosser的通信中了解到了Kleene-Rosser悖论，然而与Church，Kleene和Rosser不同的是，柯里并没有放弃基础的方法，他说他不想“逃离这个悖论”。

Haskell的研究并不能突破Kleene-Rosser悖论本身，但他的组合子逻辑和其它工作为高级语言提供了非常重要的理论支持，如果说Church和Rosser是纯粹的数学家，那么Haskell可以说是真正对计算机语言有研究的数学家。

因此他在程序员中的地位和知名度要超过Church等人。

闭包：Peter John Landin

随着lambda演算和组合子逻辑逐渐被计算机学家关注，Peter John Landin，一位真正的实战派计算机学家开始了对这方面的研究。

他从计算机的视角出发，提出了”闭包”的概念，为计算机执行lambda表达式提供了理论基础。

Peter John Landin的工作不仅仅在理论计算方面，他在编程语言设计的理论和实践都颇有建树，他提出的SECD自动机，是第一个被精确描述的虚拟机，至今仍影响着很多高级语言的运行时机制。

Peter John Landin还发明了自己的编程语言，ISWIM。这一语言尽管没有被广泛实用，但是在理论计算机领域有非常重要的地位，它影响了后世很多语言的设计。你至今仍可以在Haskell语言中看到一些它的影子。

The mechanical evaluation of expressions

$\lambda_v$和$\lambda_n$： Gordon Plotkin

随着理论计算机学术界对lambda的关注，古典的lambda演算不足以为新的计算机语言提供理论支持。

以Gordon Plotkin为代表的计算机学家开始研究对lambda演算的扩展。

Gordon Plotkin最为著名的研究是早年对ISWIM语言的建模。它在lambda中尝试引入了”二等公民”，值类型，以此构建了 $\lambda_v$演算，并在其中重新推导了Church-Rosser等基础定理。

在同一论文中，Gordon 也讨论了call-by-name的编程语言建模，引入了$\lambda_n$演算。

Gordon的学派致力于函数式编程的理论基础，他在后期还主导了在编程语言中引入Algebraic Effects（代数效果）概念的一系列相关研究。

Algebraic Operations and Generic Effects

Handlers of Algebraic Effect

Call-by-name, Call-by-value, and The λ-Calculus

Monad与范畴论：Eugenio Moggi

受导师的研究启发，Gordon 的学生 Eugenio Moggi 在他的博士论文中提出了$\lambda_p$演算，即”Partial（部分的）”lambda演算，这一理论进一步提升了lambda的相等性判定能力。

毕业之后，Eugenio Moggi仍致力于lambda的相等性判定的研究，他在尝试构建$\lambda_c$演算的过程中，提出了一个重要的抽象：在函数式编程中引入范畴论。

在论文中，他以 Monad 和 Kleisli 范畴对计算建模，考虑了现代编程语言中的各种特性，如：

• 部分计算
• 不确定性计算
• 副作用
• 异常
• 可恢复中断执行
• 交互输入
• 交互输出

这些特性的计算都可以用 Monad 进行抽象。

这个抽象模型对后世的影响甚至超越了$\lambda_c$演算本身。

Notions of computation and monads

结语

函数式编程发展历史比较长，大部分资料符号化程度又比较高，所以属于比较难以学习的内容。

本文试图从函数式编程理论的历史与人物角度出发，梳理了历史上关键的理论和人物，供有兴趣的同学顺藤摸瓜，阅读相关论文。因为描述中基本都是主观描述，如你认为不正确，欢迎评论指出。