functional-programming - 自底向上 Hindley-Milner 类型推断 : Applying a substitution to an implicit constraint

Question

我正在尝试实现可以​​在 Generalizing Hindley-Milner Type Inference Algorithms 中找到的“自下而上”类型推理算法

第 6 页解释了隐式约束是怎样的

t1 should be an instance of the type scheme that is obtained by generalizing type t2 with respect to the set of monomorphic type variables M

但是，在第 9 页上，在解释如何将替换应用于隐式约束时，我被告知要将替换应用于这组单态类型变量。问题是，如果我有替换 [t1 := t2 -> t3] 那么 M 不再是一组类型变量。

我在这里误解了什么？

Answer 1

我联系了这篇论文的作者，当他们告诉我答案时，我确实踢了自己一脚:

替换函数的形式为 S : Substitution -> a -> a 因此，当将其应用于一组类型变量时，结果将是一组类型变量。

因此，当应用 [t1 := t2 -> t3] 而不是替换为 t2 -> t3 时，我替换为 ftv(t2 -> t3) 又名 [t2, t3](其中 ftv 是一个获取类型中自由类型变量的函数)。