Types of variables

Variables of type ${\it {T}}$ have different properties from ordinary expressions of type ${\it {T}}$, because variables may be assigned to. We call the types of variables reference types, and say that a variable declared to have type ${\it {T}}$ actually has type ${\it {{\rm{\it ref}}\ T}}$. This name is reasonable since a variable of type ${\it {T}}$ actually denotes a location (or reference) in which one can store a value of type ${\it {T}}$. The ability to assign a value to a variable will have a great impact on the subtype properties (or rather the lack of them) of reference types.

Suppose we have a variable ${\it {x'}}$ of type ${\it {T'}}$ (i.e., an expression of type ${\it {{\rm{\it ref}}\ T'}}$) that we wish to have masquerade as a variable of type ${\it {T}}$. See Figure 3. It is common to think of a variable of type ${\it {T}}$ as having two values: an L-value and an R-value. The L-value is the location corresponding to the variable, while the R-value is the value of type ${\it {T}}$ actually stored there.

Variables can be used in both value-supplying and value-receiving contexts. A value-supplying context is one that requires a value of type ${\it {T}}$ (i.e., the R-value of the variable). This is illustrated in the figure by the operation (arrow) labeled ``val'' coming out of the variable (representing the R-value of the variable). By the definition of subtype, in order for a variable ${\it {x'}}$ of type ${\it {T'}}$ to be able to masquerade as a value of type ${\it {T}}$ in all contexts of this kind, we need ${\it {T' {\rm \ <: \ }T}}$. This should be clear from the right-hand diagram in the figure, where in order for ${\it {x'}}$ to provide a compatible value using the ${\it {val}}$ operator, ${\it {T' {\rm \ <: \ }T}}$.

A value-receiving context is one in which a variable of type ${\it {T}}$ is assigned to, e.g., a statement of the form ${\it {x := e}}$, for ${\it {e}}$ an expression of type ${\it {T}}$. This is illustrated in the figure by an arrow labeled ``:='' going into the variable. In this context we will be interpreting the variable as a reference or location (i.e., the L-value) in which to store a value. We have already seen above that an assignment like this is type safe if ${\it {e}}$ has a type that is a subtype of the type of the variable ${\it {x}}$. Thus if we wish to use a variable of type ${\it {T'}}$ in all contexts of this form, we must ensure that ${\it {T {\rm \ <: \ }T'}}$. Again this should be clear from the right-hand diagram in the figure.

Thus for a variable of type ${\it {T'}}$ to masquerade as a variable of type ${\it {T}}$ in value-supplying contexts we must have ${\it {T' {\rm \ <: \ }T}}$, while its use in value-receiving contexts require ${\it {T {\rm \ <: \ }T'}}$. It follows that there are no non-trivial subtypes of variable (reference) types. Thus,

$${\rm{\it {{\rm{\it ref}}\ T'}}} {\rm \ <: \ }{\rm{\it {{\rm{... ...ref}}\ T}}} \mbox{ iff } {\rm{\it {T'}}} \simeq {\rm{\it {T}}},$$

where ${\it {T' \simeq T}}$ abbreviates ${\it {T' {\rm \ <: \ }T}}$ and ${\it {T {\rm \ <: \ }T'}}$. We can think of $\simeq$ as defining an equivalence class of types including such things as pairs of record types that differ only in the order of fields. It is common to ignore the differences between such types and to consider them equivalent.

  

Figure 3: A variable ${\it {x:\ ref\ T}}$, and ${\it {x':\ ref\ T'}}$ masquerading as ${\it {x}}$.

Another way of understanding the behavior of reference and function types under subtyping is to consider the different roles played by suppliers and receivers of values. Any slot in a type expression that corresponds to a supplier of values must have subtyping behave covariantly (the same direction as the full type expression), while any slot corresponding to a receiver of values must behave contravariantly (the opposite direction). Thus L-values of variables and parameters of functions, both of which are receivers of argument values, behave contravariantly with respect to subtyping. On the other hand, the R-values of variables and the results of functions, both of which are suppliers of values, behave covariantly. Because variables have both behaviors, any changes in type must be simultaneously contravariant and covariant. Hence subtypes of reference types must actually be equivalent.

The subtyping relation among object types can be rather subtle. In the simple type system considered in section 3, object types are considered subtypes when the record of method types of the subtype extends that of the supertype. That is, a subtype may contain more methods than the supertype, but the corresponding methods must have the same types. This is more restrictive than the definition of subtype for record types given above. We will see in section 4 that there is no need for such a restrictive notion of subtyping.