编程语言的设计原理 / 2024春
新通知
- 2024/05/27 讲义：Type Inference
-
2024/05/27
作业：
王迪：
Type Inference[2024/06/03 截止]
课程简介
新兴的程序设计语言层出不穷，这些语言是如何设计出来的？主流语言中不断扩展出新的高级语言特征，这些特征是如何定义的？面向对象、函数语言、泛型编程等新型编程模型是否有共通的理论基础？本课程将揭示这些问题的答案。类型理论是指导编程语言的设计的一系列原理和方法的核心。类型声明是现代语言避免编程错误的一个基本手段，而类型理论阐释了一个良好的类型系统应该具有的特征和复杂类型的定义方法。本课程将围绕类型理论这个核心组织和讲授程序设计语言的理论。希望通过本课程的学习，使得同学们在编程语言领域具备扎实的理论功底和实践能力，为开展程序语言相关学术研究打下基础，胜任设计新语言的任务。
课程信息
地点：昌平教学楼 206
时间：第1周-第16周 星期一 第7-9节
课程大纲
详细内容
近十多年来，编程语言的发展呈现两个鲜明的趋势：1）从简单语言到复杂高级语言； 2）从固定少量语言到大量领域特定语言。曾经在编程语言排行榜上占绝对统治地位的C和Java渐被Javascript, Erlang, R等新型编程语言所挤压。一方面大量经典语言也持续扩展，引入各种高级语言成分,例如，Java起初的设计目标为一个简化版的语言，但最新的Java 8设计中已经包含了泛型、函数式编程、动态性等多种高级特性；一方面有更多的编程语言不断涌现，以适应特定的应用领域中设计专门的程序语言的需求。
在这样的情况下，掌握设计新的编程语言的能力，已经再独属资深的程序语言研究者和前沿科研人员所掌握的高级技能，而是软件开发人员的必备能力。同时，对语言设计原理的了解和掌握，也有助于更好的理解高级语言中的各种新特性，以更好的使用主流编程语言。
那么层出不穷的程序设计语言是如何设计出来的？ 主流语言中不断扩展出新的高级语言特征，这些特征是如何定义的？面向对象、函数语言、泛型编程等新型编程模型是否有共通的理论基础？ 本课程将揭示这些问题的答案。
为指导编程语言的设计，研究人员们已经提出了一系列的原理和方法，其中最核心的就是类型理论。 类型声明是现代语言中避免编程错误的一个基本手段，而类型理论解释了一个良好的类型系统应该具有的特征和复杂类型的定义方法。 本课程将围绕类型理论这个核心组织和讲授程序设计语言的现代理论。
本课程具有两个特点：1. 严谨性：课程中的概念元素都将有严格的数学定义，可以进行形式演绎和归纳， 而非空泛的概念介绍。2. 操作性：课程中的所有重要概念都将通过课程作业的方式编程实现，使得同学们在动手过程中真正掌握知识。希望通过本课程的学习，使得同学们在编程语言领域拥有扎实的理论功底和实践能力，在产业方面能胜任设计新语言的任务，在学术方面为开展程序语言相关研究打下基础。
参考书目
Types and Programming Languages, Benjamin C.Pierce, The MIT Press, 2002.（教材）
内容提要
| Class | Date | Topic and Readings | Lecturer |
|---|---|---|---|
| 1 | 19-Feb | Introduction Untyped arithmetic operations |
Zhao |
| 2 | 26-Feb | OCaml | Zhao |
| 3 | 4-Mar | Lambda Calculus Nameless Representation |
Zhao |
| 4 | 11-Mar | Type Basics Simple Typed lambda Calculus Simply Extensions |
Zhao |
| 5 | 18-Mar | Reference | Zhao |
| 6 | 25-Mar | Class Project | Zhao |
| 7 | 1-Apr | Exception | Zhao |
| 8 | 8-Apr | Subtyping Metatheory Subtyping |
Zhao |
| 9 | 15-Apr | Middle Test (+ Check project) | Zhao/Wang |
| 10 | 22-Apr | Case Study: Imperative Objects Case Study: Featherweight Java |
Wang |
| 11 | 29-Apr | May Festival (No class) | / |
| 12 | 6-May | In-class Practice | Wang |
| 13 | 13-May | Recursive Types Metatheory of Recursive Types |
Wang |
| 14 | 20-May | Type Reconstruction Universal Types |
Wang |
| 15 | 27-May | Existential Types | Wang |
| 16 | 3-Jun | Final Presentation | Zhao/Wang |
