What is the definition of “replacement” in the Scala Language Specification?

Question

Scala Language Specs (version 2.9 - June 11, 2014) uses the term “substitution” in the section on existential types, but the meaning of the substitution is not represented in the Scala Language Specification.

Can someone explain what substitution means in this context?

Does this mean that the type variable in the type expression is replaced with another specific type or variable type or type constructor?

If substitution means a specific type, then are specific types considered? Those that enter the realm as a simple name?

What would be the meaningful definition of substitution in this context?

What is being replaced by what?

Answer 1

This refers to the concept of replacing lambda calculus. From a practical point of view, it is a replacement of free variables with limited ones. For a more formal definition, you can take a look at the theory of lambda calculus.