描写类型系统的工具

元语言和对象语言

我们可以广义地将一些带有规则的元素称为语言。而我们在研究形式语言的时候，经常需要用另外一种语言描述所研究的那门语言。 研究编程语言时，我们更是经常需要用另外一套记号，来描述编程语言本身。

下面，是MDN上关于JavaScript中Array.prototype.reduce的语法的描述。

arr.reduce(callback(accumulator, currentValue[, index[, array]])[, initialValue])

下面这些记号，都不是JavaScript的一部分，而只是起到了描述语法模式的作用：

• arr, callback, accumulator, currentValue, index, array, initialValue；
• 用来表示可选的[]，以及callback中用来表示函数参数的()。

之所以说它是模式描述，是因为我们在真实调用的时候，不一定非得传入完全相同的名字的参数，只要匹配上了这个模式就行。比如，这样也是完全可以的：

[1, 2, 3].reduce((acc, cur, ind) => acc + cur + ind, -1);

像这样用来描述一种语言的语言，是元语言(Meta Language)。被描述的语言，则是对象语言(Object Language)。

熟悉元语言和元变量

"元语言"和"对象语言"这两个词，只是对于语言在发挥其作用时，所处的地位的描述。

下面是几个元语言的例子。

1. BNF(Backus-Naur Form，或Backus Normal Form)。 BNF是一种上下文无关的形式语言，它可以用来描写任何一种上下文无关语言的语法——包括它自己。

下面，我们用BNF定义了简单的算术表达式语言。此时BNF是元语言，被刻画的算术表达式语言是对象语言。

<Digit> ::= "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"
<Expr>  ::= <Expr> "-" <Expr> | <Expr> "+" <Expr> | "(" <Expr> ")" | <Digit>

0, 1+2, (1+2), 1-(2-3), (1-2)-3都是合法的表达式。

像<Digit>和<Expr>这样的，能指代一系列对象语言符号中的元语言符号，也被称为元变量(Meta Variable)或者非终止符(Nonterminal)。

• 带有"元"这个前缀，是因为它不存在于对象语言之中，而存在于元语言中。<Digit>不是一个算术表达式。

• 叫做"变量"，是因为它可以被"赋值为"它所指代的任何一个对象语言符号，而不是特定的对象语言符号。

2. Array.prototype.reduce语法的描述语言。我们将其语法高亮着色：其中粉色的是元变量，蓝色的是居于辅助地位的元变量。而剩下的是对象语言的符号。

   arr.reduce(callback(accumulator, currentValue[,index[, array]])[, initialValue])

3. 汉语。我们用汉语谈论JavaScript语法或者TAT的语法的时候，汉语就是元语言，被谈论的语言就是对象语言。在用汉语谈论汉语本身的时候，汉语即是元语言也是对象语言。比如，"形容词"这个术语就是一个元变量。

特别注意：元变量一般会避免取为对象语言中的符号，否则会给读者带来混乱。

二元关系

在刻画集合内的元素之间的关联的时候，关系(Relation)是一个有力的工具。接下来我们定义什么是二元关系，以及对本教程中初次出现的符号给一个说明。

定义：二元关系

若集合$R$满足$R\subseteq S\times S$，那么$R$就是一个集合$S$上的二元关系(Binary Relation)。

记号

• 元组(Tuple)是若干元素形成的有序结构，可以类比Array或者List或是TypeScript的元组类型。在数学上我们会用括号来表示元组。
  • 二元组：$(a, b)$表示一个二元组，又称有序对(Pair)。
  • 三元组：$(a, b, c)$表示一个三元组。
• 笛卡尔积(Cartesian Product)。$\times$表示集合的笛卡尔积运算。
  • 2个集合的笛卡尔积：$\{1, 2\}\times \{a, b\} = \{(1, a), (2, a), (1, b), (2, b)\}$
  • 3个集合的笛卡尔积：$\{1, 2\}\times \{a, b\} \times \{'0'\} = \{(1, a, '0'), (2, a, '0'), (1, b, '0'), (2, b, '0')\}$

