描写类型系统的工具
元语言和对象语言
我们可以广义地将一些带有规则的元素称为语言。而我们在研究形式语言的时候,经常需要用另外一种语言描述所研究的那门语言。 研究编程语言时,我们更是经常需要用另外一套记号,来描述编程语言本身。
下面,是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)。
熟悉元语言和元变量
"元语言"和"对象语言"这两个词,只是对于语言在发挥其作用时,所处的地位的描述。
下面是几个元语言的例子。
- 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>
不是一个算术表达式。叫做"变量",是因为它可以被"赋值为"它所指代的任何一个对象语言符号,而不是特定的对象语言符号。
Array.prototype.reduce
语法的描述语言。我们将其语法高亮着色:其中粉色的是元变量,蓝色的是居于辅助地位的元变量。而剩下的是对象语言的符号。arr.reduce(callback(accumulator, currentValue[,index[, array]])[, initialValue])
汉语。我们用汉语谈论JavaScript语法或者TAT的语法的时候,汉语就是元语言,被谈论的语言就是对象语言。在用汉语谈论汉语本身的时候,汉语即是元语言也是对象语言。比如,"形容词"这个术语就是一个元变量。
特别注意:元变量一般会避免取为对象语言中的符号,否则会给读者带来混乱。
二元关系
在刻画集合内的元素之间的关联的时候,关系(Relation)是一个有力的工具。接下来我们定义什么是二元关系,以及对本教程中初次出现的符号给一个说明。
若集合满足,那么就是一个集合上的二元关系(Binary Relation)。
- 元组(Tuple)是若干元素形成的有序结构,可以类比Array或者List或是TypeScript的元组类型。在数学上我们会用括号来表示元组。
- 二元组:表示一个二元组,又称有序对(Pair)。
- 三元组:表示一个三元组。
- 笛卡尔积(Cartesian Product)。表示集合的笛卡尔积运算。
- 2个集合的笛卡尔积:
- 3个集合的笛卡尔积:
若和是两个集合,有
- 子集(Subset)。若集合的所有元素都在集合中,我们称是的子集,记作。
- 真子集(Proper Subset)。 且 ,称是的真子集,记作。
自然数集上的小于关系,即我们通常所知的""。
但是这个列举是不精确的。一个更加精确的定义是:
的意思是“定义为”。它表示将这个左边的表达式定义为右边的表达式。
是 的另外一种写法,也是一种可接受的集合记号。它用 代替了,书写更加方便,我们会全部使用前者。
自然数集上的小于关系, 可以省略地画成这样。
- 可以看到,有小于关系的两个数都有一根有向箭头连接。
- 当我们要说0和1满足关系时,既可以写成,也可以使用中缀的写法,写成。
元关系
一元关系也叫做一元谓词(Predicate)。谓词也可以看成是接受若干个元素,返回true
或者false
的函数。
这个一元关系的具有实际的语义,即是否是偶数:
自然数上的整除关系。
表示 被 除余 。
这是一个三元关系。请读者给它找一个语义:
在本课程中,我们会主要使用二元关系和三元关系。它们是我们刻画项、类型、定型环境之间关系的有力工具。
注意:关系的数学本质仅仅是一个集合。定义哪些元素之间存在关系的时候完全是任意的。不必像我们刚刚看的那些例子一样,非得将每个关系都解释出现实意义不可。
练习:请各举出一个二元关系和四元关系的例子。
作为二元关系的定型关系
如同我们在 TypeScript 中写的那样,类型系统的文献也会将一个项以及这个项的类型的关系,记成一个中缀表达式
其中,""是一个将项和类型连接的符号。 这里的是一个元变量,它指代的是语言中的某一个项;也是一个元变量,它指代的是这个语言的类型系统中的一个类型。
我们喜欢用大写的字母来表示类型,小写的字母表示项。
因为这个关系涉及项和类型两个元素,因此它是一个二元关系。这个关系就是定型关系(Typing Relation)。
我们通常会把定型关系解读为「项是一个类型」。英文:term is of type , 或者说 is a 。
就可以解读为,🍎是一个水果,或者是🍎是一个水果类型的实例。
「水果」可以看成是一个集合,其中包含了一切水果实例。因此我们也可以说