Section C: Informal Quiz

Alberto Momigliano May 3, 2000

1 Subtyping with vectors, arrays and references

Suppose we want to extend MinML with a notion of immutable vectors and mutable arrays, of types τ vector and τ array respectively.

τ  ::= … | τ vector | τ array
e ::= … | subv(e_{1}, e_{2}) | suba(e_{1}, e_{2}) | update(e_{1}, e_{2}, e_{3})

There are three new primitive operations on vectors and arrays: Two subscript into vectors and arrays, and the other updates an array. There would also be operations for creating vectors and arrays, but they are unnecessary for the purposes of this question. Additionally, we have the following new typing rules.

\frac{⊢ e_{1} : τ vector ⊢ e_{2} : int}{⊢ subv(e_{1}, e_{2}) : τ}  \frac{⊢ e_{1} : τ array ⊢ e_{2} : int}{⊢ suba(e_{1}, e_{2}) : τ}

\frac{⊢ e_{1} : τ array ⊢ e_{2} : int ⊢ e_{3} : τ}{⊢ update(e_{1}, e_{2}, e_{3}) : unit}

1.1 Depth subtyping

Given the operations on vectors and arrays above, do either or both of the following rules validate the subsumption principle? If so, give an informal argument. If not, present a counterexample. Would that be a problem for preservation or progress?

\frac{τ_{1} <: τ_{2}}{τ_{1} vector <: τ_{2} vector}  \frac{τ_{1} <: τ_{2}}{τ_{1} array <: τ_{2} array}

1.2 Subtyping between vectors and arrays

Given the operations on vectors and arrays above, do either or both of the following rules validate the subsumption principle? Again, if so, give an informal argument. If not, exhibit the problem.

τ vector <: τ array τ array <: τ vector

1.3 Reflexivity and Transitivity

Consider the simple subtyping relation for MinML given by the following rules as well as the valid rules from the previous two questions.

\overline{int <: int}  \overline{int <: float}  \overline{float <: float}  \frac{τ′_{1} <: τ_{1} τ_{2} <: τ′_{2}}{→ τ_{1}τ_{2} <:→ τ′_{1}τ′_{2}}

Do relfexivity and transitivity of subtyping hold for these rules?

• If so, sketch a proof.

• If not, present the counterexample(s). Furthermore, investigate how can the system be modified to include reflexivity and transitivity. The modified system should have the same behavior as these rules along with the reflexivity and transitivity rule, but it should be syntax directed. State the subtyping inversion principle.

1.4 Depth subtyping on references

Which of the following depth subtyping rules for references is validated by the subsumption principle? Why? Exhibit the problem.

\frac{τ_{1} <: τ_{2}}{ref τ_{1} <: ref τ_{2}}  \frac{τ_{2} <: τ_{1}}{ref τ_{1} <: ref τ_{2}}