Towards polymorphism
the basic mechanism to allow polymorphism is to represent types as universally quantified (closed) terms
- whenever the environment is applied to an identifier it returns a renamed version of the type (using fresh variables)
unfortunately, types are not closed terms
- they are in general open terms, in which some variables (free variables) cannot be renamed
free variables can be determined from the current environment
- they are exactly those variables which occur in the environment
all the remaining variables are bound and therefore explicitely universally quantified