编程语言的设计原理 / 2025春

课程简介

新型编程语言层出不穷，这些语言是如何设计出来的？主流语言中不断扩展出新的高级语言特征，这些特征是如何定义的？面向对象编程、函数式编程、泛型编程等新型编程范式是否有共通的理论基础？本课程将揭示这些问题的答案。

类型理论是指导编程语言设计的一系列原理和方法的核心。类型声明是现代语言避免编程错误的一个基本手段，而类型理论阐释了良好的类型系统应该具有的特征和复杂的类型系统的定义方法。本课程将围绕类型理论这个核心组织和讲授编程语言的理论。通过本课程的学习，同学们在编程语言领域获得扎实的理论功底和实践能力，为开展编程语言学术研究打下基础，胜任设计编程语言的任务。

课程信息

地点：昌平教学楼 109
时间：第1周–第16周 星期一 第7–9节

课程大纲

详细内容

近年来，编程语言的发展呈现两个鲜明的趋势：1）从简单低级语言到复杂高级语言；2）从少量通用语言到大量领域特定语言。曾经在编程语言排行榜上占绝对统治地位的 C 和 Java 逐渐被 Python、Javascript、Go、Rust 等新型编程语言所挤压。一方面大量经典语言也持续扩展，引入各种高级语言成分，例如，Java 起初的设计目标为一个简化版的语言，但最新的 Java 版本已经包含了泛型、函数式编程、反射等多种高级特性；一方面有更多的编程语言不断涌现，以适应特定的应用领域中设计专门的程序语言的需求。

在这样的情况下，掌握设计编程语言的能力，已经不再是资深的编程语言研究者和前沿科研人员所独具的高级技能，而是软件开发人员的必备能力。同时，对编程语言设计原理的了解和掌握，也有助于更好地理解高级语言中的新特性，以更好地使用新型编程语言。

那么层出不穷的编程语言是如何设计出来的？主流语言中不断扩展出新的高级语言特征，这些特征是如何定义的？面向对象编程、函数式编程、泛型编程等新型编程范式是否有共通的理论基础？本课程将揭示这些问题的答案。

为指导编程语言的设计，研究人员已经提出了一系列的原理和方法，其中最核心的就是类型理论。类型声明是现代语言中避免编程错误的一个基本手段，而类型理论解释了良好的类型系统应该具有的特征和复杂的类型系统的定义方法。本课程将围绕类型理论这个核心组织和讲授编程语言的理论和实现。

本课程具有两个特点：1. 严谨性：课程中的概念元素都将有严格的形式定义，可以进行形式演绎和归纳，而非空泛的概念介绍。2. 操作性：课程中的所有重要概念都将通过课程作业的方式编程实现，在动手过程中真正掌握知识。通过本课程的学习，同学们在编程语言领域获得扎实的理论功底和实践能力，在产业方面能胜任设计编程语言的任务，在学术方面为开展编程语言相关研究打下基础。

参考书目

Types and Programming Languages, Benjamin C. Pierce, The MIT Press, 2002.（教材）

Practical Foundations for Programming Languages, Robert Harper, Cambridge University Press, 2016.（参考书）

参考代码

Types and Programming Languages 教材的参考 OCaml 代码实现可以在教材主页上找到。

今年的课程拟从 OCaml 语言切换为 MoonBit 语言，课程中涉及的代码实现在 https://github.com/pku-dppl/TAPL-in-MoonBit/。

内容提要

往年课程

• 2022春
• 2023春
• 2024春
• 2025春

任课教师

赵海燕
副教授

王迪
助理教授

课程助教

练琪灏
mepy@stu.pku.edu.cn