710 lines
41 KiB
TeX
710 lines
41 KiB
TeX
\section{Soundness}
|
|
|
|
The differenciation of wildcard placeholders and normal type placeholders is vital for the soundness proof.
|
|
During a let statement the environment $\Delta$ is extended by capture converted wildcards,
|
|
but only for the scope of the body of the let statement.
|
|
The capture converted wildcards must not be used outside of the let statement.
|
|
This is ensured by two things:
|
|
The first is lemma \ref{lemma:freeVariablesOnlyTravelOneHop} which ensures that free variables only
|
|
travel one hop at the time through a constraint set.
|
|
And the second one is the fact that normal type placeholders never contain free variables.
|
|
|
|
\unify{} calculates solutions for all normal type placeholders.
|
|
Those are used for all untyped method's argument and return type.
|
|
A correct typing for method calls can be deducted from those type informations.
|
|
|
|
\begin{lemma}{Soundness:}\label{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}) = (\Delta', C)$
|
|
\item[then] $\Delta|\Gamma \vdash \texttt{e} : \sigma(\tv{a})$ where $\Delta = \Delta_u \cup \Delta'$
|
|
\end{description}
|
|
\end{lemma}
|
|
\textit{Proof:}
|
|
By structural induction over the expression $\texttt{e}$.
|
|
\begin{description}
|
|
\item[$\texttt{let}\ \texttt{x} = \texttt{t}_1 \ \texttt{in}\ \expr{t}_2$]
|
|
$\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ by lemma \ref{lemma:wildcardWellFormedness}.
|
|
$\Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok$ by lemma \ref{lemma:unifyWellFormedness}.
|
|
$\Delta|\Gamma \vdash \expr{t}_1: \sigma(\tv{e}_1)$ by assumption.
|
|
$\Delta \vdash \sigma(\tv{e}_1) <: \wcNtype{\Delta'}{N}$ by constraint $\tv{e}_1 \lessdot \tv{x}$ and lemma \ref{lemma:unifySoundness}.
|
|
The body of the let statement will only use the free variables provided by $\Delta$ and $\Delta'$.
|
|
We can prove this by lemma \ref{lemma:tvsNoFV} and the fact that the wildcard placeholders used generated the body of the let statement are not used outside of it.
|
|
Therefore we can say $\Delta,\Delta' | \Gamma, \expr{x}:\type{N} \vdash \expr{t}_2 : \sigma(\tv{e}_2)$ by assumption
|
|
and $\Delta, \Delta' \vdash \sigma(\tv{e}_2) <: \sigma(\tv{a})$ by lemma \ref{lemma:unifySoundness}
|
|
given the constraint $\tv{e}_2 \lessdot \tv{a}$.
|
|
\item[$\texttt{let}\ \texttt{x} = \texttt{t}_1 \ \texttt{in}\ \expr{x}.\texttt{f}$]
|
|
The let statement in the input is untyped and we have to create a let statement
|
|
$\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{t}_1 \ \texttt{in}\ \expr{x}.\texttt{f}$
|
|
that suffices the T-Let and T-Field type rules.
|
|
The case where no capture conversion is needed, because $\Delta' = \emptyset$, is trivial. Here the Let statement can be skipped entirely.
|
|
We investigate the case $\sigma(\tv{x}) = \wcNtype{\Delta}{N}$.
|
|
%Constraints t1 <. x, x <. C<a>, T <. t2
|
|
Let $\type{T}_1 = \wcNtype{\Delta'}{N} = \sigma(\tv{x})$, $\sigma(\tv{t_1}) = \type{T}_1$,
|
|
$\sigma(\tv{a}) = \type{T}_2$ then
|
|
\begin{itemize}
|
|
\item $\Delta | \Gamma \vdash t_1 : \type{T}_1$ by assumption
|
|
\item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ by constraint $\tv{t_1} \lessdot \tv{x}$ and lemma \ref{lemma:unifySoundness}
|
|
\item $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_2$
|
|
First we can say $\Delta | \Gamma \vdash \expr{x} : \type{N}$ by T-Var.
|
|
%$\Delta, \Delta', \overline{\Delta} \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
|
|
%and lemma \ref{lemma:unifySoundness}.
|
|
%The environment $\overline{\Delta}$ is not needed, because of lemma \ref{lemma:freeVariablesOnlyTravelOneHop}:
|
|
%$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$
|
|
%by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
|
|
%and lemmas \ref{lemma:unifySoundness} and \ref{lemma:freeVariablesOnlyTravelOneHop}.
|
|
By lemma \ref{lemma:unifyWellFormedness} and WF-Var we can deduct
|
|
$\text{fv}(\wcNtype{\Delta'}{N}) \subseteq \Delta$
|
|
and by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
|
|
and lemmas \ref{lemma:unifySoundness} and \ref{lemma:freeVariablesOnlyTravelOneHop}
|
|
we can finally say
|
|
$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$.
|
|
With the constraint $\tv{a} \doteq [\ol{\wtv{a}}/\ol{X}]\type{T}$
|
|
and $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) \in \text{fields}(\sigma(\exptype{C}{\ol{\wtv{a}}}))$ by F-Class
|
|
we proof $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_2$.
|
|
\item $\Delta, \Delta' \vdash \type{T}_2 <: \type{T}$ by constraint %TODO: Rename constraints
|
|
\end{itemize}
|
|
|
|
%generated constraints: t1 <. x, x <. N, T <. t2
|
|
We are allowed to use capture conversion for $\expr{v}$ here.
|
|
$\Delta \vdash \expr{v} : \sigma(\tv{a})$ by assumption.
|
|
$\Delta \vdash \sigma(\tv{a}) <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ and
|
|
$\Delta \vdash \type{U}_i <: \sigma(\tv{a})$,
|
|
because of the constraints $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$, $\tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$ and lemma \ref{lemma:unifySoundness}.
|
|
$\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$.
|
|
|
|
\item[$\text{let}\ \expr{x} = \expr{e} \ \text{in}\
|
|
\text{let}\ \overline{\expr{x} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x})$]
|
|
generates constraints $\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}},
|
|
\tv{r} \lessdot \tv{a}, \ol{\tv{x}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{r}, \ol{\wtv{b}} \lessdot \ol{N}$.
|
|
%We need to proof $\text{let}\ \expr{x} : \wcNtype{\Delta'}{N} = \expr{e}, \,
|
|
%\overline{\expr{x} : \wcNtype{\Delta'}{N} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x}) : \type{T}_2$
|
|
%where $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$, $\sigma(\tv{a}) = \type{T}_2$.
|
|
We omit the case where a capture conversion is not needed and
|
|
assume $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$.
|
|
We have to show T-Let and T-Call which leaves us with:
|
|
\begin{itemize}
|
|
\item $\Delta | \Gamma \vdash \expr{e} : \sigma(\tv{e})$ and $\Delta | \Gamma \vdash \overline{\expr{e} : \sigma(\tv{e})}$ by assumption
|
|
\item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ and $\Delta \vdash \overline{\type{T}_1 <: \wcNtype{\Delta'}{N}}$ by constraints $\tv{e} \lessdot \tv{x}$, $\overline{\tv{e} \lessdot \tv{x}}$ and lemma \ref{lemma:unifySoundness}
|
|
\item $\Delta, \Delta', \overline{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash \expr{x}.\texttt{m}(\ol{x}) : \sigma(\tv{r})$ by T-Call and lemma \ref{lemma:freeVariableScope}, because the following promises are satisfied.
|
|
Note: The lemma \ref{lemma:freeVariableScope} and the fact that the wildcard placeholders $\overline{\wtv{b}}$ are
|
|
solely used here guarantees that no other than the variables declared in $\Delta, \Delta', \overline{\Delta}$ appear in $\sigma'(\overline{\wtv{b}})$.
|
|
\begin{itemize}
|
|
\item $\generics{\ol{X} \triangleleft \ol{U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m})$ is given, otherwise the program fails at the constraint generation step.
|
|
\item $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$ by constraints $\ol{\wtv{b}} \lessdot [\ol{\wtv{b}}/\ol{X}]\ol{N}$ and lemma \ref{lemma:unifySoundness}
|
|
there must be some $\ol{S}$ satisfying this premise.
|
|
|
|
% what about we apply Unify again. With the known types. TODO: proof that unify can be applied again, with the capture converted versions of the constraints
|
|
%TODO: does not work because left side is a wildcard variable (maybe just change lemma soundness a bit)
|
|
\item
|
|
\end{itemize}
|
|
\end{itemize}
|
|
\item[$\texttt{v}.\texttt{m}(\ol{v})$]
|
|
Proof is analog to field access, except the $\Delta \vdash \ol{S}\ \ok$ premise.
|
|
We know that $\unify{}(\Delta, [\overline{\wtv{b}}/\ol{Y}]\set{
|
|
\ol{\tv{e}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a},
|
|
\ol{Y} \lessdot \ol{N} } \cup C) = (\Delta', \sigma)$
|
|
and if we assume $\sigma(\ol{\tv{e}}) = \ol{\wcNtype{\Delta}{N'}}$
|
|
then the call to $\unify{}(\Delta \cup \overline{\Delta}, [\overline{\ntv{b}}/\ol{Y}]\set{
|
|
\ol{N'} \lessdot \ol{T}, \type{T} \lessdot \tv{a},
|
|
\ol{Y} \lessdot \ol{N} } \cup C)$ succeeds with $\overline{\ntv{b}}$ being normal placeholders this time,
|
|
which proofs $\Delta \vdash \ol{S}\ \ok$ via lemma \ref{lemma:unifyWellFormedness}.
|
|
%TODO: why does this call succeed?
|
|
% 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}
|
|
|
|
|
|
During the unification process free variables can only move one hop at a time.
|
|
Free variables originate from capture constraints.
|
|
By applying the capture rule to a constraint of the form $\wcNtype{\Delta}{N} \lessdotCC \type{T}$ the variables declared in $\Delta$
|
|
are now free in the constraint $\type{N} \lessdot \type{T}$.
|
|
The other way of free variables traveling into a constraint is by substitution.
|
|
This is only possible if a constraint contains wildcard placeholders.
|
|
And only free variables which reside in the same constraint as a wildcard placeholders have the possibility of being set in.
|
|
|
|
This effect is transitive. Free variables travel from constraint to constraint.
|
|
If there is no connection of constraints containing wildcard type placeholders between a free variable and a constraint,
|
|
then free variables cannot travel there.
|
|
|
|
\begin{lemma}
|
|
Free variables travel only
|
|
\end{lemma}
|
|
|
|
\begin{lemma}{Free variables}\label{lemma:freeVariableScope}
|
|
Free variables never leave their scope.
|
|
If a set of constraints does not share a single wildcard type placeholder with the rest of the constraint set,
|
|
then it will never contain free variables used outside of it.
|
|
$(\Delta, \sigma) = \unify{}(\Delta_{in}, C \cup C')$
|
|
|
|
and $\text{wtv}(C') \cap \text{wtv}(C) = \emptyset$
|
|
and $\overline{\sigma(\tv{x}) = \wcNtype{\Delta}{N}}$
|
|
|
|
then $\Delta, \Delta', \overline{\Delta}$ are all the variables used in $C'$.
|
|
\end{lemma}
|
|
\textit{Proof:} This is due to free variables only travel inbetween constraints and themselves via substitution.
|
|
|
|
If $\type{S} \lessdotCC \type{T}$ spawns free variables, they will be contained within the reach of the wildcard type placeholders
|
|
used for the method call.
|
|
No other free variables can move into that scope.
|
|
With this lemma we can further proof that during a method call only the generated free variables are used.
|
|
|
|
% \begin{lemma}
|
|
% Free variables never leave their scope.
|
|
% $C' = \set{
|
|
% \overline{\tv{e} \lessdot \tv{x}}, \overline{\tv{x} \lessdotCC \tv{x}},
|
|
% \overline{\tv{r} \lessdot \tv{a}}
|
|
% }$
|
|
% $(\Delta, \sigma) = \unify{}(\Delta_{in}, C \cup C')$
|
|
|
|
% and $\text{wtv}(C') \cap \text{wtv}(C) = \emptyset$
|
|
% and $\overline{\sigma(\tv{x}) = \wcNtype{\Delta}{N}}$
|
|
|
|
% then $\Delta, \Delta', \overline{\Delta}$ are all the variables used in $C'$.
|
|
% %if a wildcard type placeholder does not appear anywhere else, then only the free variables of its scope can be used for him
|
|
% \end{lemma}
|
|
|
|
% \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.
|
|
|
|
|
|
\begin{lemma}\label{lemma:wildcardWellFormedness}
|
|
\unify{} generates well-formed existential types
|
|
\begin{description}
|
|
\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$
|
|
\item[and] $\forall \wcNtype{\Delta''}{N} \in C: \text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
|
|
\item[and] $\sigma(\tv{a}) = \wcNtype{\Delta'}{N}$
|
|
%\item[then] $\Delta \vdash \ol{L <: U}$ and $\Delta \vdash \ol{U <: U'}$ % (with U' being upper limit by class definition)
|
|
\item[then] $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
|
|
\end{description}
|
|
\end{lemma}
|
|
\textit{Proof} is straightforward induction over the transformation rules of \unify{}
|
|
under the assumption that all supplied existential types are satisfying the premise.
|
|
All parts of \unify{} that generate wildcard types always spawn types $\wcNtype{\Delta'}{N}$
|
|
with $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$.
|
|
Only the \rulename{Adapt} rule is able to produce types neglecting the premise,
|
|
but is immediately corrected by the \rulename{Trim} rule.
|
|
|
|
% 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} by induction on subtyping rules in figure \ref{fig:subtyping}
|
|
|
|
% \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:wildcardsStayInScope}
|
|
% Free variables can only hop to another constraint if they share the same wildcard placeholder.
|
|
% \begin{description}
|
|
% \item[If] $(\sigma, \Delta) = \unify{} (\Delta', C \cup \set{\wcNtype{\Delta'}{N} \lessdot \tv{a}})$
|
|
% \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}
|
|
|
|
|
|
|
|
%TODO: use this to proof soundness. Wildcard placeholders are not shared with other constraints and therefore only the wildcards generated by capture conversion are used in a let statement.
|
|
|
|
% \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'$ 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}{\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'} })$
|
|
with $\text{wtv}(\ol{S}) = \emptyset$ and $\text{wtv}(\ol{T}) = \emptyset$
|
|
\item[Then] $\Delta, \Delta' \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
|
|
\item[and] either $\Delta, \Delta' \vdash \overline{\sigma(\type{S'}) <: \sigma(\type{T'})}$
|
|
or $\Delta, \Delta', \overline{\Delta} \vdash \overline{\sigma'(\type{S'}) <: \sigma(\type{T'})}$
|
|
with the capture converted substitution $\sigma' = \set{ \tv{a} \mapsto \type{N} \mid \tv{a} \mapsto \wcNtype{\Delta}{N} \in \sigma}$
|
|
and $\overline{\Delta} = \set{\Delta \mid \tv{a} \mapsto \wcNtype{\Delta}{N} \in \sigma }$
|
|
|
|
% 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]
|
|
To proof $\wctype{\Delta}{C}{\ol{S}} <: \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{T}}$
|
|
we have to show S-Exists for some $\Delta''$ and $\ol{T} = \sigma(\overline{\wtv{a}})$:
|
|
\begin{itemize}
|
|
\item $\Delta'' \vdash \subst{\ol{T}}{\ol{X}}\ol{L} <: \ol{T}$ by assumption and $\subst{\ol{\wtv{a}}}{\ol{X}}\ol{L} \lessdot \ol{\wtv{a}}$
|
|
\item $\Delta'' \vdash \ol{T} <: \subst{\ol{T}}{\ol{X}}\ol{U}$ by assumption and $\ol{\wtv{a}} \lessdot \subst{\ol{\wtv{a}}}{\ol{X}}\ol{L}$
|
|
\item $\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta'', \Delta')$ by setting $\Delta''$ accordingly
|
|
\end{itemize}
|
|
|
|
%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 \text{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}
|
|
|
|
\begin{lemma}
|
|
\label{lemma:freeVariablesOnlyTravelOneHop}
|
|
A constraint $\tv{a} \lessdotCC \type{T}$ or $\tv{a} \lessdot \type{T}$ implies that
|
|
$\text{fv}(\sigma(\type{T})) \subseteq \text{fv}(\sigma(\tv{a}))$.
|
|
Only free variables, which are part of the left side are used on the right side.
|
|
\end{lemma}
|
|
|
|
% \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}
|
|
|