本书详细讲解如何使用ML语言进行程序设计，并介绍函数式程序设计的基本原理。书中特别讲述了为ML的修订版所设计的新标准库的主要特性，并且给出大量例子，涵盖排序、矩阵运算、多项式运算等方面。大型的例子包括一个一般性的自顶向下语法分析器、一个l-演算归约程序和一个定理证明机。书中也讲述了关于数组、队列、优先队列等高效的函数式实现，并且有一章专门讨论函数式程序的形式论证。
　　本书可作为高等院校计算机专业相关课程的教材，也适合广大程序设计人员参考。

无

本书源于对Standard ML和函数式程序设计的讲稿。它仍可以作为函数式程序设计的课本—一本面向实用，而不是标准的、理想化的书—然而，它主要是一本有效使用ML的指南。它甚至讨论了ML的命令式特性。
　　有些内容需要离散数学的知识，例如初等逻辑和集合论。读者会发现以往的程序设计经验是有用的，但不是必需的。
　　本书是一本程序设计手册，而不是参考手册。它覆盖了ML的主要方面，但并不尽述所有的细节。它在理论原理上花费了一些篇幅，但主要还是关心高效的算法和实际的程序设计。
　　本书的组织反映了我的教学经验。高阶函数出现得较晚，在第5章讲述。惯常的做法是在一开始就介绍一些不甚自然的例子，这样做只能使学生们感到困惑。高阶函数的概念是不容易理解的，需要充分的预备知识。所以，本书从基本类型、表和树开始讲述。当讲到高阶函数时，很多相关的例子已经是现成的了。
　　练习的难度相差很大。它们不是用来评测学生的，而是为了提供实践机会，拓展内容和激发讨论的。
　　本书一览。大多数章节都专注于ML的各个方面。第1章介绍了函数式程序设计的背景思想，以及ML的历史概况。第2～5章涵盖了ML的函数式部分，包括对模块的简介。讲述了基本类型、表、树和高阶函数。对函数式程序设计的更广泛的原理也有所讨论。
　　第6章给出了论证函数式程序的形式方法。看上去似乎偏离了程序设计的主题，然而错误的程序是没用的。易于形式论证是函数式程序设计的一大好处。
　　第7章详细讲述了模块，包括函子（带参数的模块）。第8章讲述了ML的命令式特性：引用、数组和输入输出。本书的其余部分由较大的例子构成。第9章给出了函数式的语法分析器和一个l-演算解释器。第10章给出了一个定理证明机，这是ML的传统应用。
　　书中的例子非常丰富。其中一些只是为了说明ML的某个方面，但大多数本身就有一定用途—排序、函数式数组、优先队列、搜索算法、美化打印。请注意：虽然我测试过这些程序，但是它们仍不免含有错误。
　　信息和警告块。技术性的旁白、库函数的叙述以及为进一步学习而给出的笔记都会不时地出现。它们被加以如下图标以便有些读者可以跳过：
亨利王的要求。他们拿不出什么理由可以反对陛下向法兰西提出王位的要求，只除了这一点，那个在法拉蒙时代制定的一条法律，In terram Salicam mulieres ne succedant，‘在撒利族的土地上妇女没有继承权’：而法国人就把这‘撒利族的土地’曲解为法兰西的土地，并且把法拉蒙认做是这条法律的创制人和妇权的剥夺者。可是他们的历史学家却忠实地宣称撒利区是在日耳曼的土地上……
　　ML并不完美。某些缺陷会使简单的编码错误浪费掉程序员几个小时的时间。而且，新的标准库使得新旧编译器不兼容。因此，本书中有一些这样的警告图标：
小心葛罗斯特公爵。呵，勃金汉！小心那个狗东西：要知道，摇尾的狗会咬人；咬了人，它的牙毒还会叫你痛极而死；莫同他来往，千万留意；罪恶、死亡和地狱都看中了他，地下的大小役吏都在供他使唤。
　　我要赶紧补充一点，在ML里不会产生这么可怕的后果。程序里的错误是不能冲垮ML系统本身的。另一方面，程序员必须牢记，即使是正确的程序也可能给外部世界带来伤害。
　　如何得到Standard ML编译器。由于Standard ML刚出现不久，很多学院没有编译器。下面列出了现有的一些Standard ML编译器，并附有联系地址。书中的例子是在Moscow ML、Poly/ML和Standard ML of New Jersey下开发的。我尚未尝试其他的编译器。
　　要得到MLWorks，请联系Harlequin Limited, Barrington Hall, Barrington, Cambridge, CB2 5RG, England。他们的电子邮件地址是web@harlequin.com。
　　要得到Moscow ML，请联系Peter Sestoft, Mathematical Section, Royal Veterinary and Agricultural University, Thorvaldsensvej 40, DK-1871 Frederiksberg C, Denmark。或从互联网上得到该系统：
http://www.dina.kvl.dk/~sestoft/mosml.html
要得到Poly/ML，请联系Abstract Hardware Ltd, 1 Brunel Science Park, Kingston Lane, Uxbridge, Middlesex, UB8 3PQ, England。他们的电子邮件地址是lambda@ahl.co.uk。或从互联网上得到该系统：
http://www.polyml.org/
　　要得到Poplog Standard ML，请联系Integral Solutions Ltd, Berk House, Basing View, Basingstoke, Hampshire RG21 4RG, England。他们的电子邮件地址是isl@isl.co.uk。
　　要得到Standard ML of New Jersey，请联系Andrew Appel, Computer Science Department, Princeton University, Princeton NJ 08544-2087, USA。更好的是可以从互联网上得到文件：
http://www.cs.princeton.edu/~appel/smlnj/
http://www.smlnj.org/
　　书中的程序和一些练习答案可以通过电子邮件得到，我的电子邮件地址是lcp@cl.cam.ac.uk。如果可能，请使用互联网，我的主页在
http://www.cl.cam.ac.uk/users/lcp/
致谢。编辑，David Tranah，在写作的各个阶段提供了帮助，并建议了书名。Graham Birtwistle、Glenn Bruns和 David Wolfram仔细阅读了文本。Dave Berry、Simon Finn、Mike Fourman、Kent Karlsson、Robin Milner、Richard O誎eefe、Keith van Rijsbergen、Nick Rothwell、Mads Tofte、David N. Turner和Harlequin的工作人员也对文本提出了意见。Andrew Appel、Gavin Bierman、Phil Brabbin、Richard Brooksby、Guy Cousineau、Lal George、Mike Gordon、Martin Hansen、Darrell Kindred、Silvio Meira、Andrew Morris、Khalid Mughal、Tobias Nipkow、Kurt Olender、Allen Stoughton、Reuben Thomas、Ray Toal和Helen Wilson发现了前几次印刷中的错误。 Piete Brooks、John Carroll和Graham Titmus在计算机使用方面给予了帮助。我还要感谢Dave Matthews开发了Poly/ML，这是多年以来唯一高效的Standard ML的编译器。
　　在众多的参考文献中，Abelson和Sussman（1985）、Bird和Wadler（1988）以及Burge（1975）的著作特别有帮助。Reade（1989）的书中包含了在ML中实现惰性表的有用思想。
　　The Science and Engineering Research Council在过去20多年来给予了LCF和ML大量的研究资助。
　　本书的大部分写作工作都是我从剑桥大学休假的过程中完成的。我感谢计算机实验室（Computer Laboratory）和卡莱尔学院（Clare College）给予休假，以及爱丁堡大学对我六个月的招待。
　　最后，我要感谢Sue，感谢她所给我的一切帮助，以及天天耐心倾听我关于每一章进展的报道。

