scala - Scala 语言规范中术语 "substitution"的定义是什么？

Question

在 Scala 语言规范(2.9 版 - 2014 年 6 月 11 日)中，在有关存在类型的部分中使用了术语“替换”，但是，Scala 语言规范中似乎没有定义替换的含义。

有人可以解释在这种情况下替换的含义吗？

这是否意味着类型表达式中的类型变量被其他具体类型或类型变量或类型构造函数替换？

如果替换意味着是具体类型，那么考虑什么是具体类型？那些作为简单名称在范围内的？

在这种情况下，“替代”概念的有意义的定义是什么？

什么被什么取代？

Answer 1

它指的是 lambda 演算的替换概念。从实用的角度来看，它是用有界变量替换自由变量。对于更正式的定义，您可以查看 lambda 演算理论。