若$A$和$B$是两个集合，有

• 子集(Subset)。若集合$A$的所有元素都在集合$B$中，我们称$A$是$B$的子集，记作$A\subseteq B$。
• 真子集(Proper Subset)。$A\neq B$ 且 $A\subseteq B$，称$A$是$B$的真子集，记作$A\subset B$。

例子：二元关系

自然数集$\N$上的小于关系$R$，即我们通常所知的"$<$"。

$$R := \{(0, 1), (0, 2), \dots, (1, 2), \dots \}$$

但是这个列举是不精确的。一个更加精确的定义是：

$$R := \{ (n, n+m) : n\in \N, m\in \N^+ \}$$

记号

• $:=$ 的意思是“定义为”。它表示将这个左边的表达式定义为右边的表达式。

• $\{ n : n\in \N \}$是 $\{n\mid n\in \N\}$的另外一种写法，也是一种可接受的集合记号。它用 $:$ 代替了$\mid$，书写更加方便，我们会全部使用前者。

自然数集上的小于关系，$R := \{ (n, n+m) : n\in \N, m\in \N^+ \}$ 可以省略地画成这样。

1. 可以看到，有小于关系的两个数$x, y$都有一根有向箭头连接。
2. 当我们要说0和1满足关系$R$时，既可以写成$(0, 1)\in R$，也可以使用中缀的写法，写成$0R1$。

$n$元关系

一元关系也叫做一元谓词(Predicate)。谓词也可以看成是接受若干个元素，返回true或者false的函数。

例子：一元关系

这个一元关系的具有实际的语义，即是否是偶数：

$$\begin{align} \text{IsEven}:=\{0,2,4,6 \dots\}=\{n: n\in \N, 2\ \text{Divides}\ n\} \subset \N \end{align}$$

例子：二元关系

自然数上的整除关系。

$$\text{Divides} := \{ (n, m) : n\in \N^+, m\in \N, m\bmod n = 0 \}，其中$$

$x\bmod y = k$ 表示 $x$ 被 $y$ 除余 $k$。

例子：三元关系

这是一个三元关系。请读者给它找一个语义：

$$\text{ASCII} := \{(\texttt{A}, 65, \text{0x41}), (\texttt{B}, 66, \text{0x42}),\dots \} \subset \text{Letter}\times \Z \times \text{HexNumber}$$

在本课程中，我们会主要使用二元关系和三元关系。它们是我们刻画项、类型、定型环境之间关系的有力工具。

注意：关系的数学本质仅仅是一个集合。定义哪些元素之间存在关系的时候完全是任意的。不必像我们刚刚看的那些例子一样，非得将每个关系都解释出现实意义不可。

练习：请各举出一个二元关系和四元关系的例子。

---

作为二元关系的定型关系

如同我们在 TypeScript 中写的那样，类型系统的文献也会将一个项$t$以及这个项的类型$T$的关系，记成一个中缀表达式

$$t:T$$

其中，"$:$"是一个将项和类型连接的符号。 这里的$t$是一个元变量，它指代的是语言中的某一个项；$T$也是一个元变量，它指代的是这个语言的类型系统中的一个类型。

备注

我们喜欢用大写的字母来表示类型，小写的字母表示项。

因为这个关系涉及项和类型两个元素，因此它是一个二元关系。这个关系就是定型关系(Typing Relation)。

我们通常会把定型关系解读为「项$t$是一个类型$T$」。英文：term $t$ is of type $T$, 或者说 $t$ is a $T$。

例子：水果

$\text{🍎}: 水果$就可以解读为，🍎是一个水果，或者是🍎是一个水果类型的实例。

「水果」可以看成是一个集合，其中包含了一切水果实例。因此我们也可以说

$$\text{🍎} \in \text{水果}$$