因为工作的关系，需要在古老的 Scheme 上实现一个编译到某种 Vectorized statically typed IR 的编译器，其编译过程需要支持 on-demand parameterized polymorphic ，比如 + 这个函数，需要按需实例化为支持向量+常量， 向量+向量， 常量+常量的对应逻辑。这就需要 类型系统支持到 $$ \lambda 2 $$ , 也就是 System F, 在不引入类型标注的情况下，Hindley-Milner 类型系统是最好的选择

在现代语言 Haskell, Rust, TypeScript 中我们均能看到 Hindley-Milner 类型系统 的身影。HM 系统同样可以兼容类型标注作为类型推断的辅助，已经成为大多数有类型函数式语言的类型系统的基础。

Scheme as A static typed language

完全静态是不可能的，因为 Scheme 中的 List 的类型是动态的，List 中的元素可以是任意合法的 Scheme 值

1

'('bar 1 '() (lambda () #f) "foo")

这样的话 List 的元素类型就必须是一个动态类型

但是如果我们只考虑一个 Scheme 的子集，我们就可以在享受 Scheme 的一些优越特性的同时 （如 hygenic macros）, 利用类型系统更容易的写出正确的程序，并且打通和其他静态类型语言的桥梁。

我们做一个很简单的限制： List 和 Vector 的元素类型必须一致。这样 List/Vector 的类型就变成静态的了。我们获得了一个 Scheme 的语义上的子集。

我们目前有了静态类型系统的语义基础，现在我们可以在这个无类型标注的语言上构建一个真正的类型系统了

Scheme as second typed lambda calculus

众所周知，Scheme 可以认为是 lambda 演算用程序语言表达的结果，加上多参数函数，更多的基本类型（数字，字符串，bool 等），REPL 等等feature，

如上节提到， Scheme 实际上和无类型 lambda 演算一样是动态类型，我们考虑给 Scheme 加上一个最简单的静态类型系统，使得 Scheme 的每一个项都有一个确定的类型，根据我们开头提到的，这实际上要求类型系统至少是一个 支持多态的有类型 lambda 演算，也就是 System F ($$\lambda 2$$)

为了从一个简单的地方开始，我们先来看看简单类型 Lambda 演算，他是 $$\lambda 2$$ 的基础

lambda 演算 只有三个简单的语法：

  • Variable $$x$$
  • Abstraction $$(\lambda x.M)$$
  • Application $$(M N)$$

分别代表变量, 常数，抽象（也就是函数），和应用（函数应用）

如果给 LC 加上类型约束，那么自然地，我们会如何规定值的类型呢？

  • 假设变量 $$x$$ 拥有类型 $$\sigma$$, 那么 变量 $$x$$ 拥有类型 $$\sigma$$

  • 如果在某个环境中，已知 $$x$$ 有类型 $$\sigma$$ 可以推导出 $$t$$ 有类型 $$\tau$$

    那么：可以在该环境中构造 lambda 抽象 $$\lambda x.t$$ ，其类型是 $$\sigma \rightarrow \tau$$

  • 如果在特定上下文中，可以推导出 t 有类型 $$\sigma \rightarrow \tau$$ 和 u 有类型 $$\tau$$ 则在同一个上下文中，

    那么：可以推导出表达式 $$t u$$ 有类型 $$\tau$$。这捕获了函数应用的概念。

这三条规则也可以用自然推演（Natural Deduction）的形式定义，即：

$$\frac {x{\mathbin {:}}\sigma \in \Gamma }{\Gamma \vdash x{\mathbin {:}}\sigma }Var$$

$${\frac {\Gamma ,x{\mathbin {:}}\sigma \vdash e{\mathbin {:}}\tau }{\Gamma \vdash (\lambda x{\mathbin {:}}\sigma .~e){\mathbin {:}}(\sigma \to \tau )}}Abs$$

$${\frac {\Gamma \vdash e_{1}{\mathbin {:}}\sigma \to \tau \quad \Gamma \vdash e_{2}{\mathbin {:}}\sigma }{\Gamma \vdash e_{1}~e_{2}{\mathbin {:}}\tau }}App$$

在 Scheme 上实现的话，实际要做的工作就是搞清楚 Scheme 版本的 typing rules。

  • 常数，这个很简单，我们可以直接从 syntax 得到类型
  • 变量绑定，对于语句 (define x y) where $$y:\sigma$$ , 我们得到 $$x: \sigma$$
  • Function Application, 对于表达式 (foo arg2 …), 如果 foo 的类型为 $$A1 A2 … An \rightarrow Ret$$, 那么表达式的类型为 $$Ret$$

