Ecoop2024_TIforWildFJ/soundness.tex
2024-04-03 00:45:51 +02:00

667 lines
34 KiB
TeX

\section{Soundness}
\newcommand{\CC}{\text{CC}}
\begin{lemma}
A sound TypelessFJ program is also sound under LetFJ type rules.
\begin{description}
\item[if:]
$\Gamma | \Delta \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \ \text{in}\ C \text{with} \ \generics{\ol{Y \triangleleft P}}$
\end{description}
\end{lemma}
TODO: Beforehand we have to show that $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
Here $\Delta$ does not contain every $\overline{\Delta}$ ever created.
%what prevents a free variable to emerge in \Delta.N example Y^Object |- C<String> <: X^Y.C<X>
% if the Y is later needed for an equals: same(id(x), x2)
Free wildcards do not move inwards. We can show that every new type is either well-formed and therefore does not contain any free variables.
Or it is a generic method call: is it possible to use any free wildcards here?
let empty
<X> Box<X> empty()
same(Box<?>, empty())
let p1 : X.Box<X> = Box<?> in let
X.Box<X> <. Box<x>
Box<e> <. Box<x>
boxin(empty()), Box2<?>
Where can a problem arise? When we use free wildcards before they are freed.
But we can always CC them first. Exception two types: X.Pair<X, y> and Y.Pair<x, Y>
Here y = Y and x = X but
<X,Y> void same(Pair<X,Y> a, Pair<X,Y> b){}
<X> Pair<?, X> left() { return null; }
<X> Pair<X, ?> right() { return null; }
<X> Box<X> id(Box<? extends Box<X>> x)
here it could be beneficial to use a free wildcard as the parameter X to have it later
Box<?> x = ...
same(id(x), id(x)) <- this will be accepted by TI
let left : X,Y.Pair<X,Y> = left() in
let right : Pair<X,Y> = right() in
Compromise:
- Generate constraints so that they comply with LetFJ
- Propose a version which is close to Java
Version for LetFJ:
Is it still possible to do the capture conversion in form of constraints?
X.C<X> <. C<x>
T <. X.C<X>
how to proof: X.C<X> ok
If $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
then there exists a $|\texttt{e}|$ with $\Delta | \Theta \vdash |\texttt{e}| : \wcNtype{\Delta'}{N}$ in LetFJ.
This is possible by starting with the parameter types as the base case $\overline{\Delta} = \emptyset$.
Each type $\wcNtype{\Delta'}{N}$ can only use wildcards already freed.
\textit{Proof} by structural induction.
\begin{description}
\item[$\texttt{e} = \texttt{x}$] $\Delta | \Theta \vdash \texttt{e} : \type{T} \mid \emptyset$
$\Delta \vdash \type{T} \ \ok$ by \rulename{T-Method}
and therefore $\Delta | \Theta \vdash \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$.
$|\texttt{x}, \texttt{e}| = \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$
\item[$\texttt{e} = \texttt{e}.\texttt{m}(\ol{e})$] there must be atleast one value in $\texttt{e}$ or $\ol{e}$
\item[$\texttt{e}.f$] given let x : T = e' in x
let x : T = e' in let xf = x.f in xf
Required:
$ \Delta | \Theta \vdash e' : \type{T}_1$
$\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$
$\Delta, \Delta' | \Theta, x : \type{N} \vdash let xf = x.f in xf : \type{T}_2$
\end{description}
\textbf{Proof:} Every program complying with our type rules can be converted to a correct LetFJ program.
First we convert the program so that every wildcards used in an expression are in the $\Delta$ environment:
m(p) = e => let xp = p in [xp/p]e
x1.m(x2) => let xm = x1.m(x2=) in xm
x.f => let xf = x.f in xf
Then we have to proof there is never a wildcard used before it is declared.
Wildcards are introduced by the capture conversions and nothing else.
\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_u, \sigma) = \unify{}(\Delta', C)$ and let $\Delta = \Delta_u \cup \Delta'$
% , 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] there is a completion $|\texttt{e}|$ with $\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_u}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta_u}{N}$
and a $\Delta'$, $\overline{\Delta}$ where $\Delta' \subseteq \Delta_u$, $\overline{\Delta \subseteq \Delta_u}$
and $\text{dom}(\Delta') = (\text{fv}(\type{N})/\Delta)$, $\overline{\text{dom}(\Delta) = (\text{fv}(\type{N})/\Delta)}$ in
$\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\
\texttt{let}\ \ol{x} : \overline{\wcNtype{\Delta'}{N}} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x})$
%TODO: show that this type exists \wcNtype{\Delta'}{N} (a \Delta' which only contains free variables of the type N)
% and which is a supertype of T_r (so no free variables in T_r)
% Solution: Make this a lemma and guarantee that Unify does only create types Delta.T with \Delta subset fv(T)
% This is possible because free variables (except those in \Delta_in) are never used in wildcard environments
By lemma \ref{lemma:unifyWeakening} we know that
$\unify{}(\Delta, [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{ \overline{\wcNtype{\Delta}{N}} \lessdotCC \ol{T}, \wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}})$
has a solution.
Also $\overline{\wcNtype{\Delta}{N}} \lessdot \ol{T}$ and $\wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}$ will be converted to
$\ol{N} \lessdot \ol{T}$ and $\type{N} \lessdot \exptype{C}{\ol{X}}$ by the \rulename{Capture} rule.
Which then results in the same as calling $\unify{}((\Delta, \Delta', \overline{\Delta}), [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{\ol{N} \lessdot \ol{T}, \type{N} \lessdot \exptype{C}{\ol{X}}})$,
which shows $\Delta, \Delta', \overline{\Delta} \vdash \overline{N} <: [\ol{S}/\ol{X}]\overline{U}$.
This implies $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ and $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
$\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T}$,
$\Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$
are guaranteed by the generated constraints and lemma \ref{lemma:unifySoundness} and \ref{lemma:unifyCC}.
$\Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}$ 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 $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok $ by premise of WF-Class.
The same goes for $\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}
Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$).
\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}\label{lemma:unifyNoExcessWildcards}
\begin{description}
\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$
\item[Then] $\sigma(\tv{a}) = \wcNtype{\Delta''}{N} \implies \text{dom}(\Delta'') \subseteq \text{fv}(\type{N})$
\end{description}
\end{lemma}
\textit{Proof:} Easy -
All types given in the input to the \unify{} algorithm already comply with this requirement
and none of the rules change.
Note: the \rulename{Super} rule removes unnecessary wildcards.
\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] $\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})$
\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}\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}$
\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.
% do we even have to proof that?
% \begin{lemma}
% C = Delta.N <c T
% is the same for Unify as:
% Delta |- N <. T
% \end{lemma}
\begin{lemma} \label{lemma:unifyWeakening}
Removing constraints does not render \unify{} impossible as long as the removed constraints do not share wildcard placeholders.
If there is a solution for a constraint set $C$, then there is also a solution for a subset of that constraint set.
\begin{description}
\item[If] $(\sigma, \Delta) = \unify{}( C \cup C')$ and $\text{wtv}(C) \cap \text{wtv}(C') = \emptyset$
\item[then] $ (\sigma', \Delta') = \unify{}( C')$
\end{description}
\end{lemma}
\textit{Proof:}
%TODO
% does this really work. We have to show that the algorithm never gets stuck as long as there is a solution
% maybe there are substitutions with types containing free variables that make additional solutions possible. Check!
\begin{lemma}{\unify{} Soundness:}\label{lemma:unifySoundness}
\unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}.
\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[Then] there exists a substitution $\sigma'$ and a set of types $\overline{\wcNtype{\Delta}{N}}$ with:
\begin{itemize}
\item $\sigma \subseteq \sigma'$
\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \wcNtype{\Delta}{N}}$
\item $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$
\end{itemize}
\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[GenDelta'] same as GenDelta by setting $\sigma'(\wtv{b}) = \rwildcard{B}$
\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[Same] by S-Exists
\item[SameW] %TODO
\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 \ref{def:equal}
%by definition
%TODO
% Unify does never contain wildcard environments with unused wildcards. Therefore after N <: N' and N' <: N, both types have the same wildcard environment
% \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{Converting to Wild FJ}
Wildcards are existential types which have to be \textit{unpacked} before they can be used.
In Java this is done implicitly by a process called capture conversion \cite{JavaLanguageSpecification}.
The type system in \cite{WildcardsNeedWitnessProtection} makes this process explicit by using \texttt{let} statements.
Our type inference algorithm will accept an input program without let statements and add them where necessary.
%Type inference adds \texttt{let} statements in a fashion similar to the Java capture conversion \cite{WildFJ}.
%We wrap every parameter of a method invocation in \texttt{let} statement unknowing if a capture conversion is necessary.
Figure \ref{fig:tletexpr} shows type rules for fields and method calls.
They have been merged with let statements and simplified.
The let statements and the type $\wcNtype{\Delta'}{N}$, which the type inference algorithm can freely choose,
are necessary for the soundness proof.
%TODO: Show that well-formed implies witnessed!
We change the type rules to require the well-formedness instead of the witnessed property.
See figure \ref{fig:well-formedness}.
Our well-formedness criteria is more restrictive than the ones used for \wildFJ{}.
\cite{WildcardsNeedWitnessProtection} works with the two different judgements $\ok$ and \texttt{witnessed}.
With \texttt{witnessed} being the stronger one.
We rephrased the $\ok$ judgement to include \texttt{witnessed} aswell.
$\type{T} \ \ok$ in this paper means $\type{T} \ \ok$ and $\type{T} \ \texttt{witnessed}$ in the sense of the \wildFJ{} type rules.
Java's type system is complex enough as it is. Simplification, when possible, is always appreciated.
Our $\ok$ rule may not be able to express every corner of the Java type system, but is sufficient to show soundness regarding type inference for a Java core calculus.
The \rulename{WF-Class} rule requires upper and lower bounds to be direct subtypes of each other $\type{L} <: \type{U}$.
The type rules from \cite{WildcardsNeedWitnessProtection} use a witness type instead.
Stating that a type is well formed (\texttt{witnessed}) if there exists atleast one simple type $\type{N}$ as a possible subtype:
$\Delta \vdash \type{N} <: \wctype{\Delta'}{C}{\ol{T}}$.
A witness type is easy to find by replacing every wildcard $\ol{W}$ in $\wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$ by its upper bound:
$\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} <: \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$.
$\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} \ \texttt{witnessed}$ is given due to $\Delta \vdash \ol{T}, \ol{L}, \ol{U} \ \ok$
and $\Delta \vdash \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}} \ \ok$.
\begin{figure}[tp]
$\begin{array}{l}
\typerule{T-Var}\\
\begin{array}{@{}c}
x : \type{T} \in \Gamma
\\
\hline
\vspace*{-0.3cm}\\
\Delta | \Gamma \vdash x : \type{T}
\end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
\typerule{T-New}\\
\begin{array}{@{}c}
\Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} \ \ok \quad \quad
\text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
\Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
\Delta \vdash \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
\Delta, \overline{\Delta} \vdash \overline{\type{N}} <: \overline{\type{U}} \quad \quad
\Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
\overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
\Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok
\\
\hline
\vspace*{-0.3cm}\\
\Delta | \Gamma \vdash \letstmt{\ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}{\texttt{new} \ \exptype{C}{\ol{T}}(\overline{t})} : \type{T}
\end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
\typerule{T-Field}\\
\begin{array}{@{}c}
\Delta | \Gamma \vdash \texttt{t} : \type{T} \quad \quad
\Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
\textit{fields}(\type{N}) = \ol{U\ f} \\
\Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
\text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
\Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
\\
\hline
\vspace*{-0.3cm}\\
\Delta | \Gamma \vdash \texttt{let}\ x : \wcNtype{\Delta'}{N} = \texttt{t} \ \texttt{in}\ x.\texttt{f}_i : \type{S}
\end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
\typerule{T-Call}\\
\begin{array}{@{}c}
\Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
\textit{mtype}(\texttt{m}, \type{N}) = \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \quad \quad
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
\\
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
\Delta | \Gamma \vdash \texttt{t}_r : \type{T}_r \quad \quad
\Delta | \Gamma \vdash \ol{t} : \ol{T} \quad \quad
\Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
\Delta \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
\\
\Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
\Delta, \Delta', \Delta'' \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
\text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
\overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
\\
\hline
\vspace*{-0.3cm}\\
\Delta | \Gamma \vdash \letstmt{x : \wcNtype{\Delta'}{N} = t_r, \ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}
{\texttt{x}.\generics{\ol{S}}\texttt{m}(\ol{x})} : \type{T}
\end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
\typerule{T-Elvis}\\
\begin{array}{@{}c}
\Delta | \Gamma \vdash t_1 : \type{T}_1 \quad \quad
\Delta | \Gamma \vdash t_2 : \type{T}_2 \quad \quad
\Delta \vdash \type{T}_1 <: \type{T} \quad \quad
\Delta \vdash \type{T}_2 <: \type{T}
\\
\hline
\vspace*{-0.3cm}\\
\Delta | \Gamma \vdash t_1 \elvis{} t_2 : \type{T}
\end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
\typerule{T-Method}\\
\begin{array}{@{}c}
\text{dom}(\Delta)=\ol{X} \quad \quad
\Delta' = \overline{\type{Y} : \bot .. \type{U}} \quad \quad
\Delta, \Delta' \vdash \ol{U}, \type{T}, \ol{T}\ \ok \quad \quad
\texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \set{\ldots} \\
\Delta, \Delta' | \overline{x:\type{T}}, \texttt{this} : \exptype{C}{\ol{X}} \vdash t:\type{S} \quad \quad
\Delta, \Delta' \vdash \type{S} <: \type{T} \quad \quad
\text{override}(\texttt{m}, \type{N}, \generics{\ol{Y \triangleleft U}}\ol{T} \to \type{T})
\\
\hline
\vspace*{-0.3cm}\\
\Delta \vdash \generics{\ol{Y \triangleleft U}} \type{T} \ \texttt{m}(\overline{\type{T} \ x}) = t \ \ok \ \texttt{in C}
\end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
\typerule{T-Class}\\
\begin{array}{@{}c}
\Delta = \overline{\type{X} : \bot .. \type{U}} \quad \quad
\Delta \vdash \ol{U}, \ol{T} \ \ok \quad \quad
\Delta \vdash \type{N} \ \ok \quad \quad
\Delta \vdash \ol{M} \ \ok \texttt{ in C}
\\
\hline
\vspace*{-0.3cm}\\
\texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M} } \ \ok
\end{array}
\end{array}$
\caption{T-Call and T-Field} \label{fig:tletexpr}
\end{figure}