柯韦：暂无简介

多年前我曾经认为自己是一个程序员，对程序设计有着执著的兴趣。试图洞悉本质的渴望以及相关知识的匮乏往往令我陷入苦思。于是我开始了新一轮的阅读。在一个图书馆中书架林立的某处，我发现了这本写给程序员的书。在我相对贫乏的阅读历史中，书名带有“程序员”（programmer）的寥寥无几，又怎能不留意呢？这本书最终没有让我失望。
　　如果说过去我对程序设计有过一些有意义的思考，而从中得到了乐趣的话，函数式程序设计则系统地叙述了这些令人兴奋的闪光之处。这种基于某种数学概念的方法把我们从程序运行的细节中解放出来，转而关注如何去表达。程序因此变成一个个静态的方程式，安详地躺在那里，展示着简单而丰富的内涵。我们则不再被传统的动态步骤困扰，思想在清晰的、静态的表达基础上轻松地延伸着，这是多么美妙的感受啊！我们曾经认为，如果无法理解赋值语句就不能进行程序设计，我们费了多少力气去习惯它，以至于后来已完全在脑海中根深蒂固了。现在我们要从这种被扭曲的思维中走出来，回到更为自然的思考方式去，而函数式程序设计则是众多方法中的一个。
　　ML语言是函数式语言中较为经典的，它的语法简单优美，语义清晰准确并易于理解，语言的实现也相当高效和严谨。和最新式的函数式语言不同，ML牺牲了一些数学上的纯粹性，换来了相对简单的语义描述，理解它不需要十分高深的数学抽象思考。这对于语言的实用性是十分重要的。正如书中所说，我们不希望从机器语言繁琐的运行步骤中走出来，而立即又掉进同样复杂繁琐的数学模型中去。作为一种入门的函数式程序设计语言，ML不仅对于初学程序设计的学生是一个好的语言，对于有经验的程序员来说也是一个好的桥梁，程序员们将或多或少地发现，他们过去的一些思考竟有如此简单的归宿。我想，这也是原书命名的由来。
　　原书是一本非常流行的ML语言和函数式程序设计教材，尽管第2版面世至今已有很长时间了，但依旧被国外许多大学的相关科目广泛采用。书中在介绍ML语言的同时更多地阐述了语言和函数式程序设计的思考方法。大量的例子条理分明，深浅搭配适度。随处可见的精心安排的旁白涉及了计算机语言理论研究的许多方面，作为科普读物来说也非常赏心悦目。我很喜欢这本书，衷心地希望能将之介绍给更多的中国读者。我的翻译工作是认真而仔细的，然而由于水平有限，令人遗憾之处恐在所难免，希望读者不要因此受阻，能在阅读中有所收获。
　　我感谢机械工业出版社，她们出版了许多计算机基础理论的译著，这一本也不例外。我衷心希望此举能将计算机不仅作为一种技术，也作为一种科学推广，产生更多的思想积淀，形成更广泛的基础。我还要感谢在此书翻译过程中给我宝贵指点和帮助的各位尊敬的老师和编辑们。原书的作者Paulson博士也对我的提问作出了耐心的讲解。

