小编rei*_*erp的帖子

我正在实施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 …