我正在尝试实现可以在 Generalizing Hindley-Milner Type Inference Algorithms 中找到的“自下而上”类型推理算法
第 6 页解释了隐式约束是怎样的
t1
should be an instance of the type scheme that is obtained by generalizing typet2
with respect to the set of monomorphic type variablesM
但是,在第 9 页上,在解释如何将替换应用于隐式约束时,我被告知要将替换应用于这组单态类型变量。问题是,如果我有替换 [t1 := t2 -> t3]
那么 M
不再是一组类型变量。
我在这里误解了什么?
最佳答案
我联系了这篇论文的作者,当他们告诉我答案时,我确实踢了自己一脚:
替换函数的形式为 S : Substitution -> a -> a
因此,当将其应用于一组类型变量时,结果将是一组类型变量。
因此,当应用 [t1 := t2 -> t3]
而不是替换为 t2 -> t3
时,我替换为 ftv(t2 -> t3)
又名 [t2, t3]
(其中 ftv
是一个获取类型中自由类型变量的函数)。
关于functional-programming - 自底向上 Hindley-Milner 类型推断 : Applying a substitution to an implicit constraint,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/11724023/