12

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

applyBindings :: TyEnv -> Type -> Type

它将tyvar -> ty绑定应用于TyEnv给定的Type. 我发现在我的代码中忘记调用是一个常见错误applyBindings，而且我没有从 Haskell 的类型系统中得到任何帮助，因为ty它与applyBindings tyenv ty. 我正在寻找一种在类型系统中强制执行以下不变量的方法：

在进行类型推断时，必须在返回“最终”结果之前应用绑定

在为单态对象语言进行类型推断时，有一种自然的方式来强制执行这一点，正如在 wren ng thornton 的unification-fd 包中实现的那样：我们为 s 定义了两种数据类型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，那么我们将得到一个类型错误。

这是我正在寻找的解决方案，但对于具有多态性的对象语言。就目前而言，上述方法并不适用，因为我们的对象语言类型可能具有类型变量——事实上，如果在应用绑定后有自由变量，我们不想 return Nothing，但我们想概括一下这些变量。

有没有按照我描述的思路的解决方案，即提供applyBindings不同类型的解决方案const id？真正的编译器是否使用与 Mark 和 Oleg 的教程相同的双关语（在统一变量和对象语言类型变量之间）？

4

1 回答 1

5

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

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

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

于 2012-03-19T01:22:04.960 回答