跳到主要内容

俯瞰编程语言：宇宙的层级

宇宙的层级：从字符串宇宙下行​

我们不是在讨论天文学。只是，在讨论某个系统的时候，我们会把这个系统中的一切事物形成的那个搜集，叫做宇宙(Universe)。

在这一节中，我们讨论的东西也可以叫做形式语言意义上的语言。但是，为了加深读者的印象，我仍然决定使用宇宙这个名字。

讨论宇宙及宇宙之间的联系和转化，可以使得我们对我们所研究的东西（类型系统和编程语言）有更深刻的认识。

  • 字符串宇宙。可被一切可枚举的字母表上的所有字符串构成的宇宙；
  • 形式语言宇宙。字符串宇宙中，一切可依据某种形式语言的语法规则产生的字符串构成的宇宙；
  • JavaScript程序宇宙。形式语言宇宙中，可被特定JavaScript语言规范所定义的语法解析的字符串形成的宇宙；
  • 在运行时不会报错的JavaScript程序宇宙；
  • 可被重建出TypeScript类型的JavaScript程序宇宙；
  • ……

宇宙的层级：从常量宇宙上行，有限关系宇宙​

在一开始，我们只有常量可用。我们用常量构建表达式，进行计算。计算都是一次性的，不能够复用。

  • 常量宇宙。比如，1，"test"等等一切常量形成的宇宙。

没过多久，我们开始写真正意义上的程序。

  • 有限关系宇宙。有限关系，指的是关系中的元素是有限的。

    现在，我们可以通过穷尽描写常量之间的对应关系，把计算结果存下来，进行复用。这样，我们就能写有现实意义的程序，比如计算Fibonacci数的程序可以是一个有限的预处理好的表：

F={(0,0),(1,1),(2,1),(3,2),(4,3),(5,5)}F = \{(0,0), (1,1), (2, 1), (3, 2), (4, 3), (5, 5)\}

F(0)F(0)输出00，F(1)F(1)输出11……

这也是一种硬编码。但是，这种描写方式所能处理的关系是有限的。你没法通过这种方式，写一个能够把所有自然数转换为其对应的Fibonacci数的程序。哪怕是只是硬编码0∼1000\sim 100都非常痛苦，而且对一些不在表中的输入，没法动态地计算答案。我们必须往上走。

宇宙的层级：函数宇宙​

于是，我们将常量语言作为对象语言进行扩张，发明了函数语言。

  • 函数宇宙(项宇宙)。为了扩张有限关系宇宙中的每个关系，使得我们能够（在原则上）支持无穷集之间的关系，我们引入了函数来对这种关系做抽象，并且第一次通过在线的计算，而不是去查预处理好的表来得到答案。

我们可以写出

F(0)=0F(1)=1F(x)=F(x−1)+F(x−2)F(0) = 0\\ F(1) = 1\\ F(x) = F(x-1) + F(x-2)

来进行计算。

我们发现函数不够安全。F(−1)F(-1)或者F(‘‘0")F(``0")都会导致这个函数发散（即，计算不出结果，不会停机）。我们需要一个工具来对函数、以及表达式进行约束。

宇宙的层级：类型宇宙​

  • 类型(Type)宇宙。为了得到用以对函数进行约束的工具，我们发明了类型。

    我们可以类型来为常量分类。于是，我们定义了自然数集N\N，整数集Z\Z和实数集R\R，还有字符串集合。字符串集合和数集不相交。

    我们可以用函数类型→\to来描写函数的定义域(Domain)、陪域(Codomain)，对不符合类型的函数体或者函数调用，予以拒绝。

    比如，通过定义FF和加号减号的类型为

    F:N→N,+:N→N→N,−:N→N→NF: \N \to \N, \\ +: \N \to \N \to \N, \\ -: \N \to \N \to \N

    并让减号最后的返回值出现负数时截断为0， 来拒绝不合法的调用。

宇宙的层级：二阶类型宇宙和高阶类型宇宙​

  • 二阶类型(Kind)宇宙。如果把→\to视作是一种在类型宇宙中的函数，接受两个类型参数，返回一个新的类型，那么我们也可以给→\to定义其二阶类型(Kind，没有很好的中文翻译，试译作二阶类型)。

我们再次将类型语言作为对象语言进行扩张，引入新的记号，得到了二阶类型语言。

→ ::∗⇒∗\to\ :: * \Rightarrow *

其中，::::是::的升级版，⇒\Rightarrow是→\to的升级版，一般都只用在高阶类型上面。

  • 三阶类型宇宙(类型的类型的类型宇宙)。构造高阶类型的这个过程可以一直持续下去……但是我们一般只走到二阶类型宇宙为止，更高阶的类型，通常会纳入二阶类型语言的框架中进行描写。

扩展阅读​

如果你想进一步了解λ\lambda-演算...