# Subtyping for Assignments

## Named Variables

If a mutable variable named has type , it means that it is guaranteed to be able to store values in

We cannot pretend that can store values of supertype because if we later read a value, we can unexpectedly get value that is not in

Assignment rule for named variables is therefore

## Reference Cells

Certain types denote memory regions that do not necessarily have static names

- mutable containers
- arrays

If is a type, then denotes values of references to cells that store values of type

Following language ML

- we write for a new cell storing value
- we write for reading content of reference
- we write for storing values of into cell referenced by

If it

- does not imply that and it
- does not imply that

The only rule that applies is that if then

#### Examples

*Note: To understand the following examples, note that (x : t ref ref) coresponds to (var x : t ref). In the example below, we therefore have mutable variables x and y, storing (pos ref) and (int ref). You can think of them as simply reference variables pointing to objects with a single mutable field, which we can extract with !x and assign to using :=. An assignment of the form x=y in Java here becomes x:=!y. The expression x:=y would not even type check and makes no sense because y has type of the form (t ref ref) but we expect type of form (t ref).*

If we assume covariance, the program would type check and cause division by zero:

x : (pos ref) ref y : (int ref) ref z : int ref y := (!x); (!y) := 0; z = z / !(!x);

If we assume contravariance, then replace y:=(!x) with x:=(!y) and it will type check and lead to same problem:

x : (pos ref) ref y : (int ref) ref z : int ref x := (!y); (!y) := 0; z = z / !(!x);

Note: analogous issues arrise with arrays and mutable containers