极道
·
如何阅读类型系统符号？
💡
原文中文，约1500字，阅读约需4分钟。
📝
内容提要
对于对类型系统和类型理论感兴趣的人来说，他们第一次接触文献时会看到一些复杂的语法，但实际上相当简单。基本思想来自形式逻辑，整个表达式是一个蕴涵，上半部分是假设，下半部分是结果。了解这些符号后，可以理解如何使用规则来计算表达式的类型。规则包括应用、函数、let语句、子类型和类型泛化。通过递归应用规则，可以得到表达式类型的证明。这些规则精确地说明了如何找出表达式的类型。
🎯
关键要点
- 类型系统和类型理论的基本思想源自形式逻辑，表达式是一个蕴涵，上半部分是假设，下半部分是结果。
- 符号 Γ 代表上下文，⊢ 表示可以证明的内容，x : σ 表示 x 的类型是 σ。
- 如果 x 在上下文 Γ 中具有类型 σ，则可以得出 Γ ⊢ x : σ。
- 规则 [App] 说明如何将函数应用于值以获得类型。
- let 语句的规则说明如何处理局部绑定。
- Inst] 规则处理子类型，表示子类型的值也可以被视为父类型。
- 类型泛化规则说明如果变量在上下文中没有自由，则可以确定表达式的类型。
- 使用这些规则可以计算表达式的类型，通过递归应用规则直到完成证明树。
- 这些规则精确地说明了如何找出表达式的类型，类似于 Prolog 中的证明树计算。
➡️
