当我们在谈论编程语言的时候我们在谈论什么

阅读注意事项:本文将会使用作者自行维护的《类型论中文术语翻译表》。 截止 2020 年,类型论相关中文术语依然非常混乱。由于这个学科尚未像集合论、分析、代数等学科一样成为主流, 因此翻译尚有改进的可能。作者将从 2021 年开始自行采用这个术语翻译表进行类型论相关讨论,并尽可能地宣传这个翻译表。

PLCT 的首次公开分享。前置知识:

我们从这个问题开始:如何『精通』一门编程语言?或许你会认为『能实现它的编译器』就是对这门语言的精通了。这个回答我认为是合理的(相关讨论见 https://www.zhihu.com/question/349737758/answer/851524909),但是它却是一个不完整的论证——因为我们根本就没有定义什么是『编程语言』,于是也就无从谈起实现的编译器的依据。在讨论一个编程语言的时候,我们往往会讨论它的文法,那么除此之外还有什么呢?或者说,一门『编程语言』比起一颗『语法树』多了什么?

实际上你在讨论很多门相对独立的语言

这些独立的语言其实是可以在语言之间互相交换的,比如 Rust 的那套 mod, use 的系统完全可以和 Kotlin 的 package, import 的系统互换,编程语言的表达力不会受到影响(或者说是管理模块的表达力与模块语言绑定,理论上对于一个语言来说是可插拔的)。

部分语言的类型语言也可以互换,也不会影响表达力。一个更加广为人知的例子是 C 语言的宏被用于 Haskell 预处理。

而往往现在的工业人在设计、实现编程语言的时候,却认为这些不同的语言是不同的——他们往往会重新设计一个语言里所有的组件。因为一些技术原因,复用一个编程语言的某些子语言相对来说比较困难,但是某些技术已经实现了不同编程语言之间的『语言特性』的复用。

我们往往最为关心表达式语言,因为我们的逻辑与计算都是在这个语言里进行的。

类型系统以规范程序

符合语法树定义的代码往往并不都是我们想要的代码,比如 1()。我们通过给表达式以『类型』来规范表达式,来规定如何构造合法的表达式。

类型是一门编程语言中非常重要的组成部分,因为我们关心表达式语言,而类型和表达式语言的相关度比起其他语言都要高。

表达式语言往往是个很庞大的语言,而类型是一种有效的给表达式语言分类的手段。类型会对表达式分类是因为它本身的设计目的——拥有相同类型的表达式在代码里是可以『互换』的,而这种『满足类型的要求的程序』符合的这个『满足类型的要求』的性质叫做良类型的的程序。相同类型的表达式互换不影响良类型性。

类型对表达式的分类方式并不是『同类型的表达式被分为一类』,这样讨论的是所有的程序和所有的类型, 而程序可以有无限个、类型在大部分类型系统里面也有无限个。数学上讨论无限大的对象的时候往往会涉及对这个对象的结构找有限的、被重复的规律,所以我们这里也对程序找规律。

我们『构造』程序和类型的手段却是有限的——比如在 C 语言里面,那些值类型本身就是一些类型(有限个),然后我们可以用结构体、union、数组、指针等功能从已有的类型构造新类型。我们仅有这些手段——我们可以说所有的类型都是由这些方法互相缝合构造出来的,而且这些手段是有限的。同样的,构造程序的手段也是有限的。描述表达式的 BNF 就只有有限个分支。

我们根据这有限个构造类型的手段对有限个构造程序的手段进行分类。对于任何类型(比如 int)或者构造类型的『形式』(比如指针),我们都会有对它的实例的构造以及对它实例的使用。构造的例子比如(叫做构造规则):

使用的例子比如(叫做消去规则):

用这样的方法,可以概况大部分编程语言里所有的程序。这种讨论方式也有一些例外,比如我说『C++ 有依值类型』因为『模板参数可以带值』,但是实际上我们此处只讨论了『构造类型』的过程——我们可以通过模板构造函数类型,而模板支持值。但是只看类型当然很美好,如果我们去观察这些类型的实例的构造方式,就会发现模板函数在被构造的时候不会有任何类型检查、递归的时候传入不同的值参数可能会导致无限实例化,因此我们构造出来的模板函数的实例并不是可以互相替换的(类型相同的函数并不能互换,因为它们在被使用的时候需要进行额外的类型检查),所以 C++ 的类型系统并不适合用这种方式讨论。

同样地,用这种方式思考程序有助于加深对编程语言的理解,因为我们是站在最高的层次思考『所有可能被构造出来的程序』的。这里要提一下 (simply typed) lambda calculus 这个编程语言,它里面的每个类型对应的构造和使用规则区分得都很开,每个功能都非常独立,我自己是很喜欢的。

Encode: 如果我们能用 A 类型及其构造、消去规则去实现出 B 类型的构造、消去规则,那我们可以说 A 是一个比 B 更 general 的类型,然后这个『实现』的过程我们称之为『encode』。

语义以解释程序

『你每天面对这些代码,你很开心吗?』——杨超越

我们在面对代码里的表达式的时候,除了它们的类型还会思考什么呢?类型是一个在进行一遍检查后就不再有用的东西。我们当然会关心这些程序的『含义』的。我们可以说『语义』是这些程序的『执行方式』,比如函数调用的语义就是把函数体的语义拿出来,然后把里面的形参换成实参,然后这个函数体的语义就是这个函数调用的语义。我们也可以说这个编程语言实际上是某个更基础的语言的『高级语言形式』,比如我们也可以用『讨论翻译出汇编的方式』来讨论 C 程序的语义。

比如我有一个 f(a),那么它的语义就是(首先 f 需要是一个有函数体的函数,而且只能有一个参数,这个参数的类型和表达式 a 的类型相同)『f 的函数体』中『所有对参数的引用』全部换成 a 的语义后得到的一坨也是表达式的东西的语义。

事实上,这分别就对应着解释型语言和编译型语言。这么一讲是不是感觉和常见的编译原理知识联系到一起了?

这两种方式分别叫做『操作语义』和『指称语义』,是两种研究语义的思路。而研究语义的具体手法又有许多,我自己比较喜欢的是一种介于操作语义和指称语义之间的手法,叫做『范畴语义』,它通过把编程语言里的构造解释为某个预层里的对象、态射和自然变换的方式来解释程序。

如何描述类型系统

此处插入这篇文章的内容。

例子:函数类型,我们首先定义类型的类型 $\mathcal U$,我们说在上下文 $\Gamma$ 中,$A$ 是合法的类型当且仅当 $\Gamma \vdash A :\mathcal U$。然后我们可以定义 $\N$ 和函数类型(形成规则): \(\cfrac{}{\Gamma\vdash \N :\mathcal U} \quad \cfrac{\Gamma \vdash A : \mathcal U \quad \Gamma \vdash B:\mathcal U}{\Gamma \vdash A\to B :\mathcal U}\)

构造的规则就是: \(\cfrac{}{\Gamma\vdash 0:\N} \quad \cfrac{\Gamma \vdash a:\N}{\Gamma\vdash s~a:\N} \quad \cfrac{\Gamma,a:A \vdash b:B}{\Gamma\vdash \lambda a.b:A\to B}\)

消去的规则就是: \(\cfrac{\Gamma \vdash a:\N \quad \Gamma \vdash b:\N}{\Gamma \vdash a+b:\N \quad \Gamma \vdash a\times b:\N \quad \cdots} \quad \cfrac{\Gamma \vdash f:A \to B \quad \Gamma \vdash a : A}{\Gamma \vdash f(a) : B}\)