LARA

Subtyping with Assignments and Generics

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$

In a Scala-like language, we would write $Ref[T]$ instead of ${}ref{}\ x$, and we would define 

class Ref[T](var content : T)

We would write $x.\mbox{content}$ instead of $!x$, and write $x.\mbox{content}=e$ instead of $!x:=e$.

\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);

that is, in Scala: 

var x : Ref[Pos] = Ref[Pos](1)
var y : Ref[Int] = Ref[Int](-1)
var z : Int
y = x
y.content = 0
z = z / x.content

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);

that is, in Scala: 

var x : Ref[Pos] = Ref[Pos](1)
var y : Ref[Int] = Ref[Int](-1)
var z : Int
x = y
y.content = 0
z = z / x.content

Therefore, we have only the rule

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

In Scala-like notation, Ref[S] <: Ref[T] only if S=T, it is not sufficient that S <: T, otherwise we would have examples like above that crash.