如何阅读类型系统符号？

如何阅读类型系统符号？

对于许多对类型系统和类型理论感兴趣的人来说，他们第一次接触文献时会看到以下内容：

这种语法虽然看起来很复杂，但实际上相当简单。

基本思想来自形式逻辑：整个表达式是一个蕴涵implication ，上半部分是假设，下半部分是结果。(上下文)

也就是说，如果上部表达式为真，则可以得出结论底部表达式也为真。

符号
另一件需要记住的事情是，有些字母具有传统含义；有些字母具有传统含义。特别是， Γ 代表你所处的“上下文”——也就是说，你所看到的其他事物的类型是什么。

⊢ 符号的基本意思是你能证明什么。因此，Γ ⊢ ......就是 "我能在上下文Γ中证明...... "的语句。这些陈述也称为类型判断。

还有一点要记住：在数学中，就像 ML 和 Scala 一样，x : σ 表示 x 的类型是 σ。

理解图中符号意义
因此，知道了这一点，第一个表达式就变得容易理解了：如果我们知道 x : σ ∈ Γ（也就是说，x 在某种上下文 Γ 中具有某种类型 σ），那么我们就知道 Γ ⊢ x : σ（也就是说，在 Γ 中，x 具有类型 σ）。因此，这其实并没有告诉你什么超级有趣的事情；它只是告诉你如何使用上下文。

其他规则也很简单。例如，以 [App] 为例。这条规则有两个条件：e₀ 是一个从某种类型 τ 到某种类型 τ' 的函数；e₁ 是一个 τ 类型的值。现在你知道了将 e₀ 应用到 e₁ 会得到什么类型！希望这不是一个惊喜:).

下一条规则有更多新语法。因此，如果我们知道变量 x 的类型是 τ，表达式 e 的类型是 τ'，我们也就知道了接收 x 并返回 e 的函数的类型。

下一条只是告诉你如何处理 let 语句。如果你知道某个表达式 e₁ 的类型是 τ，只要 x 的类型是 σ，那么局部绑定 x 到类型为 σ 的值的 let 表达式将使 e₁ 的类型是 τ！

Inst] 规则处理子类型。它说，如果你有一个 σ' 类型的值，并且它是σ 的子类型（⊑ 表示部分排序关系），那么该表达式也是σ 类型的。

最后一条规则涉及类型的泛化。这条规则的意思是，如果有某个变量 α 在你的上下文中没有 "free"，那么可以肯定地说，你所知道的任何表达式的类型 e : σ 对于 α 的任何值都将具有该类型。

如何使用规则
既然你已经理解了这些符号，那么该如何使用这些规则呢？嗯，你可以用这些规则来计算各种值的类型。要做到这一点，请查看你的表达式（例如 f x y），然后找到一条结论（底部部分）与你的语句相匹配的规则。我们把你要找的东西称为 "目标"。在这种情况下，你要找的是以 e₀ e₁ 结尾的规则。找到这条规则后，你现在就必须找到证明这条规则线以上所有内容的规则。这些内容通常与子表达式的类型相对应，所以你基本上是在递归表达式的部分内容。这样做直到完成证明树，从而得到表达式类型的证明。

因此，这些规则所做的就是精确地--以通常的数学迂腐细节:P--说明如何找出表达式的类型。

现在，如果你用过 Prolog，这听起来应该很熟悉--你基本上是在像人类的 Prolog 解释器一样计算证明树。Prolog 被称为 "逻辑编程 "是有原因的！这一点也很重要，因为我第一次接触 H-M 推理算法就是在 Prolog 中实现的。这其实简单得出奇，而且让人一目了然。你当然应该试试。