逻辑与计算之间最深刻的联系是一种双关。「命题即类型」的学说断言， 形式化的结构可以按两种方式看待：可以看做逻辑中的命题，也可以看做计算中的类型。 此外，相关的结构可以看做命题的证明或者其相应类型的程序。更进一步来说， 证明的化简与程序的求值对应。

与此相应，本书的名字也有两种含义。它可以看做「编程语言的基础」，也可以看做 「编程的语言基础」。我们在 Agda 证明助理中编写的规范（Specification） 同时描述了编程语言以及该语言编写的程序自身。

本书面向本科最后一年学有余力的学生，或者一年级的研究生或博士生。 本书以简单类型 λ-演算（Simply-Typed Lambda Calculus，简称 STLC）作为核心示例， 旨在教授编程语言的操作语义基础。全书以 Agda 文学脚本的形式写成。 使用证明助理可以让开发过程变得更加具体而清晰易懂，还可以给予学生即时反馈， 帮助学生发现理解有误的地方并及时纠正。

本书分为两册。第一分册为逻辑基础，发展了所需的形式化工具。第二分册为编程语言基础， 介绍了操作语义的基本方法。

个人言论

从 2013 年开始，我在爱丁堡大学为四年制本科生和研究生教授编程语言的类型和语义的课程。 该课程的早期版本基于 Benjamin Pierce 的著作 TAPL。我的版本则基于 Pierce 的后续教材 Software Foundations（中文版《软件基础》），此书为 Pierce 与他人合著，基于 Coq 编写。正如 Pierce 在 ICFP 的主题演讲 Lambda, The Ultimate TA 中所言，我也相信基于证明助理的课程会对学习有所帮助。

然而有了五年的教学经验后，我得出了 Coq 并不是最好的授课载体的结论。 对于学习编程语言理论的基础而言，我们花费了太多课程去专门学习证明推导的策略（Tactic）。 每个概念都需要学习两遍：例如，在学过一遍积数据类型（Product Data Type）之后， 我们还要再学一遍与之对应的连词（Conjunction）的引入（Introduction）和消除（Elimination）策略。 Coq 用来生成归纳假设（Induction Hypothesis）的规则有时看起来很玄学。而 notation 构造则允许直观但灵活多变的语法，同一个概念总是有两个名字有时会令人迷惑， 例如，subst N x M 和 N [x := M]。策略的名字时短时长；标准库中的命名约定则非常不一致。 命题即类型作为证明的基础虽然存在，但却被雪藏了。

我发现自己热衷于用 Agda 重构此课程。在 Agda 中，我们不再需要学习策略了： 这里只有依赖类型编程，简单纯粹。我们总是通过构造子来引入，通过模式匹配来消除。 归纳不再是谜之独立的概念，它与我们熟悉的递归概念直接对应。混缀语法十分灵活， 但每个概念只需要一个名字，例如代换就是 _[_:=_]。标准库虽不完美，但它的一致性却很合理。 命题即类型作为证明的基础则被骄傲地展示了出来。

然而，此前还没有 Agda 描述的编程语言理论教材。虽然 Stump 的 Verified Functional Programming in Agda 涵盖了相关的范围， 但比起编程语言理论，却更多关注于依赖类型编程。

本书最初的目标只是简单地改编《软件基础》，保持同样的内容，而只是将代码从 Coq 翻译成 Agda。但五年的课堂经验让我很快就明白了，自己有一些关于如何展示这些材料的想法。 有人说除非你不得不写书，否则绝对不要写书。而我很快就发现这是一本我不得不写的书。

我很幸运地得到了我的学生 Wen Kokke 的热情帮助。她引导着我站在 Agda 新手的视角写书，还提供了一些十分易用的工具来产生清晰易读的的页面。

这里的大部分内容都是在 2018 年上半年的休假期间写的。

— Philip Wadler, Rio de Janeiro, January–June 2018

习题说明

标有（推荐）的习题是爱丁堡大学使用本教材的课程中学生需要做的。

标有（延伸）的习题提供了额外的挑战。很少有学生全部做完，但大部分练习至少应该尝试一下。

没有标记的习题供想要更多实践的学生练习。