191 lines
10 KiB
TeX
191 lines
10 KiB
TeX
\section{Soundness}
|
|
|
|
|
|
|
|
% %This lemma can be used to proof Normalize rule!
|
|
% \begin{lemma}\label{lemma:wildcardReplacement}
|
|
% Wildcards with the same upper and lower bound can be replaced by their bounds without breaking subtype relations.
|
|
% \begin{description}
|
|
% \item[If] $\Delta \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash \type{T} <: \type{S}$
|
|
% \item[and] $\type{U} = \type{L}$ and $\text{fv}(\type{U}) = \emptyset$
|
|
% \item[Then] $\Delta \vdash [\type{U}/\type{X}]\type{T} <: [\type{U}/\type{X}]\type{S}$
|
|
% \end{description}
|
|
% \end{lemma}
|
|
% \textit{Proof:} %TODO
|
|
% %By structural induction over the subtype relation
|
|
% %S-Refl: by assumption L <: L implies [\type{U}/\type{X}]L
|
|
|
|
% \begin{lemma}\label{lemma:noAdditionalFV}
|
|
% Type solution $\sigma$ does not add additional free variables.
|
|
% \begin{description}
|
|
% \item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup C)$
|
|
% \item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
|
|
% \item[Then] $fv(\sigma(\overline{ \type{S} })) = \emptyset, fv(\sigma(\overline{ \type{T} })) = \emptyset$
|
|
% \end{description}
|
|
% \end{lemma}
|
|
|
|
% \begin{lemma}
|
|
% % https://math.libretexts.org/Bookshelves/Mathematical_Logic_and_Proof/Book%3A_Mathematical_Reasoning__Writing_and_Proof_(Sundstrom)/07%3A_Equivalence_Relations/7.03%3A_Equivalence_Classes
|
|
% $\doteq$ is an equivalence relation on a constraint set $C$.
|
|
|
|
% \begin{description}
|
|
% \item[If] $\Delta \vdash \overline{\type{T} <: \type{S}}$ and $\type{T} \doteq \type{S}$
|
|
% \item[Then] $\Delta \vdash [\type{T}/\type{S}](\overline{\type{T} <: \type{S}})$
|
|
% \end{description}
|
|
% \end{lemma}
|
|
|
|
\begin{lemma}
|
|
The \unify{} algorithm only produces correct output for constraints not containing free variables.
|
|
|
|
\begin{description}
|
|
\item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdot \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
|
|
\item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
|
|
\item[Then] there exists a $\Delta'$ with:
|
|
$\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
|
|
and $\Delta, \Delta' \vdash \overline{\text{CC}(\sigma(\type{S'})) <: \sigma(\type{T'})}$
|
|
% and $\sigma(\type{T'}) = \sigma(\type{T'})$.
|
|
|
|
The function $\text{CC}$ is given as $\text{CC}(\wcNtype{\Delta}{N}) = \type{N}$
|
|
\end{description}
|
|
\end{lemma}
|
|
|
|
\textit{Proof:}
|
|
%(we are going backwards over the algorithm)
|
|
%first we have to determine the \Delta'' -> it's only the wildcards which are free in N
|
|
% during this proof we can use Delta'' as we like
|
|
|
|
For every step in the \unify{} algorithm:
|
|
Assuming the unifier $\sigma$ is correct for a constraint set $C'$, the unifier is also correct for the
|
|
constraint set $C$ before the transformation.
|
|
\begin{description}
|
|
\item[Assumption:] $\unify{}(C) = (\Delta, \sigma)$, with $\Delta \vdash \sigma(C)$
|
|
\item[Induction step:] For every case $C'$ which can be transformed to $C$ we have to show $\Delta \vdash \sigma(C')$
|
|
\end{description}
|
|
|
|
\unify{} terminates with $C = \emptyset$ for which the preposition holds:
|
|
$\Delta \vdash \sigma(\emptyset)$
|
|
|
|
We now show that for every transformation of a constraint set $C$ to a constraint set $C'$
|
|
the preposition holds for $C$ using the assumption that it holds for $C'$ :
|
|
$\Delta \vdash \sigma(C') \implies \Delta \vdash \sigma(C)$
|
|
|
|
\begin{description}
|
|
\item[AddDelta] $C$ is not changed
|
|
\item[GenDelta] by definition, S-Var-Left, and S-Trans %The generated type variable is unique due to the solved form property. %and the solved form property (no $\tv{a}$ in $C$)
|
|
\item[GenSigma] by definition.
|
|
% holds for $\set{\tv{a} \doteq \type{G}}$ by definition.
|
|
% Holds for $C$ by assumption and because $\tv{a} \notin C$ by solved form definition ($[\type{G}/\tv{a}]C = C$).
|
|
\item[Ground] Assumption and S-Bot
|
|
\item[Sub-Elim] Assumption and S-Refl
|
|
\item[Force] by assumption and $\rwildcard{X} = \type{U}$ %TODO: step 5 should remove all X^T_T with T (make wildcards with same upper and lower bounds to normal types)
|
|
\item[Raise] Assumption, S-Trans
|
|
\item[Settle] Assumption, S-Trans
|
|
\item[Super] S-Extends ($\vdash \wctype{\Delta}{C}{\ol{T}} <: \wctype{\Delta}{D}{[\ol{T}/\ol{X}]\ol{N}}$), S-Trans
|
|
\item[\generalizeRule{}] by Assumption, because $C \subset C'$
|
|
\item[Adapt] Assumption, S-Extends, S-Trans
|
|
\item[Adopt] Assumption, because $C \subset C'$
|
|
%\item[Capture, Reduce] are always applied together. We have to destinct between two cases:
|
|
\item[Capture]
|
|
If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.
|
|
If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$ we have to show $\Delta' \vdash \text{CC}(\sigma(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}})) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$,
|
|
which holds by assumption with $\Delta'$ chosen in a way that $\text{fv}(\exptype{C}{\ol{S}}) \subseteq \Delta'$. The variables $\ol{C}$ in $\ol{S}$ can be renamed to $\ol{B}$, because $\ol{C}$ are fresh.
|
|
%If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$ we have to show $\Delta \vdash \sigma(\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$.
|
|
%$\Delta \vdash \sigma([\ol{C}/\ol{B}]\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$ holds by assumption and
|
|
%the variables $\ol{B}$ in $\ol{S}$ can be renamed to $\ol{C}$, because $\ol{C} \notin \ol{S}$ ($\ol{C}$ are fresh).
|
|
%The assumption implies $\text{fv}(\ol{S}) \subseteq \text{dom}(\Delta \cup \set{\overline{\wildcard{C}{\type{U'}}{\type{L'}}}})$
|
|
%, which implies $\text{fv}(\ol{S}) \subseteq \text{dom}(\Delta \cup \set{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}})$.
|
|
|
|
%We are doing a capture conversion. If $\type{T}$ does not contain free variables, this does not affect the subtype relation.
|
|
\item[Reduce] %Assumption and S-Exists.
|
|
If $\text{fv}(\exptype{C}{\ol{S}}) = \emptyset$ the preposition holds by Assumption and S-Exists.
|
|
If $\text{fv}(\exptype{C}{\ol{S}}) \neq \emptyset$ there exists a $\Delta'$ with
|
|
$\Delta' \vdash \text{CC}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$.
|
|
\item[Match] Assumption, S-Trans
|
|
\item[Trim] Assumption and S-Exists
|
|
\item[Remove] $C$ is not changed
|
|
\item[Circle] S-Refl
|
|
\item[Swap] by definition
|
|
\item[Erase] S-Refl
|
|
\item[Equals] by definition
|
|
% \item[Reduce]
|
|
% The renaming from $\rwildcard{C}$ to $\rwildcard{B}$ is not a problem. It's allowed to rename wildcards inside a type.
|
|
% Removing $\rwildcard{C}$ from the environment does not change anything because it was freshly generated and is used nowhere.
|
|
|
|
% The rest follows directly from S-Exists.
|
|
% We can say: $\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$,
|
|
% because the input to the \unify{} algorithm has no free type variables and we never substitute a type with free type variables
|
|
% and none of the other steps of the algorithm generates a $\lessdot$ constraint containing free type variables on the right side. %TODO: proof
|
|
|
|
% $\text{fv}(\ol{T}) \subseteq \text{dom}(\wildcardEnv \cup \overline{\wildcard{B}{\type{U'}}{\type{L'}}})$
|
|
% TODO: The capture conversion has to be when substituting a $\wtv{a}$ variable. Then we have to rename!
|
|
% %Lets first try it without the capture conversion. And involve the wtvs in the second step
|
|
% % The algorithm works by never substituting wildcards
|
|
|
|
|
|
|
|
% \unify{} cannot guarantee the premise $\text{dom}(\Delta, \Delta') \cap \text{fv}(\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N}) = \emptyset$.
|
|
% We loosen the soundness requirements and allow a arbitrary environment $\Delta''$ to be added to the right side of the subtype relation.
|
|
% This is still sufficient to proof soundness for the whole algorithm.
|
|
% We show that the need for the additional environment $\Delta''$ can be satisfied by a let statement.
|
|
|
|
% \begin{itemize}
|
|
% \item $\Delta, \Delta' \vdash [\ol{T}/\ol{X}]\ol{L} <: \ol{T}$: S-Exists
|
|
% \item $\Delta, \Delta' \vdash \ol{T} <: [\ol{T}/\ol{X}]\ol{U}$: S-Exists
|
|
% \item $\textit{fv}(\ol{T}) \subseteq \text{dom}{\Delta, \Delta'}$: $\wildcardEnv$ holds all variables %TODO: Proof
|
|
% \end{itemize}
|
|
\item[Normalize] Assumption and lemma 5 \emph{substitution preserves subtyping}.%\ref{lemma:wildcardReplacement}. (Or Lemma 5 from the wildcard paper. \emph{substitution preserves subtyping})
|
|
% The GenSigma step replaces both sides of $\rwildcard{A} \doteq \rwildcard{B}$ with the upper bound $\type{U}$.
|
|
% This works for every constraint, whether it contains free variables or not.
|
|
% It does not add to free variables of constraints because the upper bound does not contain any.
|
|
The GenSigma and Gen Delta steps remove Wildcards which have the same upper and lower bound.
|
|
$\rwildcard{A},\rwildcard{B} \notin \sigma(C)$
|
|
|
|
% sigma(T) = sigma(U) we have to show that T = U means \Delta \vdash [T/U]C \implies \Delta \vdash [U/T]C
|
|
% the constraints L <. U, U <. L lead to L =. U
|
|
%If L is List<X> with X being free wildcard
|
|
%then U <. L will fail if U is type variable
|
|
|
|
|
|
|
|
|
|
% this is because bounds never contain free variables (is that true?)
|
|
|
|
%This type contains free variables when A is replaced by an CC wildcard
|
|
|
|
%This must fail:
|
|
\begin{verbatim}
|
|
<A> A m(List<? extends List<A>> l, A)
|
|
|
|
m(List<List<? super String>> l, "hi")
|
|
\end{verbatim}
|
|
%This fails because of Equals rule (TODO: proof)
|
|
|
|
\item[Tame] same reasoning as Normalize
|
|
\item[Bot] S-Bot
|
|
\item[Pit] S-Bot
|
|
\item[Upper] S-Trans and S-VarLeft
|
|
\item[Lower] S-Trans and S-VerRight
|
|
\item[Subst-WC] by S-Refl
|
|
\item[Subst]
|
|
$\sigma(C \cup \set{\tv{a} \doteq \type{T}}) = \sigma([\type{T}/\tv{a}]C \cup \set{\tv{a} \doteq \type{T}})$
|
|
and
|
|
$\sigma(\wildcardEnv) = \sigma([\type{T}/\tv{a}]\wildcardEnv)$
|
|
\item[Subst-WC]
|
|
%Proof by Lemma 5 \emph{Type substitution preserves subtyping} from \cite{WildcardsNeedWitnessProtection}.
|
|
Same as Subst
|
|
\end{description}
|
|
|
|
\subsection{Type Inference Soundness}
|
|
The type solution is a correct one in respect to the type rules.
|
|
|
|
Problem:
|
|
The capture conversion and let statements.
|
|
Constraint a <. b => CC(X.C<X>) <: C<X>
|
|
Why is X the only type used
|
|
|
|
$\type{T} \lessdot \type{S}$:
|
|
If the left part of the constraint has no free variables the solution $\sigma(\type{T})$ will have neither.
|
|
This means that all used type variables on both sides are bound in the global environment or the environment of the left side
|
|
%X.C<X> <: C<X>
|
|
%C<X> = C<X> (both sides must be the same)
|
|
%the left side has no free variables! |