第2版序
　　每次重新印刷，书中的一些小错误都会悄悄地消失。但是重新印刷并不会做大的改进，尽管改进是很有意义的。因为这样做会影响页码编号，使内容产生差别而互不兼容。重大的改动积累起来（以及编辑的催促）便产生了这个第2版。
　　非常幸运的是，对ML语言的改动都凑到了一起。ML有了新的标准库，并且语言本身也经过了修订。值得强调的是，这些改动没有牺牲ML固有的可靠性。一些晦涩的技术要点已经得到简化，原先定义中不合适的地方也改正了。现有的程序几乎不用改动就可以继续运行。最明显的改动是增加了新的字符类型，还有一套新的顶层库函数。
　　这版新书及时反映了语言的变化，并在格局安排上做了很大的改进。模块提前到第2章就介绍了，而不是放到第7章，它的使用贯穿全书。这使得重点有所转移，从数据结构（比如二叉搜索树）变为抽象类型（比如字典）。抽象类型通常在某一小节引入，并给出它的ML签名。然后讲解实现背后的思想，最后给出ML结构的代码。虽然评审对第1版较为宽容，但是许多读者要求重新组织内容。
　　书中的程序不仅移动了位置，而且重新编写过。它们反映了如何使用模块的新思路。由于open声明会隐藏模块结构，所以已经很少出现了。函子也仅在需要的时候才使用。现在，程序的缩进也排得很仔细了，加上其他改进，代码变得更加易读，质量也更好了，表现在合并排序更为简单迅速，优先队列也更快了。
　　新标准库也要求尽早地提到模块。尽管这样做就必须修改现有代码，但它能使ML在现实语言中的地位更加稳固。新标准库的设计经过了漫长的磋商过程，主要是为了提供全面的支持，同时避免过分的复杂化。它的组织显示了ML模块的优点。字符串处理、输入输出和系统接口这些模块都提供了实际的功能改进。
　　新标准库导致很多代码必须重写。当新标准库包含函数foldl时，读者一般不愿意再看到以前类似的函数foldleft。但是这些函数不是完全一样的，所以，重写并不只是改个名字那么简单。很多曾讲述实用函数的章节，现在都要对照新标准结构进行检查更新。
　　更新过的参考文献说明了函数式程序设计和ML在各领域的广泛应用。ML符合构建可靠系统的要求。软件工程师们需要一种能提供类型安全、模块化、编译时一致性检测和容错（异常）的语言。ML程序是可移植的，这要部分归功于标准库。商业化的编译器正在不断提高质量和效率。ML的运行速度可以和C媲美，特别是在需要复杂存储管理的应用场合。本书的名字（指英文书名）曾引来一些嘲笑，但却给出了很好的提示。
　　我最惊讶的是看到第1版出现在初级程序员的手中，尽管第一页上写着让他们看点别的书。为了帮助初学者，我加入了一些特别简单的例子，并将大多数参考引用从正文中移走。重写了第1章，试图以一种既适合初学者又适合有经验的C程序员的方式介绍基本的程序设计概念。这比听上去要容易：C并不想给程序员一个解决问题的环境，而仅仅是给底层的硬件稍加装扮。第1章仍旧包含一些基本的计算机常识，但教师也许还是喜欢从第2章开始讲述，因为它带有简单的会话过程。
　　在书的末尾列出了一些项目建议。我故意说得不很明确，因为一个大项目的第一步就是准确地分析需求。我希望看到越来越多的人在项目中采用ML，选择ML，特别是取代像C这样不安全的语言，最终会被看作是专业的一种标志。
　　我非常感谢所有对这一版给出有用的意见、建议或代码的人们。他们分别是Matthew Arcus、Jon Fairbairn、Andy Gordon、Carl Gunter、Michael Hansen、Andrew Kennedy、David MacQueen、Brian Monahan、Arthur Norman、Chris Okasaki、John Reppy、Hans Rischel、Peter Sestoft、Mark Staples和Mads Tofte。Sestoft还给了我一个Moscow ML的预发行版，含有库的更新。CUP的Alison Woollatt编写了的类文件。Franklin Chen和Namhyun Hur报告了前一版中的错误。

