【发布时间】：2016-06-04 12:46:08
【问题描述】：
为了使 ML 类型推断的 PT 算法起作用，输入程序表达式必须具有每个绑定变量都是不同的属性。谁能举例说明一下？
【问题讨论】：
-
谁能分享这个 PT 算法的链接？我不知道有什么，谷歌指出了这个问题。
-
是什么让您认为这是一项要求？ AFAICT，算法 W 可以很好地处理范围和阴影。必须唯一选择（“新鲜”）的是推理类型变量。
-
如果“PT”指的是主体类型，这是类型系统的属性，而不是算法，但 Hindley-Milner 算法使用统一算法来计算主体类型。您能否解释一下您到底想知道什么，以及“每个绑定变量都是不同的”是什么意思？
-
PT 指的是原则类型，给定的算法是 Hindley-Milner。换句话说，对于纯 λ 表达式是否需要重命名？ （let-free 表达式）
标签： type-inference ml bound-variable