我正在尝试实现“自下而上”类型推理算法，该算法可在Generalizing Hindley-Milner Type Inference Algorithms中找到
第 6 页解释了隐式约束是如何产生的
t1应该是类型方案的一个实例，它是通过t2关于单态类型变量集的类型泛化获得的M
然而，在第 9 页，在解释如何对隐式约束应用替换时，有人告诉我对这组单态类型变量应用替换。问题是，如果我有替换[t1 := t2 -> t3]，则M不再是一组类型变量。
我在这里有什么误解？
user181351
问问题
547 次
2 回答
3
我与论文的作者取得了联系，当他们告诉我答案时，我确实有点自责：
替换函数具有以下形式S : Substitution -> a -> a，因此当将其应用于一组类型变量时，结果将是一组类型变量。
因此，当应用[t1 := t2 -> t3]而不是替换时，t2 -> t3我替换为ftv(t2 -> t3)aka [t2, t3]（其中ftv是获取类型中的自由类型变量的函数）。
于 2012-10-12T17:50:29.627 回答
1
如果一组单态类型变量被编码为一组单型（与裸变量名相反），那么第 9 页的 freevars(M) 中的 freevars 不需要（又一次）重载，同上替换的应用。
在这方面，SOLVE 的类型似乎有点不正确：在 activevars 的定义中，freevars 应用于 M，而在 SOLVE 中，freevars 不应用于 M（“freevars(t2) - M”），并且 M 不可能包含类型方案，即具有绑定变量。那么 M 是一组自由变量名称（无需在与其他 freevars(t) 进行集合操作之前应用 freevars）还是一组单型（需要应用 freevars）？
于 2015-05-29T17:39:44.600 回答