第1章　 Standard ML 1函数式程序设计 2
1.1　 表达式和命令 2
1.2　 过程式程序设计语言中的表达式 3
1.3　 存储管理 3
1.4　 函数式语言的元素 4
1.5　 函数式程序设计的效率 7
Standard ML概述 8
1.6　 Standard ML的演化 8
1.7　 ML的自动定理证明传统 9
1.8　 新标准库 10
1.9　 ML和工作中的程序员 11
第2章　 名字、函数和类型 13
本章提要 13
值的声明 14
2.1　 命名常量 14
2.2　 声明函数 15
2.3　 Standard ML中的标识符 16
数、字符串和真值 17
2.4　 算术运算 17
2.5　 字符串和字符 19
2.6　 真值和条件表达式 20
序偶、元组和记录 21
2.7　 向量：序偶的例子 21
2.8　 多参数和多结果的函数 22
2.9　 记录 24
2.10　 中缀操作符 27
表达式的求值 29
2.11　 ML中的求值：传值调用 29
2.12　 传值调用下的递归函数 30
2.13　 传需调用或惰性求值 33
书写递归函数 36
2.14　 整数次幂 36
2.15　 斐波那契数列 37
2.16　 整数平方根 39
局部声明 39
2.17　 例子：实数平方根 40
2.18　 使用local来隐藏声明 41
2.19　 联立声明 42
模块系统初步 44
2.20　 复数 44
2.21　 结构 45
2.22　 签名 46
多态类型检测 47
2.23　 类型推导 47
2.24　 多态函数声明 48
要点小结 50
第3章　 表 51
本章提要 51
表的简介 51
3.1　 表的构造 52
3.2　 表的操作 53
基本的表函数 54
3.3　 表的测试和分解 55
3.4　 与数量有关的表处理 56
3.5　 追加和翻转 58
3.6　 表的表，序偶的表 60
表的应用 61
3.7　 找零钱 61
3.8　 二进制算术 63
3.9　 矩阵的转置 64
3.10　 矩阵乘法 66
3.11　 高斯消元法 67
3.12　 分解一个数为两个平方数之和 70
3.13　 求后继排列的问题 71
多态函数中的相等测试 72
3.14　 相等类型 73
3.15　 多态集合操作 73
3.16　 关联表 76
3.17　 图的算法 77
排序：案例研究 81
3.18　 随机数 81
3.19　 插入排序 82
3.20　 快速排序 83
3.21　 合并排序 84
多项式算术 86
3.22　 表示抽象数据 87
3.23　 多项式的表示 87
3.24　 多项式加法和乘法 88
3.25　 最大公因式 90
要点小结 91
第4章　 树和具体数据 93
本章提要 93
数据类型声明 93
4.1　 国王和他的臣民 94
4.2　 枚举类型 95
4.3　 多态数据类型 97
4.4　 通过val、as、case进行模式匹配 99
异常 101
4.5　 异常初步 101
4.6　 声明异常 102
4.7　 抛出异常 103
4.8　 处理异常 105
4.9　 对异常的异议 106
树 107
4.10　 二叉树类型 107
4.11　 枚举树的内容 109
4.12　 由表建立树 111
4.13　 为二叉树设计的结构 112
基于树的数据结构 112
4.14　 字典 113
4.15　 函数式数组和弹性数组 116
4.16　 优先队列 120
重言式检测器 124
4.17　 命题逻辑 124
4.18　 否定范式 126
4.19　 合取范式 127
要点小结 129
第5章　 函数和无穷数据 131
本章提要 131
作为值的函数 131
5.1　 使用fn记法的匿名函数 132
5.2　 柯里函数 132
5.3　 数据结构中的函数 135
5.4　 作为参数和结果的函数 135
通用算子 137
5.5　 切片 137
5.6　 组合子 138
5.7　 表算子map（映射）和 filter（过滤） 139
5.8　 表算子takewhile和dropwhile 141
5.9　 表算子exists（存在）和all（全称） 141
5.10　 表算子 foldl（左折叠）和foldr（右折叠） 142
5.11　 更多递归算子的例子 144
序列，或无穷表 147
5.12　 序列类型 147
5.13　 基本的序列处理 149
5.14　 基本的序列应用 151
5.15　 数值计算 153
5.16　 交替和序列的序列 155
搜索策略和无穷表 156
5.17　 用ML实现的搜索策略 158
5.18　 生成回文 159
5.19　 八皇后问题 160
5.20　 迭代深化 161
要点小结 162
第6章　 函数式程序的论证 163
本章提要 163
一些数学证明的原理 163
6.1　 ML程序和数学 164
6.2　 数学归纳法和完全归纳法 165
6.3　 程序验证的简单例子 168
结构归纳法 171
6.4　 关于表的结构归纳法 171
6.5　 关于树的结构归纳法 175
6.6　 函数值和算子 178
一般性归纳原理 181
6.7　 计算范式 182
6.8　 良基归纳和递归 185
6.9　 递归程序模式 187
描述和验证 189
6.10　 有序谓词 190
6.11　 通过多重集合表示重新排列 191
6.12　 验证的意义 194
要点小结 195
第7章　 抽象类型和函子 197
本章提要 197
队列的三种表示方法 198
7.1　 将队列表示为表 198
7.2　 将队列表示为新的数据类型 199
7.3　 将队列表示为表的序偶 200
签名和抽象 201
7.4　 队列应具有的签名 202
7.5　 签名约束 202
7.6　 抽象类型（abstype）声明 204
7.7　 从结构导出的签名 206
函子 207
7.8　 测试多个队列结构 208
7.9　 泛型矩阵运算 210
7.10　 泛型的字典和优先队列 214
利用模块建立大型系统 217
7.11　 多参数函子 217
7.12　 共享约束 221
7.13　 全函子式程序设计 224
7.14　 open声明 228
7.15　 签名和子结构 232
模块参考指南 234
7.16　 签名和结构的语法 235
7.17　 模块声明的语法 237
要点小结 237
第8章　 ML中的命令式程序设计 239
本章提要 239
引用类型 239
8.1　 引用及其操作 240
8.2　 控制结构 242
8.3　 多态引用 245
数据结构中的引用 249
8.4　 序列，或惰性表 249
8.5　 环形缓冲区 252
8.6　 可变更的数组和函数式的数组 255
输入和输出 259
8.7　 字符串处理 259
8.8　 文本输入输出 262
8.9　 文本处理的例子 264
8.10　 美化打印程序 267
要点小结 271
第9章　 书写l-演算的解释器 273
本章提要 273
函数式语法分析器 273
9.1　 扫描或词法分析 273
9.2　 自顶向下的语法分析套件 275
9.3　 语法分析器的ML代码 277
9.4　 例子：分析和显示类型 280
l-演算简介 284
9.5　 l-项和l-归约 284
9.6　 在替换中防止变量的捕获 286
在ML中表示l-项 288
9.7　 基本操作 288
9.8　 l-项的语法分析 290
9.9　 显示l-项 291
作为程序设计语言的l-演算 293
9.10　 l-演算中的数据结构 293
9.11　 l-演算中的递归定义 296
9.12　 l-项的求值 296
9.13　 演示求值程序 299
要点小结 301
第10章　 策略定理证明机 303
本章提要 303
一阶逻辑的相继式演算 303
10.1　 命题逻辑的相继式演算 304
10.2　 证明相继式演算中的定理 305
10.3　 量词的相继式规则 307
10.4　 带量词的定理证明 308
在ML中处理项和公式 310
10.5　 表示项和公式 310
10.6　 分析和显示公式 312
10.7　 合一 316
策略和证明状态 319
10.8　 证明状态 319
10.9　 ML签名 320
10.10　 用于基本相继式的策略 321
10.11　 命题策略 323
10.12　 量词策略 324
搜索证明 326
10.13　 变换证明状态的命令 326
10.14　 两个使用策略的证明实例 328
10.15　 策略算子 330
10.16　 一阶逻辑的自动策略 333
要点小结 336

项目建议 337
参考文献 339
Standard ML语法图 347
语法图中英词汇对照表 357
索引 359
预定义标识符 367