用于 ML 类型推理的 PT 算法

Question

要使 ML 类型推理的 PT 算法正常工作，输入程序表达式必须具有每个绑定变量都是不同的属性。有人可以用一个例子来解释吗？

Answer 1

关键在于由不同绑定程序绑定的变量彼此不同，因此可能具有不同的类型。因此，重命名它们是一种很好的做法，以避免混淆并能够谈论"x"的类型，而不必担心我们指的是"x"的哪个活页夹。