自序

提到计算机编程语言，很多人只听说过流行的语言，如 C、C++、Java、Python等。事实上，计算机科学家还创造了一类函数式编程语言，如 Lisp、Scheme、Clojure、Erlang、 OCaml、Haskell、F#等。目前函数式编程语言的用户数较少，而且大部分用于学术研究而非商业，因此普及程度远远不能与流行语言相比。但是，的确有一些大型商业项目的开发基于函数式编程语言。例如， Jane Street是一家从事金融量化交易的跨国公司，拥有 400多名 OCaml程序员和超过 1500万行 OCaml代码，以支撑每天数十亿美元的交易。另外，近年来形式化验证方法逐渐受到关注，函数式语言广泛用于开发编译器、程序分析器、验证器及定理证明器，以帮助提高软硬件系统的可信程度。
在这样的背景下，作者认为有必要在国内开展函数式程序设计相关的教学工作。深入讲解函数式编程需要比较多的学时，而目前不少大学在主推通识教育，希望压缩专业课程的学时数，因此，一种可能的办法是开设一门本科选修课程，或者是在一门编程语言课程中预留学分给函数式编程教学模块。本书的编写目的是服务于这类函数式程序设计入门课，重点让学生有机会了解函数式程序设计的基本思想和概念，让学生了解、欣赏，进而喜欢函数式编程。至于函数式语言背后极其丰富的语义理论，更适合设置在软件理论专业的研究生课程中，因此不在本书予以讨论。
本书主要介绍 ζ-演算、Coq和 OCaml，通过这些内容的掌握，相信读者可以触类旁通，轻松学习其他函数式编程语言。关于这三部分内容，如果读者希望了解更多，有专门的书籍进行深入讲解，例如， ζ-演算的经典教材是 Barendregt的 [2]，Coq的著名教材是 Pierce等的 [13]，OCaml的优秀参考书是 Minsky等的 [10]和陈钢老师的 [5]。本书精心挑选了一些练习题，希望读者通过做练习加强对基本概念的理解。
希望本书的出版能够为国内计算机程序设计和形式化验证方向的专业人才培养贡献微薄之力。
邓玉欣 
2023年 3月上海

前言

函数式程序设计是计算机科学中非常重要、历史比较长久的一个研究方向，但本人在教学过程中发现国内还没有一本系统介绍这个方向而且适合初学者的读物。为此，通过总结国内外相关文献和过去五年的教学实践，本人尝试编写了这本教材 ——《函数式程序设计》。
在内容选取上，本书只涉及 ζ-演算、Coq和 OCaml。毫无疑问， ζ-演算是理解函数式编程语言的基础和出发点，因此我们介绍相关的语法和归约语义。虽然 ζ-演算适合理解函数式编程的一些核心思想，比如数据即函数，但是它的语法构造比较原始，即使表示一个数字，都要写很长的 ζ-项，可读性低，更不用提编写程序。 Coq是离 ζ-演算比较接近但又能用于编写一些可读性较好的计算函数的编程语言，因此值得重点介绍。 Coq是用于讲授归纳定义和归纳证明思想的出色工具，不过它的长处在于定理证明，若要深入讲解，需要很大篇幅，因此最好留给专门的书籍，而在入门课程中只讲解基本的证明方法。为满足适合逻辑证明的需要， Coq只接受可终止的函数。这么强的要求，决定它不可能用于日常编程。因此，最后我们介绍一门通用的编程语言 OCaml，除了基本的程序设计概念，我们还会讨论一些比较高级的特征。
本书共分 4章。
第 1章 ζ-演算。先概述 ζ-演算的起源，然后介绍不带类型的 ζ-演算、简单类型的 ζ-演算和 F系统。
第 2章 Coq。从函数式编程的角度介绍归约规则、列表、多态列表、依赖类型、高阶函数、柯里-霍华德关联及余归纳类型等。
第 3章 OCaml。介绍基本的程序设计概念，例如数据类型与函数、控制结构、异常、模块，以及函子和单子这样比较高级的语言特征。
第 4章部分习题参考答案。为前三章部分有难度的习题提供参考答案，方便感兴趣的读者自行学习。
本书由浅入深，从基础原理到高级的语言特征逐步介绍，具有通俗、系统、宽广的特点，适合作为普通高等院校计算机科学和软件工程专业的本科生教学参考书，同时也可作为软件理论方向研究人员的入门读物。
感谢傅育熙老师、陈钢老师和曹钦翔老师对本书部分内容提出的宝贵意见。感谢清华大学出版社龙启铭和常建丽两位编辑在出版过程中给予的热情帮助。本书由华东师范大学精品教材建设专项基金资助。
由于作者水平有限，书中的疏漏和不足之处在所难免，恳请广大读者及时指正！
邓玉欣 
2023年 5月上海