
\input{minml-defns}
\input{kw-minml-defns}

\section{Subtyping with vectors, arrays and references}

Suppose we want to extend \MinML{} with a notion of immutable vectors
and mutable arrays, of types \(\Vector{\tau}\) and \(\Array{\tau}\)
respectively.
%
\begin{align*}
  \tau &\bnfdef \dots\bnfalt\Vector{\tau}\bnfalt\Array{\tau} \\
  e &\bnfdef \dots\bnfalt\SubV{e_1}{e_2}\bnfalt\SubA{e_1}{e_2}\bnfalt\Update{e_1}{e_2}{e_3}
\end{align*}

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.
%
\begin{gather*}
  \begin{array}{cc}
    \infer{\Gvdash\Dec{\SubV{e_1}{e_2}}{\tau}}
    {\Gvdash e_1\Of\Vector{\tau} & \Gvdash e_2\Of\Int} &
    \infer{\Gvdash\Dec{\SubA{e_1}{e_2}}{\tau}}
    {\Gvdash e_1\Of\Array{\tau} & \Gvdash e_2\Of\Int}
  \end{array} \\[0.1in]
  \begin{array}{c}
    \infer{\Gvdash\Dec{\Update{e_1}{e_2}{e_3}}{\Unit}}
    {\Gvdash e_1\Of\Array{\tau} & \Gvdash e_2\Of\Int
      & \Gvdash e_3\Of\tau}
  \end{array}
\end{gather*}

\subsection{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?
%
\[ \begin{array}{c}
  \infer{\Vector{\tau_1}\SubType\Vector{\tau_2}}
  {\tau_1\SubType\tau_2} \qquad
  \infer{\Array{\tau_1}\SubType\Array{\tau_2}}
  {\tau_1\SubType\tau_2}
\end{array} \]

\vspace*{2in}

\subsection{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.
%
\[ \begin{array}{c}
  \infer{\Vector{\tau}\SubType\Array{\tau}}{} \qquad
  \infer{\Array{\tau}\SubType\Vector{\tau}}{}
\end{array} \]

\vspace*{2in}

\subsection{Transitivity}

Consider the simple subtyping relation for \MinML{} given by the
following rules \emph{as well as} the valid rules from the previous
two questions.
%
\[ \begin{array}{cccc}
    \infer{\Int\SubType\Int}{} &
    \infer{\Int\SubType\Float}{} &
    \infer{\Float\SubType\Float}{} &
    \infer{\Arrow{\tau_1}{\tau_2}\SubType\Arrow{\tau'_1}{\tau'_2}}
    {\tau'_1\SubType\tau_1 & \tau_2\SubType\tau'_2}
\end{array} \]
%
Does transitivity of subtyping hold for these rules?
\begin{itemize}
\item If so, sketch a proof.
\item If not, present a counterexample. Furthermore, investigate how
  can the system be modified to include transitivity?  The modified
  system should have the same behavior as these rules along with the
  transitivity rule, but it should be syntax directed (allow an inversion principle.
\end{itemize}

\vspace*{2.5in}

\subsection{Depth subtyping on references}

Which of the following depth subtyping rules for references is
validated by the subsumption principle? Why? Exhibit the problem.
%
\[ \begin{array}{c}
  \infer{\Ref{\tau_1}\SubType\Ref{\tau_2}}
  {\tau_1\SubType\tau_2} \qquad
  \infer{\Ref{\tau_1}\SubType\Ref{\tau_2}}
  {\tau_2\SubType\tau_1}
\end{array} \]

\vspace*{1in}


% \ifsoln

% \clearpage
% \subsection{Solution}
% \begin{enumerate}
% \item First, not second.
% \item Second, not first.
% \item No.  Need
%   \[ \begin{array}{c}
%     \infer{\Array{\tau_1}\SubType\Vector{\tau_2}}{\tau_1\SubType\tau_2}
%   \end{array} \]
% \item Second.
% \item
%   \[ \begin{array}{c}
%     \infer{\Cont{\tau_1}\SubType\Cont{\tau_2}\Coerce v'}
%     {\tau_2\SubType\tau_1\Coerce v}
%   \end{array} \]
%   where \(v'=\Fn{k}{\Cont{\tau_1}}{\mathcd{wrap\_cont}\,k\,v}\)
% \end{enumerate}
% \fi


