Hindley-Milner算法:使用类型来确保应用绑定

Question

我正在实施Hindley-Milner类型推理算法,遵循Mark Jones和Oleg Kiselyov的教程.这两个都有一个"应用绑定"操作,其大致类型的形式

applyBindings :: TyEnv -> Type -> Type

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

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

在对单形对象语言进行类型推断时,有一种自然的方法可以强制执行此操作,正如在thornton的unification-fd包中实现的那样:我们为Types 定义了两种数据类型:

-- | 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是统一-fd).这强制了我们的不变量 - 如果我们忘记了applyBindings,那么我们将得到一个类型错误.

这是我正在寻找的解决方案,但是对于具有多态性的对象语言.目前的上述方法并不适用,因为我们的对象语言类型可能有类型变量 - 实际上,如果在应用绑定后存在变量,我们不想返回Nothing,但我们想要概括这些变量.

是否有我所描述的解决方案,即提供applyBindings不同类型的解决方案const id？真正的编译器是否使用Mark's和Oleg的教程所做的相同的惩罚(在统一变量和对象语言类型变量之间)？

Answer 1

我在黑暗中采取刺,因为我认为你提出的解决方案可能存在其他问题,但我可以解决至少一个难题:

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

这种变化并不难实现,事实上我认为GHC类型检查器是这样工作的,至少在一次.您可能想查看任意等级类型的实用类型推断论文; 附录包含许多非常有用的代码.