stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Type soundness

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-01-31 18:06:04 +01:00
parent 4725943448
commit 3716fcdfd1
1 changed files with 30 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

51
soundness.tex
View File

@ -97,28 +97,29 @@ By structural induction over the expression $\texttt{e}$.
\item[$\texttt{e}.\texttt{m}(\ol{e})$]
Lets have a look at the case where the receiver and parameter types are all named types.
So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta'}{N}$:
\begin{gather}
So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta'}{N}$:
\begin{gather}
\label{sp:0}
\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T} \\
\label{sp:1}
\Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U} \\
\label{sp:2}
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\
\label{sp:3}
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\
\label{sp:4}
\Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
\end{gather}
\ref{sp:1} is guaranteed by the constraints $\ol{r} \lessdot \ol{T}$.
$\ol{\tv{r}} \lessdot \ol{T}$ says that there is a $\Delta'$ with
$\Delta, \Delta' \vdash CC(\sigma(\tv{r})) <: \type{T}$.
\ref{sp:0}, \ref{sp:1} and \ref{sp:2} are guaranteed by the generated constraints and lemma \ref{lemma:unifySoundness} and \ref{lemma:unifyCC}.
\ref{sp:4} due to $\ol{T} = \ol{\wcNtype{\Delta}{N}}$ and S-Refl. $\Delta, \Delta' \vdash \type{T}_r <: \wcNtype{\Delta'}{N}$ accordingly.
$\Delta|\Gamma \vdash \texttt{t}_r : \type{T}_r$ and $\Delta|\Gamma \vdash \ol{t} : \ol{T}_r$ by assumption.
$\Delta, \Delta' \vdash \ol{\wcNtype{\Delta}{N}} \ \ok$ by lemma \ref{lemma:unifyWellFormedness},
therefore $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} \ \ok$, which implies $\Delta, \Delta', \overline{\Delta} \vdash \ol{U} \ \ok$
by lemma \ref{lemma:wfHereditary} and \ref{sp:3} by premise of WF-Class.
The same goes for $\wcNtype{\Delta'}{N}$.
$\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ TODO!
If $\overline{\sigma(\tv{r}) = \wcNtype{\Delta}{N}}$
then \ref{sp:1} due to lemma \ref{lemma:unifyCC}.
Let $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta}{N}}$, then
\ref{sp:4} by lemma \ref{lemma:unifySoundness} and \ref{lemma:tvsNoFV}.
The environments $\overline{\Delta}$ are not needed,
because none of the variables in $\text{dom}(\overline{\Delta})$ are used in $\ol{T}$ or $\Delta, \Delta'$.
\ref{sp:3}
%\ref{sp:3}
%TODO: S is not in \sigma. They are generated by a local type inference algorithm
Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$).
@ -154,22 +155,30 @@ Method calls generate multiple constraints that share the same wildcard placehol
% $\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
% %UNIFY fails when there are free variables on the right side of a a =. T constraint
\begin{lemma}
\begin{lemma}\label{lemma:unifyWellFormedness}
\unify{} generates well-formed types as long as well-formed types are supplied.
\begin{description}
\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$ and $\sigma(\tv{a}) = \wcNtype{\ol{\wildcard{X}{\type{U}}{\type{L}}}}{N}$
\item[and] $\forall \wcNtype{\Delta}{N} \in C: \ \Delta' \vdash \wcNtype{\Delta}{N} \ \ok$
\item[then] $\Delta \vdash \ol{L <: U}$ and $\Delta \vdash \ol{U <: U'}$ % (with U' being upper limit by class definition)
\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$ %and $\sigma(\tv{a}) = \wcNtype{\ol{\wildcard{X}{\type{U}}{\type{L}}}}{N}$
\item[and] $\wcNtype{\Delta}{N} \in C \implies \Delta' \vdash \wcNtype{\Delta}{N} \ \ok$
%\item[then] $\Delta \vdash \ol{L <: U}$ and $\Delta \vdash \ol{U <: U'}$ % (with U' being upper limit by class definition)
\item[then] $\Delta \vdash \sigma(\tv{a}) \ \ok$
\end{description}
\end{lemma}
Only the \rulename{General} rule generates fresh wildcards.
By lemma \ref{lemma:unifySoundness} we get $\Delta \vdash \sigma(\type{T}) <: \sigma(\tv{a})$ with $\sigma(\tv{a}) = \wctype{\ol{\wildcard{X}{\sigma(U)}{\sigma(L)}}}{C}{\ol{X}}$
By S-Exists and S-Trans we can say $\Delta \vdash \sigma(\type{L}) <: \sigma(\type{U})$
%Only the \rulename{General} rule generates fresh wildcards.
%By lemma \ref{lemma:unifySoundness} we get $\Delta \vdash \sigma(\type{T}) <: \sigma(\tv{a})$ with $\sigma(\tv{a}) = \wctype{\ol{\wildcard{X}{\sigma(U)}{\sigma(L)}}}{C}{\ol{X}}$
%By S-Exists and S-Trans we can say $\Delta \vdash \sigma(\type{L}) <: \sigma(\type{U})$
\textit{Proof:}
by induction over every step of the \unify{} algorithm.
Hint: a type placeholder $\tv{a}$ will never be replaced by a free variable or a type containing free variables.
This fact together with the presumption that every supplied type is well-formed we can easily show that this lemma is true.
\textit{Proof: (Variant 2)}
The GenSigma and GenDelta rules check for well-formedness.
% All types supplied to the Unify algorithm by TYPEs only contain ? extends or ? super wildcards. (X : [bot..T] or X : [T .. Object]).
% Both are well formed!
\begin{lemma}
\begin{lemma}\label{lemma:wfHereditary}
Well-formedness is hereditary
\begin{description}
\item[If] $\triangle \vdash \exptype{C}{\ol{X}} \ \ok$ and $\triangle \vdash \exptype{C}{\ol{X}} <: \type{S}$