LARA

Subtyping for Assignments

Named Variables

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

We cannot pretend that $x$ can store values of supertype $t <: t'$ because if we later read a value, we can unexpectedly get value that is not in $V_t$

Assignment rule for named variables is therefore

\begin{equation*} \frac{(x \mapsto t) \in \Gamma,\ \Gamma \vdash e:t', t' <: t} {\Gamma \vdash (x = e)} \end{equation*}

Reference Cells

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

  • mutable containers
  • arrays

If $t$ is a type, then $t\ ref$ denotes values of references to cells that store values of type $t$

Following language ML

  • we write $ref x$ for a new cell storing value $x$
  • we write $!x$ for reading content of reference $x$
  • we write $x:=e$ for storing values of $e$ into cell referenced by $x$

\begin{equation*} \frac{e : t\ ref} {!e : t} \end{equation*}

\begin{equation*} \frac{e_1 : t\ ref,\ e_2 : t',\ t' <: t} {e_1 := e_2} \end{equation*}

If $t <: t'$ it

  • does not imply that $t\ ref <: t'\ ref$ and it
  • does not imply that $t'\ ref <: t\ ref$

The only rule that applies is that if $t=t'$ then $t\ ref = t'\ ref$

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