406 lines
21 KiB
TeX
406 lines
21 KiB
TeX
\section{Soundness}
|
|
|
|
\newcommand{\CC}{\text{CC}}
|
|
|
|
\begin{theorem}\label{testenv-theorem}
|
|
Type inference produces a correctly typed program.
|
|
\begin{description}
|
|
\item[If] $\fjtypeinference(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
|
|
\triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \mtypeEnvironment{}'$
|
|
\item[Then] $\texttt{class}\ \exptype{C}{\ol{X}
|
|
\triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \} \text{ok}$,
|
|
with $\ol{M} = $
|
|
\end{description}
|
|
\end{theorem}
|
|
|
|
\begin{lemma}{Well-formedness:}
|
|
TODO:
|
|
\end{lemma}
|
|
|
|
\begin{lemma}{Soundness:}
|
|
\unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
|
|
\begin{description}
|
|
\item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = C$
|
|
and $(\Delta, \sigma) = \unify{}(\Delta', C)$
|
|
% , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } }$
|
|
% and $\vdash \ol{L} : \mtypeEnvironment{}$
|
|
% and $\Gamma \subseteq \mtypeEnvironment{}$
|
|
% \item[given] a $(\Delta, \sigma)$ with $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
|
|
% and there exists a $\Delta'$ with $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T'})}$
|
|
\item[then] $\Delta|\Gamma \vdash |\texttt{e}| : \sigma(\tv{a})$
|
|
\end{description}
|
|
\end{lemma}
|
|
Regular type placeholders represent type annotations.
|
|
These are the only types a \wildFJ{} program needs to be correctly typed.
|
|
The type placeholders flagged as wildcard placeholders are intermediate types
|
|
used in let statements and as type parameters for generic method calls.
|
|
|
|
%Unify needs to return S aswell and guarantee that the \Delta' environment are the wildcards
|
|
% only used inside the constraint the wildcard variable occurs
|
|
% should Unify also return the \Delta' environment? Otherwise the bounds of free wildcard variables are lost
|
|
|
|
% Or is it possible to deduct the right \ol{S} directly from the types in the normal TPHs?
|
|
|
|
\textit{Proof:}
|
|
By structural induction over the expression $\texttt{e}$.
|
|
\begin{description}
|
|
\item[$\texttt{e}.\texttt{f}$] Let $\sigma(\tv{r}) = \wcNtype{\Delta_c}{N}$,
|
|
then $\Delta|\Gamma \vdash \texttt{e} : \wcNtype{\Delta_c}{N}$ by assumption.
|
|
$\Delta', \Delta, \Delta_c \vdash \type{N} <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
|
|
%Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$.
|
|
%Let $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) = \wcNtype{\Delta_t}{N_t}$.
|
|
|
|
The completion of $|\texttt{e}.\texttt{f}|$ is $\texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f}$
|
|
|
|
We now show
|
|
$\Delta|\Gamma \vdash \texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f} : \sigma(a)$
|
|
by the T-Field rule.
|
|
$\Delta \vdash \wcNtype{\Delta_c}{N} <: \wcNtype{\Delta_c}{N}$ by S-Refl.
|
|
$\Delta, \Delta_c \vdash \type{U}_i <: \sigma(\tv{a})$,
|
|
because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$ and lemma \ref{lemma:unifySoundness}.
|
|
$\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$
|
|
and $\text{fv}(\type{U}_i) \subseteq \text{fv}(\type{N})$ by definition of $\textit{fields}$.
|
|
|
|
$\text{dom}(\Delta_c) \subseteq \text{fv}{\type{N}}$ by lemma \ref{lemma:tvsNoFV}.
|
|
|
|
% X.List<X> <. List<a?>
|
|
% $\sigma(\ol{\tv{r}}) = \overline{\wcNtype{\Delta}{N}}$,
|
|
% $\ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
|
|
% TODO: S ok? We could proof $\Delta, \Delta' \overline{\Delta} \vdash \ol{S} \ \ok$
|
|
% by proofing every substitution in Unify is ok aslong as every type in the inputs is ok
|
|
% S ok when all variables are in the environment and every L <: U and U <: Class-bound
|
|
% This can be given by the constraints generated. We can proof if T ok and S <: T and T <: S' then S ok and S' ok
|
|
|
|
% If S ok and T <. S , then Unify generates a T ok
|
|
S typeinference:
|
|
T <: [S/Y]U
|
|
We apply the following lemma
|
|
Lemma
|
|
if T ok and T <: S then S ok
|
|
|
|
until
|
|
T = [S/Y]U
|
|
|
|
and then we can say by
|
|
Lemma:
|
|
If [S/Y]U ok then S ok (TODO: proof!)
|
|
|
|
So we do not have to proof S ok (but T)
|
|
|
|
% T_r <: C<T> (S is in T)
|
|
% Is C<T> ok?
|
|
% if every type environment \Delta supplied to Unify is ok (L <: U), then \sigma(a) = \Delta'.N implies \Delta' conforms to (L <: U)
|
|
% this together with the X <. N constraints proofs T_r ok
|
|
|
|
$\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
|
|
%Easy, because unify only generates substitutions for normal type placeholders which are OK
|
|
|
|
\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}
|
|
\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'} \\
|
|
\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}$.
|
|
|
|
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}
|
|
%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}}$).
|
|
%TODO: show that only those wildcards in the parameters and receiver type are used ($\ol{\Delta}$)
|
|
|
|
% X.List<X> <. List<a?>
|
|
% set \sigma(r) = X.N
|
|
% If there exists a subtype r <: T, then r <: X.N, N <: T with X.N == r
|
|
% If CC(X.N) <: T, then N <: T
|
|
% R <: X.N due to S-Refl.
|
|
% \Delta, X \vdash N <: T due to assumption and S-Exists.
|
|
% What if X.N <: Y (where is this Y coming from?)
|
|
% %TODO:
|
|
% We have to show, that all constraints using the same wtv's C = X1.T1 <. X2.T2 ,...
|
|
% with a? \in T1, T2, ....
|
|
% then \Delta' \subseteq X1, X2, ... for \Delta, \Delta \vdash sigma(T1) <: sigma(X2.T2), ....
|
|
|
|
% when only wildcards in the top level domain from the constraints involving the a? variables are involved
|
|
% then they are all contained in $\Delta, \Delta', \overline{Delta}$, which makes S ok true! (does it?)
|
|
% and due to r <. T, the judgements N <: [S/X]U and T_r <: \Delta.N are true!
|
|
|
|
% If $\ol{\tv{r}} \lessdot \ol{T}$ how can we say that \Delta' only uses
|
|
\end{description}
|
|
|
|
% \begin{lemma} Unify does add free variables to types not containing free variables (or wildcard placeholders)
|
|
% \begin{description}
|
|
% \item[If] $(\sigma, \Delta) = \unify{}( \Delta', C )$
|
|
% \item[Then] $\forall x \in \set{\type{S} \mid \type{S} \in C, \text{fv}(\type{S}) = \emptyset }: \text{fv}(\sigma(\type{S})) \subseteq \text{dom}(\Delta)$
|
|
% \end{description}
|
|
% \end{lemma}
|
|
% \textit{Proof:} by induction over the \unify{} algorithm.
|
|
% A unifier $\sigma(\tv{a}) = \type{T}$, where the type variable $\tv{a}$ is not flagged as a wildcard will always hold
|
|
% $\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}
|
|
\unify{} generates well-formed type environments
|
|
\begin{description}
|
|
\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$
|
|
\item[and] $\forall \Delta_w \in C: \vdash \type{L} <: \type{U}$
|
|
\item[then] TODO
|
|
\end{description}
|
|
\end{lemma}
|
|
|
|
\begin{lemma}
|
|
Well-formedness is hereditary
|
|
\begin{description}
|
|
\item[If] $\triangle \vdash \exptype{C}{\ol{X}} \ \ok$ and $\triangle \vdash \exptype{C}{\ol{X}} <: \type{S}$
|
|
\item[Then] $\triangle \vdash \type{S} \ \ok$
|
|
\end{description}
|
|
\end{lemma}
|
|
\textit{Proof:}
|
|
|
|
\begin{lemma}
|
|
|
|
\begin{description}
|
|
\item[If] $\Delta \vdash \wctype{\Delta'}{C}{\ol{T}} \ \ok$
|
|
\item[Then] $\Delta, \Delta' \vdash \ok{T} \ \ok$
|
|
\end{description}
|
|
\end{lemma}
|
|
\textit{Proof:} by definition of WF-Class
|
|
|
|
|
|
\begin{lemma} \label{lemma:tvsNoFV}
|
|
\unify{} does not add free variables to types not containing free variables.
|
|
\begin{description}
|
|
\item[If] $(\sigma, \Delta) = \unify{} (\Delta', C)$
|
|
\item[and] $\tv{a}$ being a type placeholders used in $C$
|
|
\item[then] $\text{fv}(\sigma(\tv{a})) \subseteq \Delta, \Delta'$
|
|
\end{description}
|
|
\end{lemma}
|
|
\textit{Proof:}
|
|
Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.
|
|
|
|
\begin{lemma} \label{lemma:unifyCC}
|
|
Free variables do not leave their scope. TODO
|
|
Wildcard variables are only substituted by wildcards inside the same constraint.
|
|
|
|
\begin{description}
|
|
\item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \type{T} \lessdot \type{S} } \cup \set{ \overline{\type{T} \lessdotCC \type{S} } } )$
|
|
\item[and] $\text{fv}(\type{T}, \type{S}) \subseteq \text{fv}(\ol{T}, \ol{S})$,
|
|
$\sigma(\ol{T}) = \ol{\wcNtype{\Delta}{N}}$ and $\sigma(\type{T}) = \wcNtype{\Delta'}{N'}$
|
|
\item[then] $ \Delta, \overline{\Delta}, \Delta' \vdash \sigma(\type{T}) <: \sigma(\type{S}) $
|
|
|
|
% \item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \overline{\wcNtype{\Delta}{N} \lessdot \type{T} } } )$
|
|
% \item[and] $\text{fv}(\ol{T}) \notin C$, $\text{fv}(\ol{\wcNtype{\Delta}{N}}) \notin C$
|
|
% \item[Then] $\Delta, \overline{\Delta} \vdash \overline{ \sigma(\type{N}) <: \sigma(\type{T}) }$
|
|
\end{description}
|
|
|
|
Their scope is the set of constraints, which contain the same free variable placeholders.
|
|
|
|
\end{lemma}
|
|
\textit{Proof:}
|
|
%TODO: is it true even?
|
|
The input set does not contain free variables, only free variable placeholders.
|
|
The only time \unify{} add a wildcard to the $\wildcardEnv$ is the \rulename{Capture} rule.
|
|
This rule is only applied for the outer wildcard environments for each type.
|
|
|
|
\begin{lemma}\label{lemma:unifySoundness}
|
|
The \unify{} algorithm only produces correct output.
|
|
\begin{description}
|
|
\item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \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 $\sigma'$ with:
|
|
$\sigma \subseteq \sigma'$ and
|
|
$\Delta, \Delta', \overline{\Delta} \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
|
|
and $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$ where $\overline{\sigma(\type{S'}) = \wcNtype{\Delta}{N}}$,
|
|
otherwise $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \sigma'(\type{T'})}$
|
|
% and $\sigma(\type{T'}) = \sigma(\type{T'})$.
|
|
|
|
% The function $\CC{}$ is given as $\CC{}(\wcNtype{\Delta}{N}) = \type{N}$
|
|
|
|
% Unify cannot guarantee that only wildcards declared on the left side are used. Example input:
|
|
% List<b?> <. List<b?>
|
|
% b? =. X
|
|
% but if the left side is a normal type (no fv's) then this can be guaranteed (maybe?)
|
|
%String <. X_String % here X is not in the environment
|
|
|
|
% What is the problem?
|
|
% a? can only use wildcards, which are declared in \Delta or on the left side
|
|
% Otherwise constraints of the form a <. T cannot ensure soundness!
|
|
|
|
% We could say that a? only gets free variables hold by the constraints a? appears in
|
|
|
|
% a constraint a <. T means that there are free variables
|
|
\end{description}
|
|
\end{lemma}
|
|
|
|
% \begin{lemma} % a lemma where we distinguis between free variable on the left or the right side of a constraint (not needed anymore)
|
|
% 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{ \wcNtype{\Delta'}{N} \lessdot \type{T'} } \cup \overline{ \type{S'} \lessdot \wcNtype{\Delta'}{N'} })$
|
|
% \item[and] $fv(\overline{ \type{S} }) = \emptyset, fv(\overline{ \type{T} }) = \emptyset, fv(\overline{ \type{T'} }) = \emptyset, fv(\overline{ \type{S'} }) = \emptyset$
|
|
% \item[Then] $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
|
|
% and $\Delta, \Delta' \vdash \overline{\sigma(\type{N}) <: \sigma(\type{T'})}, \overline{\sigma(\type{S'}) <: \sigma(\type{N'})}$
|
|
% %TODO: Rephrase (\Delta' is used three times!)
|
|
% %The function $\CC{}$ is given as $\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 and S-Refl.
|
|
% 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[Prepare]
|
|
Given a $\wctype{\Delta_c}{C}{\ol{S}} \lessdot \wcNtype{\Delta''}{N}$
|
|
we get $\Delta, \Delta', \overline{\Delta} \vdash \exptype{C}{\ol{S}} <: \wcNtype{\Delta''}{N}$ with $\Delta_c \subseteq \overline{\Delta}$.
|
|
|
|
$\text{fv}(\sigma'(\wctype{\Delta_c}{C}{\ol{S}})) = \emptyset$ implies $\text{fv}(\ol{S})\subseteq \text{dom}(\Delta, \Delta_c)$
|
|
and $\text{fv}(\sigma'(\wcNtype{\Delta''}{N})) = \emptyset$ implies $\text{dom}(\Delta_c) \cap \text{fv}(\sigma'(\wcNtype{\Delta''}{N})) = \emptyset$.
|
|
|
|
No free variables on both sides also mean we do not need $\overline{\Delta}$.
|
|
Therefore we can say $\Delta, \Delta' \vdash \wctype{\Delta_c}{C}{\ol{S}} <: \wcNtype{\Delta''}{N}$.
|
|
|
|
\item[Capture]
|
|
Everytime the \rulename{Capture} rule is invoked we add the freshly generated free variables to the global environment $\wildcardEnv$.
|
|
We get a $\sigma'$ %and a $\Delta'$
|
|
with $\Delta, \Delta' \vdash \sigma'([\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}}) <: \sigma'(\wctype{\Delta}{C}{\ol{T}})$
|
|
where $\sigma'(\ol{\wildcard{C}{U}{L}}) \subseteq \Delta'$ by assumption.
|
|
\unify{} performs a capture conversion only on $\lessdotCC$ constraints.
|
|
Therefore we can say that $\Delta, \Delta', \overline{\Delta} \vdash \sigma'(\exptype{C}{\ol{S}})
|
|
<: \sigma'(\wctype{\Delta}{C}{\ol{T}})$ with $\overline{\Delta}$ being all the fresh wildcards generated by \rulename{Capture}.
|
|
|
|
\item[Reduce]
|
|
|
|
%Assumption and S-Exists.
|
|
% Three different cases of the constraint $\exptype{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$:
|
|
% \begin{description}
|
|
% \item[$\text{fv}(\exptype{C}{\ol{S}}) = \emptyset, \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$:]
|
|
% the preposition holds by Assumption and S-Exists.
|
|
% \item[$\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$:]
|
|
% then $\text{fv}(\exptype{C}{\ol{S}}) \subseteq \Delta'$ with $\Delta' = \overline{\wildcard{A}{\type{U}}{\type{L}}}$
|
|
% \item[$\text{fv}(\exptype{C}{\ol{S}}) = \emptyset$] $\Delta' = \emptyset$
|
|
% \end{description}
|
|
% List<X> <. Y.List<Y>, free variables are either in
|
|
If $\text{fv}(\exptype{C}{\ol{S}}) = \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.
|
|
Otherwise
|
|
$\Delta' \vdash \CC{}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$
|
|
holds with any $\Delta'$ so that $(\text{fv}(\exptype{C}{\ol{S}}) \cup \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) ) \subseteq \text{dom}(\Delta') $.
|
|
\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}
|