到现在为止，好像都没什么问题，直到我们遇到函数定义：

  • Native function，看起来也还好办，只需要库函数自己声明自己的类型就行，但是由于没有多态，目前我们只能指定 如 + 这样的函数类型为 $$Int… \rightarrow Int$$ ，一旦这样声明， + 就不能接受 $$Float$$ 类型的数据了
  • User Defined Function, 对于形如 (lambda (arg1...) ...last) 这样的函数，我们没有足够的信息来确定 arg1 arg2 等参数的类型，因为我们没有引入显式类型标注。但是引入类型标注无疑会导致语言成倍的复杂

怎么办呢？一个自然的想法是，从函数的应用处来反推函数的类型，我们可以假定在函数应用处，所有参数的类型已经确定，那么把参数的类型作为代换，就能推出整个函数体的类型。比如

1
2

(define identity (x) x)
(identity 1)

把 x 用常量 1 代换，而常量 1 具有类型 $$Int$$, 函数体为 x，因此这个函数的应用结果 (identity 1) 的类型也是 $$Int$$，函数 identity 的类型为 $$Int \rightarrow Int$$

很快我们就会发现问题，identity 可能不只有一种类型，他可能是 $$Float \rightarrow Float$$, $$Symbol \rightarrow Symbol$$ … 等等，一个值怎么会有多种类型？然而从 Scheme 的语义看，这完全没有问题，站在解释器的角度，我只不过把参数代换进函数体，得到一个结果而已。

可是到类型系统这里就遇到了灾难，我们发现简单类型 Lambda 演算已经不够用了，我们需要一种描述机制可以描述 id 这样的函数。

在值的世界里，函数参数是一个 $$Variable$$ ，它会在应用的时候被替换成具体值，那么自然的，在在类型世界里，函数参数的类型也可以是一个 $$Variable$$，称为类型变量，在应用的时候，类型变量的值被替换为了具体类型

对于 $$id = \lambda x.x$$ 这样的函数，如果引入类型变量，我们可以这样表示其类型：$$id: \Lambda X.X \rightarrow X $$，这个 大写的 $$\Lambda$$ 就相当于类型世界的 $$\lambda$$

$$id$$ 函数的类型的产生是自然的，不需要依赖别的信息，仅靠函数体就能得到，可以很简单的证明，对于任意 lambda 抽象，我们都能产生这么一个带有类型变量的类型

现在，我们得到了一个带有类型变量的类型，如果这时候没有额外的信息，这个类型实际上就无法”求解“了，也就是无法代换为不含类型变量的具体类型，这些类型变量被称作是 “自由的”

显而易见，我们可以从函数调用处获得这些”额外信息“

值得注意的是，调用处有多个，在每个 id 的 occurrence， id 都是不同的类型，就 符号 id 而言其本身是多态的（Polymorphism）, 但是这种多态是有限的，其范围就是所有的 occurrence。这种有限的多态，正是 Hindley Milner 系统中的核心： Let-Polymorphism

Hindley Milner(以下简称 HM) 在 Lambda Calculus 的语法基础上增加了一条 let 语句

$$ {\begin{array}{lrll}\e&=&x&{\textrm {variable}}\&\vert &e_{1}\ e_{2}&{\textrm {application}}\&\vert &\lambda \ x\ .\ e&{\textrm {abstraction}}\&\vert &{\mathtt {let}}\ x=e_{1}\ {\mathtt {in}}\ e_{2}&\\\end{array}} $$

上面这个公式里的 let 语句就是实现 Let-Polymorphism 的基础，举例来说：

$$\mathtt{let} \ id = \lambda x.x \ \mathtt{in} \ (id\ 3) \ (id \ \mathtt{“text”}) …$$

实际上表达了一个代换过程，这里两个 id 在各自的表达式里分别代换为 $$Int \rightarrow Int$$ 和 $$String \rightarrow String$$。这种 let 形式实质上绕开了多态的问题，也就是说在 HM 系统里，除了 Let 语句，其他地方任然不允许一个identifier有多个类型

这样缺点也很明显：表达起来很繁琐，所有函数的应用点都需要写在 let 语句里。实际上如果一个函数所有可能的调用都是已知的，那么所有调用点的类型都能够确定，我们也不需要拘泥于写出 let … 这样的形式。我们只需要在函数定义的环境里的所有应用都当做是 let 语句的 $$e_2$$ 部分就可以了。

