以下内容摘自 scheme-langserver 的相关文档( https://github.com/ufo5260987423/scheme-langserver/blob/main/doc/analysis/type-inference.cn.md):
包括 Java 和 Typescript 等编程语言都有一个类型系统, 能帮程序员尽可能避免代码执行中的错误。这些系统上基于遵循Hindley-Milner Type System或者System F的一些基本理论构建。然而，艰涩的理论不能保证它们的全知全能。
对 scheme 语言这样一种“非类型语言(untyped language)”，很多类型系统需要的信息并不能够轻易的从代码中找到：
(lambda (a) (+ 1 a))
显然，这段代码无法显式给出参数a的类型。或者说，a的类型是一个包含所有可能类型的全集something ？（后续会说明这是啥）。这是因为 scheme 语言不像许多其他语言一样在字面上给出函数的参数的类型。如果是 Typescript ，为了给a标明类型number：
function(a: number){return 1+a}
许多 scheme 语言的同类（比如 Typed-racket ）会改变它们的语法并且要求像 Typescript 这样的语言一样在字面上给出类型信息。但是，scheme-langserver 认为可能有另外的手段——当下的大多数 scheme 代码都在尽量遵循r6rs标准，这意味着可以依据标准中给出的函数（或者按照 lisp 家族的术语来说，过程）所具有的语义来猜测类型信息。回归上面的那段 scheme 代码，我们有如下推导：
[ol]
[/ol]
这个推导过程将帮助 scheme-langserver 找到隐含的类型信息并给出类型推导结果。本文将从如下几个反面进行介绍：
[ol]
[/ol]
类型表达式
让我们首先考虑字面量的类型判断，以下分为四种简单的情况：
[ol]
[/ol]
此外，上文讨论的这些判断器当然是 r6rs 中的标准判断器，然而我们不能保证在任意代码中它们不会撞上“真假美猴王”。因此，scheme-langserver 使用identifier-references来表示上面这些判断器，带上它们的上下文信息；并使用函数construct-type-expression-with-meta构建他们。
从代码中收集类型信息
Lambda 算式
在 scheme-langserver 的处理过程中，所有的代码通过一整套索引系统管理：代码文件被表示为document，其中的代码被解析为index-node。至此，一种工程上的直觉告诉我们，应当从这一套索引中收集类型相关的信息，为接下来的推导打基础。显然，这一步最困难的事情在于如何从字面量所给出的简单信息，一路火花带闪电，给出那些更为复合的信息。
前人在这个问题上已经水了很多论文，他们大多数用 lambda 算式的那一套理论摇唇鼓舌：说来说去就一件事，不论怎样形式的代码都可以转化为 lambda 算式那种形式的代码。本文不会在这里介绍什么$\alpha$转换，$\beta$规约。在这个小节，本文只介绍如下两个案例：
[ol]
[/ol]
function (){
var a = 2;
return a+1;
};
//=================>
//可以转换为
function (){
return (function(a){return a+1;})(2);
};
其中2是一个字面量，按照上文的讲法，把它的类型信息number?传给了变量a。
[ol]
[/ol]
在此基础上，收集信息的工作仍然有很长的路线要走，因为：
[ol]
[/ol]
扩展类型表达式
上文我们多次提到了这样几个概念“复合”、“复杂”、“多个不同部分”，它们实际上都指向了如下三个事实：
[ol]
[/ol]
基于数学的一般原则，scheme-langserver 引入了variable。它会在收集类型信息的过程中占住identifier-reference在类型表达式里面的位置，这样就方便后面进行进一步的逻辑运算和推导。
逻辑运算和推导
Hindley-Milner 类型系统
虽然 lambda 算式和我们的那些规则已经指出了类型信息应该如何在代码的结构框架上传递。但是，从字面量到变量，从 r6rs 标准到自定义的代码，仍然有大量琐碎的逻辑运算和推导工作要做。这里就存在一个问题，即如何利用这些信息做燃料驱动一台引擎，这台引擎将吞食上述信息并突出我们想要的那些未知的类型信息。Hindley-Milner 类型系统描述的就是如何在 lambda 算式基础上做这些工作。它总结了如下几条规则：
[ol]
Variable Access
$$ \frac{(x:\sigma) \in \Gamma}{\Gamma \vdash (x:\sigma)} $$
这一条说的是，如果横线上方的变量$x$已知类型$\sigma$，那么横线下方的逻辑运算成立：即遇到$x$类型系统就能够给出它的类型$\sigma$。这里$\Gamma$可以看做一台无情的机器，虽然上述逻辑运算很愚蠢，但是它仍然会忠诚的执行。$\in$实质上代表了一种扩展机器的知识库的行为——在这条推导规则中，它把$(x:\sigma)$塞进知识库。然后，$\vdash$指向$\Gamma$机械运算的结果。
Application
$$\frac{\Gamma \vdash (e_1:(\tau_1 \to \tau_2)) \quad\quad \Gamma \vdash (e_2 : \tau_1) }{\Gamma \vdash ((e_1\ e_2) : \tau_2)}$$
本规则经常用于函数的调用，如将函数e1用于参数e2——(e1 e2) （类似(+ 1 a)）——然后获得这个表达式的返回值的类型$\tau_2$。相关实现可以在application.sls中研究。注意，这里的$\to$就是上文中的，只是方向相反而已。
Abstract
$$\frac{(\Gamma, ;(x:\tau_1)) \vdash (e:\tau_2)}{\Gamma \vdash ((\lambda\ x\ .\ e) : (\tau_1 \to \tau_2))} $$
本规则用于获得函数如(lambda (x) (+ 1 x))的类型。如果一个函数$e$的参数$x$已知类型$\tau_1$，返回值类型$\tau_2$，则函数的类型为$\tau_1 \to \tau_2$。在 scheme-langserver 中，这个类型表示为(tau1 。
Let
$$\frac{\Gamma \vdash (e_1:\sigma) \quad\quad (\Gamma,,(x:\sigma)) \vdash (e_2:\tau)}{\Gamma \vdash ((\mathtt{let}\ (x = e_1)\ \mathtt{in}\ e_2) : \tau)} $$
已知：表达式$e_1$具有类型$\sigma$；当变量$x$具有类型$\sigma$，函数$e_2$具有类型$\tau$。将$e_1$代入$e_2$表达式中的$x$，返回值类型仍然是$\tau$。
Subtype
$$\frac{\Gamma \vdash (e: \sigma_1) \quad\quad \sigma_1 \sqsubseteq \sigma_2}{\Gamma \vdash (e : \sigma_2)}$$
这条规则说的是如果$e$有类型$\sigma_1$，且$\sigma_1$是$\sigma_2$的一个子集（或者说$\sigma_1$继承了$\sigma_2$，$e$也将具有类型$\sigma_2$。
Type Generalize
$$\frac{\Gamma \vdash (e: \sigma) \quad\quad \alpha \notin \mathtt{free}(\Gamma)}{\Gamma \vdash (e:(\forall\ \alpha\ .\ \sigma))}$$
这一条规则用来拓展$\Gamma$关于类型的知识（在 scheme 语言中，大多用于解析 record type ）。它呈现的逻辑是：若已知某类型变量$\alpha$“不自由”，且某表达式$e$有类型$\sigma$，则$e$同时可能有类型$\alpha$。其中$\alpha$是$\sigma$的任意子集。这一条规则实际上是 Subtype 的反演——“不自由”说的是在知识库中，存在一些变量具有$\alpha$这个类型，因此我们可以在横线下方一一枚举$\alpha$，看它们是否满足这个判断。有的读者可能对“不自由”和“枚举”没有清晰的认识：它本质上反映的是“排中律”的取消，即“两个互相矛盾的命题必有一真”，这个类似反证法的逻辑不一定成立。因为你必须把矛盾中的一个方面一一列举，才能证明其中一个是真的。对于本规则而言，一一列举“不自由”的$\alpha$在逻辑运算上比较经济实惠。
[/ol]
实现$\Gamma$ 机的工程直觉
[ol]
[/ol]
Unification 机制
首先总结上文，$\Gamma$机是一台吞下用index-node表示的静态代码，然后转化成类型表达式的机器。这里面就有一个算法来推导类型表达式里面啊那些未知量。在 scheme-langserver 中，我们的代码采用了 Robinson's Unification Algorithm：$\Gamma$机像蜘蛛一样在图数据构成的网上面爬来爬去，把$:$和$\sqsubseteq$传递的已知信息传递给未知量。在这个过程中，scheme-langserver 采用了 path-memory 和循环检测机制防止死循环。整个机制的细节总结如下:
[ol]
[/ol]
Gradual Typing 和隐式变换
正如本文开头那个例子(lambda (a) (+ 1 a))指出的，参数a没有被显式标注类型，这就导致 Hindley-Milner 类型系统中的很多等价代换无法发挥作用。Scheme-langserver 使用Gradual Typing做了一个隐式变换：+ 只接受有number?类型的参数，那a就等于被标注number?类型了嘛。
但是，正如 Gradual Typing 作者 Jeremy Siek 所言（作者默默吐槽，其实没看他的论文前，我也发现了这个方法），这种隐式变换将破坏 subtype 规则。这是因为这种变换的前提是假设代码总是能够执行。不过在我看来，总是要有一点妥协的，关键看 scheme-langserver 能否根据类型推断的结果给出有价值的信息。
TODO: 用类型推断给出代码的诊断信息
