haskell - Hindley-Milner 算法 : using types to ensure bindings are applied

Question

我正在按照 Mark Jones 的教程实现 Hindley-Milner 类型推理算法和 Oleg Kiselyov .这两个都有一个“应用绑定(bind)”操作，其类型大致为

applyBindings :: TyEnv -> Type -> Type

这适用 tyvar -> ty TyEnv 中的绑定(bind)到给定的 Type .我发现在我的代码中忘记调用 applyBindings 是一个常见错误。 ，并且我没有从 Haskell 的类型系统中得到任何帮助，因为 ty与 applyBindings tyenv ty 具有相同的类型.我正在寻找一种在类型系统中强制执行以下不变量的方法:

when doing type inference, bindings must be applied before returning a 'final' result

在对单态对象语言进行类型推断时，有一种自然的方式来强制执行这一点，如 wren ng thornton 的 unification-fd package 中所实现的。 : 我们为 Type 定义了两种数据类型年代:

-- | Types not containing unification variables
type Type = ...          -- (Fix TypeF) in wren's package

-- | Types possibly containing unification variables
type MutType = ...       -- (MutTerm IntVar TypeF) in wren's package

并给 applyBindings类型

-- | Apply all bindings, returning Nothing if there are still free variables
-- otherwise just
applyBindings :: TyEnv -> MutType -> Maybe Type

(这个函数实际上是 freeze . applyBindings 在 unification-fd 中)。这会强制执行我们的不变量 - 如果我们忘记 applyBindings ，那么我们会得到一个类型错误。

这是我正在寻找的解决方案，但对于具有多态性的对象语言。就目前而言，上述方法不适用，因为我们的对象语言类型可能有类型变量——事实上，如果在应用绑定(bind)后有自由变量，我们不想返回 Nothing ，但我们想对这些变量进行泛化。

有没有符合我描述的解决方案，即给出 applyBindings 的解决方案？与 const id 不同的类型?真正的编译器是否使用与 Mark 和 Oleg 的教程相同的双关语(在统一变量和对象语言类型变量之间)？

Answer 1

我在这里暗中尝试，因为我认为您提出的解决方案可能存在其他问题，但我至少可以解决一个困难:

您的类型检查器应该对统一类型变量和对象语言类型变量有不同的表示。

这种变化并不难实现，事实上我认为 GHC 类型检查器是这样工作的，至少有一次。您可能想查看论文 Practical Type Inference for Arbitrary-Rank Types ;附录包含很多非常有用的代码。