基于 let 语句，我们可以在简单类型 Lambda 演算上增加一条 Rules：LET

$$\frac{\Gamma \vdash e_{0}:\sigma \ \ \ \ \ \ \Gamma,x:\sigma \vdash e_{1}:\tau}{\Gamma \vdash \mathbf{let}\ x= e_{0}\ \mathbf{in}\ e_{1}:\tau}{Let}$$

到了这里，我们已经可以利用静态类型系统来为 无类型 Lambda 演算，或者是 Scheme 来做一些静态类型检查了，举例来说：

假设我们已经知道函数 + 的类型为 $$\Lambda X \rightarrow X \rightarrow X$$ , 对于下面的 scheme 程序：

(define (id (x) x)

(+ 1 (id "a")) ，

我们在全局环境里定义了 id 和 +，因此我们剩下的约束都是在一个全局的 Let 语句里产生的：

$$Let \space \texttt{id} : \Lambda X. X \rightarrow X \ \space\texttt{+} : \Lambda X. X \rightarrow X \rightarrow X $$

我们可以在 parse 的过程中根据语法产生五个显而易见的约束：

$$ Int = X \ typeof \space \texttt {(id “a”)} = X \ typeof \space \texttt{(+ 1 (id “a”)) } = X \ String = Y \ typeof \space \texttt {(id “a”)} = Y $$

这个过程叫做 syntax-direct rules。这些约束都是以等价形式出现的，即等号左边和右边是没有次序的等价关系。

注意，这里出现的所有类型和类型变量都是 mono type，所有重复出现的函数引用都有单独的类型

求解这些约束，我们能得到一个类型错误：表达式 $$\texttt{(id “a”)}$$ 的类型为 $$String$$，而我们又期望表达式 $$\texttt{(id “a”)}$$ 的类型为 $$Int$$。

这些约束的求解过程 (unification) 实际上是一个类型空间上的高斯消元，具体算法有 Algorithm J 和 Algorithm W， 由于相较而言比较好实现，工业上 Algorithm W 用的比较多。

你可以在 wikipedia 上找到关于 Algorithm W 的说明，以及使用 Haskell 实现 algorithm W 的 paper。尽管如此，我还是给出一个简单的算法帮助理解：

  1. 给定一个约束集合 $$S$$, 记其中所有出现的自由变量集合为 $$F = free(S)$$
  2. 根据 $$F$$ 构造一个初始化变量表 $$\textbf{Table} = { var: var | var \in F }$$
  3. 从 $$S$$ 中取一个约束 $$C_i$$, 令 $$S^{\prime} = S - { c_i }$$
  • $$[VAR]$$ 如果 $$c_i$$ 符合形式 $$x_i = \tau$$ 或者 $$\tau = x_i$$,（即约束的任意一边是一个类型变量） 那么
    • 对于剩下的约束，做一个“替换“操作，$$\forall C \in S^{\prime}, subsitude(C,x_i = \tau$$)
    • 对于 $$\textbf{Table}$$ 中对应的变量同样做这个替换操作 $$x_i = \tau$$
  • $$[VAR]$$ 如果 $$c_i$$ 符合形式 $$X_l \rightarrow Y_l = X_r \rightarrow Y_r$$, 那么就产生两个新的约束 $$X_l = X_r$$ 和 $$Y_l = Y_r$$ 加入到 $$S$$ 中 （这里代表了函数的等价约束）

$$ S := S \cup { X_l = X_r, Y_l = Y_r}$$

  • \( [APP] \) 如果 \( c_i \) 符合形式 \( (F \space X) = Y \), 那么该约束转换为 \( F = X \rightarrow Y \), \( S := S \cup { F = X \rightarrow Y } \)
  • \( [ABS|LET] \) 如果 \( c_i \) 符合形式 \( F = \Lambda X. Y \), 这里右边 F 是一个let-polytype， 需要类型参数来确定具体的 monotype 类型。 产生这种形式的约束一般是遇到了函数定义 \( ABS \) 。我们根据上文的 Let-polymorphism知道，所有函数的类型在不同的 occurrence 处是不一样的，因此这条规则接下来的动作是，找到 F 的所有 occurrence ，然后产生恰当的类型参数，得到一个 monotype，这里我们可以直接产生最 general 的类型，即对所有的类型参数都直接生成一个类型变量

$$ \forall Fi \in S^{\prime}, Fi = (F Xi) $$

这是最基本的 Algorithm W 的描述，我们可以增加一些自定义 syntax-directive rule 和 type operator 来补充完整 scheme 的类型系统。比如，为了描述 r7rs 的 vector 类型，我们需要一个类型构造器 $$Vec: \Lambda X_1 X_2… X_n . Vec \space \texttt{of} \space X_1 X_2… X_n$$ , 以及一条生成规则：

$$typeof \texttt{ #(x1 x2 … xn)} = Vec \space \texttt{of} \space X_1 X_2… X_n$$

当然，根据我们的目标， vec 的元素类型需要限定为一致　

$$X_1 = X_2, X_2=X_3, …X_n = X$$　

而 vec 的类型也可以简化为 $$Vec \space \texttt{of} \space X$$

在 unify 的时候，也需要增加一条

  • \( [VAR] \) 如果 $$c_i$$ 符合形式 $$Vec \space \texttt{of} \space X = Vec \space \texttt{of} \space Y$$, 那么就产生n个新的约束加入到 $$S$$ 中 （这里代表了数组的等价约束）

$$S := S \cup { X = Y}$$

题外话：如果在 unification 的时候带上类型约束产生的位置并在求解的时候传递下去，就可以在报类型错误的时候给出正确的定位信息了

Hindley-Milner 的另外两个 Rules，$$GEN$$ 和 $$INST$$，实际上已经隐式包含在 $$ABS$$ 和 $$APP$$ 中了，在 syntax-directive 的过程里不会显式的出现，这里也给出两个 rules 的形式化描述：

$$ \frac{\Gamma \vdash e:\sigma \ \ \ \ \alpha \notin free(\Gamma)}{\Gamma \vdash e:\forall \alpha.\sigma}{GEN} \ \frac{\Gamma \vdash e:\sigma \ \ \ \ \ \sigma \succeq \sigma’}{\Gamma \vdash e:\sigma’}{INST} $$

　

至此，可以说基本完成了一个静态类型 scheme 的框架，基于此我们也实现了 scheme 的一个子集的编译器

后记

我依旧庆幸自己有这么一个机会能在腾讯做这么 Geek 的事情，本文完成时，已经距离我提交离职申请过去5天了。

我相信任何一个熟悉腾讯这家公司的人，都不太相信我能在腾讯写编译器。我曾经也以为，我能干出点不同的事情。然而我忽略了最重要的两点：

  • 作为一家游戏工作室，如何能投入资源帮你做这个编译器项目？
  • 作为一个只有两个人的研发小组，为什么要去负责推广？我们究竟是做一个 Seller 还是 Developer？

Google 的前辈 laike9m 的 blog 有一段话，我很认同

  • 这里仅讨论内部工具项目，不适用于面向外部用户的产品。几年下来我有一个很直接的观察，成功的内部工具基本都是 2c，很少有 2b 的。可能有人会好奇，内部工具也有 2b2c 之说吗？有个很简单判断方法：一个工具或系统，如果工程师能自己用起来，那就是 2c；如果需要部门里 >1 人讨论并决定，那就是 2b。举两个例子：一个开箱即用的任务监控面板是 2c 的，而一个需要修改 release 流程才能使用的工具就是 2b 的。当然，我观察到的样本很少，所以结论未必对。但我真心感觉 2b 的东西想推动，要花费几倍于 2c 工具的时间，效果还未必好。总之如果你有的选，请尽量把时间花在 2c 项目上。

很不幸，Leader 认为我们应该按照 2b 模式去做。 于是我得自己负责宣传，绞尽脑汁想落地，不断推销我们的东西。逐渐的我开始觉得不对劲，这不是就是发生在阿里达摩院的相似的故事吗？我并不否认销售的作用，甚至我很认同，在有朝一日，如果我去创业，或者成为某个大产品/业务的负责人，这些都是我应该考虑的事情，可是无论如何，都不是我现在这个位置和现在拥有的资源所能够考虑的事情

另外还有一点是，也许腾讯做中间件产品太习惯 2b 了，工程师几乎遇不到 ”开箱即用“ 的产品，做什么都习惯拉个群做”客服“，软件质量上的缺陷用这种方式弥补，而不是靠单元测试和issue tracker，久而久之，可能就忘记了外面的世界是什么样

总而言之，在腾讯做技术没有前途，本人待业中，希望有好坑可以联系我~