跳到主要内容

描写类型系统的工具

元语言和对象语言

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

下面,是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>不是一个算术表达式。

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

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

    arr.reduce(callback(accumulator, currentValue[,index[, array]])[, initialValue])
  2. 汉语。我们用汉语谈论JavaScript语法或者TAT的语法的时候,汉语就是元语言,被谈论的语言就是对象语言。在用汉语谈论汉语本身的时候,汉语即是元语言也是对象语言。比如,"形容词"这个术语就是一个元变量。

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

二元关系

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

定义:二元关系

若集合RR满足RS×SR\subseteq S\times S,那么RR就是一个集合SS上的二元关系(Binary Relation)。

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

AABB是两个集合,有

  • 子集(Subset)。若集合AA的所有元素都在集合BB中,我们称AABB的子集,记作ABA\subseteq B
  • 真子集(Proper Subset)。ABA\neq BABA\subseteq B,称AABB的真子集,记作ABA\subset B
例子:二元关系

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

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

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

R:={(n,n+m):nN,mN+}R := \{ (n, n+m) : n\in \N, m\in \N^+ \}
记号
  • :=:= 的意思是“定义为”。它表示将这个左边的表达式定义为右边的表达式。

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

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

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

nn元关系

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

例子:一元关系

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

IsEven:={0,2,4,6}={n:nN,2 Divides n}N\begin{align} \text{IsEven}:=\{0,2,4,6 \dots\}=\{n: n\in \N, 2\ \text{Divides}\ n\} \subset \N \end{align}
例子:二元关系

自然数上的整除关系。

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

xmody=kx\bmod y = k 表示 xxyy 除余 kk

例子:三元关系

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

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

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

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

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


作为二元关系的定型关系

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

t:Tt:T

其中,"::"是一个将项和类型连接的符号。 这里的tt是一个元变量,它指代的是语言中的某一个项;TT也是一个元变量,它指代的是这个语言的类型系统中的一个类型。

备注

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

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

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

例子:水果

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

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

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