PT algorithm for ML type inference

167 Views Asked by At

For the PT algorithm for ML type inference to work, the input program expression has to have the property that every bound variable is distinct. Can somebody explain it with an example?

1

There are 1 best solutions below

0
On

The point is simply that variables bound by different binders are different from each other, and hence may have different types. So, it is a good practice to rename them, in order to avoid confusion and to be able to talk about the type of "x", without having to worry about which among the binders of "x" we are referring to.