LARA

Subtyping Rules

Subtype relation C<:D iff there is a chain of subclass relations from D (the super class) to C (the subclass)

How do we modify subtyping rules for

  • assignments
  • method calls

Assignment

\begin{equation*}
\frac{?}
     {\Gamma \vdash (x=e) : void}
\end{equation*}

Method calls:

\begin{equation*}
\frac{?}
     {\Gamma \vdash (x=m(e_1,\ldots,e_n)) : void}
\end{equation*}

Method definitions:

\begin{equation*}
\frac{?}
     {\Gamma \vdash (T\ m(T_1\, x_1,\ldots,T_n\, x_n) \{s; \mbox{return}\ e\} : {?}}
\end{equation*}

What is the justification for these changes from the viewpoint of interpreter?

Generic Subtyping Rule:

\begin{equation*}
   \frac{\Gamma \vdash x : C, C<:D}
        {?}
\end{equation*}

Answer

Uniqueness and Non-Uniqueness of Assigned Types