RustTyC

RustTyC 是一个将类型规则转换为 Rust 的简单接口，并执行类型检查过程以生成类型表。

TL;DR

• 从 crates.io 添加依赖项。
• 查看 文档。
• 在我的 博客 上介绍类型格子和推理规则的基本知识。

什么是 RustTyC？

RustTyC 提供了一个接口，允许将基于类似 Hindley-Milner 的有界类型半格的推理规则直观地转换为 Rust 代码。

用法

第一步也是最重要的一步是，将依赖项添加到您的 Cargo.toml 中。

rusttyc = "0.4.*"

接下来，让我们谈谈数据结构。我假设您已经有了某些代码数据结构，用于表示您想要进行类型检查的程序。我们可以称之为 AST。然后，您需要一些类型的表示，我们将其称为 AbsTy。这很可能是一个枚举，列出了值可能具有的所有可能类型，包括未解析的类型（Top/Unconstrained/Infer）、抽象类型（Numeric）和递归类型（Option(Box<AbsTy>) 或 Either(Box<AbsTy>, Box<AbsTy>)）。

要获得晶格结构，请实现 rusttyc::Variant 类型。这需要您实现三个函数并提供相关的错误类型（Variant::Err）。在到达实现的精髓之前（你看到了我在那里做了什么吗？），让我们先看看简单的函数：提供类型晶格的顶层元素的 Variant::top()，以及提供特定类型算子的 Variant::arity(&self) -> Arity。算子可以取 Arity::Variable 或 Arity::Fixed(usize)。这里没有什么特别令人兴奋的。最后，还有一个 Variant::meet(Partial<Self>, Partial<Self>) -> Result<Partial<Self>, Self::Err> 函数。如果你暂时忘记了 Partial 的事情，这个函数正是我们所期望的：它接受两个抽象类型，并按照类型晶格的规则提供一个新的类型。如果两个类型不兼容，它将返回一个包含一些调试信息的错误。请注意，类型检查器将丰富错误信息，以便更容易跟踪，从而产生一个 TcErr。如果你好奇，可以看看它的文档。那么，Partial 是什么呢？Partial 是 Variant 和相应类型的最小子代数数量的组合。例如，数值类型通常没有子代。因此，当它被 Partial 包裹时，它的 Partial::least_arity 总是 0。然而，元组类型的情形则完全不同。假设一个变量代表一个九元组（9-tuple），但类型推理只推断出在位置 0、3 和 4 将有一个子代。在这种情况下，它的 Partial::least_arity 将是 5（回忆：索引 4 占位表示至少有 5 个元素）。类似地，如果类型是顶层变体，它可能解析为元组或选项，因此它的算子只能是一个下界。

现在要做的是开始收集约束。在你的代码中，使用 rusttyc::TypeChecker::new() 创建一个新的类型检查器，并遍历你的抽象语法树（AST）。对于AST中的每个节点，创建一个 rusttyc::TcKey 并对其施加一系列约束。键代表AST中的节点（无论是什么）或变量。变量的特殊之处在于它们可能在AST中出现多次并引用同一对象。有几种方法可以处理这个挑战，其中最简单的方法是让类型检查器来处理。为此，调用 TypeChecker::get_var_key(&mut self, var: Var) -> TcKey 函数。使用相同的变量多次调用此函数将返回相同的键；方便起见。

假设AST是代码 c := a + 3 的树表示。您将想要通过递归调用 tc_ast 函数来遍历树。假设 tc 是类型检查器，该函数返回一个 Result<TcKey, TcErr<AbsTy>>，其中键包含节点的类型。我们将从底部到顶部讨论节点。第一个节点是变量 a。这里没有太多要做的事情，只需为 a 获取一个键并返回它： Ok(tc.get_var_key(var))。接下来是整数字面量 3。假设这样的字面量应将值绑定到类型 AbsTy::Unsigned。因此，使用

let key = tc.new_term_key();  // Generate a fresh key.
tc.impose(key.more_conc_than_explicit(AbsTy::Unsigned))?;  // Set an explicit abstract type as bound for `key`.
Ok(key)

现在是最有趣的部分：执行加法。思路是递归地检查两个子项，遇到它们的类型，并返回结果。

let left = tc_expr(&mut tc, lhs);
let right = tc_expr(&mut tc, rhs);
let key = tc.new_term_key();
tc.impose(key.is_meet_of(left, right))?;
Ok(key)

嗯，这比预期的简单，对吧？

让我们通过赋值来结束。为此，我们递归地检查表达式，检索 c 的键，并将其与表达式的结果相等。

let res = tc_expr(rhs);
let key = tc.get_var_key(lhs);
tc.impose(lhs.is_sym_meet_of(key))?;
Ok(key)

到此为止！通过生成类型表来检索整个过程的输出。

let type_table = tc.type_check()?;

(A-)对称关系

需要注意的一点是，类型关系类似于友谊：有些是对称的，有些则不是。只要每个人都意识到这一点，就没有问题。因此，RustTyc 提供了强制实施这两种关系的方法。两个键 k 和 k' 之间的对称关系意味着一个键的细化也会细化另一个键。假设 k 与 k' 之间存在非对称关系，例如 k 比更具体。在这种情况下，细化 k' 的类型意味着 k 的细化，但反之则不然。常规的交集（TcKey::is_meet_of(...)）本质上是非对称的，其对称对应物是 TcKey::is_sym_meet_of(...)。