函数式编程入门书籍 Elementary Functional Programmings
在编程语言这一点上，其实本人知道的也比较有限，只是比普通程序员多懂一点。
以前读书的时候感觉周围的 PL（即 programming languages）研究者们关心的都是语言的“前中端问题”，例如类型系统和语义等；并没有太多与虚拟机、垃圾回收、IR 优化相关的话题。所以我这边推荐的入门书籍也还是以类型系统和语义为主的。
对这些入门书籍的学习不仅仅是可以很好地了解编程语言的类型系统与语义，以至为 PL 专业的硕士、博士研究生铺平道路。更重要的是可以了解 turing-machine 之外的另一种计算模型，即 lambda calculus；可以了解到大家熟悉的 imperative、state-based、loop-based 之外的另一种编程思想，即 declarative、function-based、recursion-based 的编程思想——这种新的思想不一定能带来代码运行速度上的提升，但却几乎一定能带来抽象能力、问题拆解能力的提升。
废话说得比较多了，下面是一些本人有所了解的书籍，有些可能比较旧了。而且书籍这种东西，对其评价或许也是带有很强的主观色彩的。
《Types and Programming Languages》，即耳熟能详的 TAPL，作者是 Pierce, Benjamin C。这是一本 2002 年出版的书，挺老了，但仍然是一本很棒的 PL 入门书。通过阅读（和动手），我们会学到类型系统和语义的相关知识，以及 lambda calculus 的入门知识。可以从中系统地了解多态（即 polymorphism，如 Java 泛型，C++ 模板）的几个维度：类型依赖类型（如 class List<X>），项（类型的成员）依赖类型（如 <T> boolean contains(Collection<T> c)），以及类型依赖项（常用来写证明，无法用 Java 举例）；而最后一个最为常见的且抽象层级比较低的，项依赖项，就是大家最为熟悉的函数或者说方法。书中还会详尽地介绍子类型系统、交类型、并类型，以及子类型中的型变。这些知识对于日常编程以及熟练掌握一门程序语言自然是大有裨益的。此外，贯穿全书的是语言的类型检查、语义的形式化写法，以及两个重要结论及其证明：1 通过类型检查的代码要么是值，要么可以继续计算到值（progress），2 通过类型检查的代码，计算后的结果仍然可通过类型检查（preservation）。考察一门语言时，这两点也是要重点审视的。另外，就中国内地来说，北京大学有开课，可以参考，课件或许更适合中国人学习？（有一个比较精简的，Luca Cardelli 的《Type Systems》，40 几页，复习的时候用挺好。）
《Practical Foundations for Programming Languages》，即 PFPL，作者是 Robert Harper（官方免费版戳此）。广度感觉特别广（特别是相对于上一本来说），覆盖了方方面面。唉，但一直没时间看，或者说每次看到 total functions 那里都中断了……我把大的主题（每一个主题都有若干章节）列一下吧，看完就知道有多广了：Judgments and Rules，Statics and Dynamics，Total Functions，Finite Data Types，Types and Propositions，Infinite Data Types，Variable Types，Partiality and Recursive Types，Dynamic Types，Subtyping，Dynamic Dispatch，Control Flow，Symbolic Data，Mutable State，Parallelism，Concurrency and Distribution，Modularity，Equational Reasoning。
[《Type Theory and Formal Proof: An Introduction》](Type Theory and Formal Proof: An Introduction)，我只看了前 9 章左右，就我看的部分来说，基本在讲 lambda calculus。看引用数可能不是一本特别好的书，但对初学与入门 lambda calculus 的我来说还是很有帮助的。Lambda calculus 保留了核心的函数构造和函数调用，而将其余的语言成分（如自然数）都视为前者的编码。我们会惊叹原来这两条规则已经图灵完备了，任意复杂的代码都可以由其组合出。书里让我印象比较深刻的，一是前几个章节对不同维度的多态的介绍（在第一本书 TAPL 中有提及），以及最终组合出的精美的 lambda cube；二是 lambda calculus 通过统一、简洁的符号，表示出的 term : type : kind : sort 这一条链（如 true : Bool : * : □），至此（typing 的） term : type 和（kinding 的）type : kind 的许多规则可以统一合并；三是逻辑和类型的对应关系，例如逻辑中的 P => Q 就是 P -> Q 这个函数类型呀。
《The Implementation of Functional Programming Languages》，没有博士学位的 Simon Peyton Jones 的著作，也是一本很老的书了，网上有官方公开的免费版。这本书比较注重实践，读起来没那么抽象。前半部分讲了如何对一个还算丰富的表层语言做类型检查、解糖、翻译到精简的核心语言。如果我没记错的话，核心中的核心是 match 表达式和模式匹配。后半部分讲了图规约（graph reduction）算法和基于图规约的中间表示（IR）和抽象机 G-machine，以及相关的优化算法。这是一种完全不同于栈机（stack machine）的抽象机。Haskell 的编译器 GHC 的实现中大量用到了本书中的思想（毕竟本书作者就是 “GHC 之父”）。
如果想学习函数式的数据结构和算法，那么 Chris Okasaki 的《Purely Functional Data Structures》（这里有一本）和 Richard Bird 的《Pearls of Functional Algorithm Design》（这里有一本）就挺好的。我记得读大学的时候，红黑树的删除（含旋转）操作简直是噩梦。但函数式基于模式匹配的写法，似乎十几行就完事了，理解起来异常简单。当然，我得提醒，函数式其实也没有高明到哪里，它不是万能的（这儿还有一篇文章）。
学写证明的话，最近几年新出的《The Little Typer》或许不错。活到现在还不太会写证明，抱歉。
说了这么多，其实有些大佬的页面就是宝藏。比如这位有三四个博士学位的（好像是物理、化学、计算机等）Oleg Kiselyov 的页面就够大部分学一辈子了。里头都是抽象度贼高的运行速度还贼快的硬核神奇代码，再配上论文。反正我是学不太会。
另外，上面的推荐书籍也看出来了，我不是 Lisp 派。所以就遗漏了《Structure and Interpretation of Computer Programs》、《Essentials of Programming Languages》等圣经。里面有些设计电路的章节也挺让人印象深刻的，确实巧妙。说起来就不爽，计算机理论专业干嘛要教 Verilog HDL 这种语言和用它写电路呢？听说牛津大学就是用 Haskell 写电路的。