314 lines
12 KiB
TeX
314 lines
12 KiB
TeX
\section{Syntax}
|
|
$
|
|
\begin{array}{lrcl}
|
|
\hline
|
|
\text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{W}} \\
|
|
\text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
|
|
\text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
|
|
\text{Type variable contexts} & \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
|
|
\text{Class declarations} & D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
|
|
\text{Method declarations} & \texttt{M} & ::= & \generics{\ol{X \triangleleft T}} \type{T} \ \texttt{m}(\overline{\type{T}\ x}) = t \\
|
|
\text{Terms} & t & ::= & x \\
|
|
& & \ \ | & \texttt{new} \ \exptype{C}{\ol{T}}(\overline{t})\\
|
|
& & \ \ | & t.f\\
|
|
& & \ \ | & t.\generics{\ol{T}}\texttt{m}(\overline{t})\\
|
|
& & \ \ | & t \elvis{} t\\
|
|
\text{Variable contexts} & \Gamma & ::= & \overline{x:\type{T}}\\
|
|
\hline
|
|
\end{array}
|
|
$
|
|
|
|
Each class type has a set of wildcard types $\overline{\Delta}$ attached to it.
|
|
The type $\wctype{\overline{\Delta}}{C}{\ol{T}}$ defines a set of wildcards $\overline{\Delta}$,
|
|
which can be used inside the type parameters $\ol{T}$.
|
|
|
|
\section{Type rules}
|
|
|
|
\begin{figure}[tp]
|
|
$\begin{array}{l}
|
|
\typerule{S-Refl}\\
|
|
\begin{array}{@{}c}
|
|
\Delta \vdash \type{T} <: \type{T}
|
|
\end{array}
|
|
\end{array}$
|
|
$\begin{array}{l}
|
|
\typerule{S-Trans}\\
|
|
\begin{array}{@{}c}
|
|
\Delta \vdash \type{S} <: \type{T}' \quad \quad
|
|
\Delta \vdash \type{T}' <: \type{T}
|
|
\\
|
|
\hline
|
|
\vspace*{-0.3cm}\\
|
|
\Delta \vdash \type{S} <: \type{T}
|
|
\end{array}
|
|
\end{array}$
|
|
$\begin{array}{l}
|
|
\typerule{S-Upper}\\
|
|
\begin{array}{@{}c}
|
|
\wildcard{X}{U}{L} \in \Delta \\
|
|
\vspace*{-0.9em}\\
|
|
\hline
|
|
\vspace*{-0.9em}\\
|
|
\Delta \vdash \type{X} <: \type{U}
|
|
\end{array}
|
|
\end{array}$
|
|
$\begin{array}{l}
|
|
\typerule{S-Lower}\\
|
|
\begin{array}{@{}c}
|
|
\wildcard{X}{U}{L} \in \Delta \\
|
|
\vspace*{-0.9em}\\
|
|
\hline
|
|
\vspace*{-0.9em}\\
|
|
\Delta \vdash \type{L} <: \type{X}
|
|
\end{array}
|
|
\end{array}$
|
|
\\[1em]
|
|
$\begin{array}{l}
|
|
\typerule{S-Extends}\\
|
|
\begin{array}{@{}c}
|
|
\texttt{class}\ \exptype{C}{\overline{\type{X} \triangleleft \type{U}}} \triangleleft \exptype{D}{\ol{S}} \ \{ \ldots \} \\
|
|
\ol{X} \cap \text{dom}(\Delta) = \emptyset
|
|
\\
|
|
\hline
|
|
\vspace*{-0.3cm}\\
|
|
\Delta \vdash \wctype{\Delta'}{C}{\ol{T}} <: \wctype{\Delta'}{D}{[\ol{T}/\ol{X}]\ol{S}}
|
|
\end{array}
|
|
\end{array}$
|
|
$\begin{array}{l}
|
|
\typerule{S-Exists}\\
|
|
\begin{array}{@{}c}
|
|
\Delta', \Delta \vdash [\ol{T}/\ol{\type{X}}]\ol{L} <: \ol{T} \quad \quad
|
|
\Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\
|
|
\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta, \Delta') \quad \quad
|
|
\text{dom}(\Delta') \cap \text{fv}(\wctype{\ol{\wildcard{X}{U}{L}}}{C}{\ol{S}}) = \emptyset
|
|
\\
|
|
\hline
|
|
\vspace*{-0.3cm}\\
|
|
\Delta \vdash \wctype{\Delta'}{C}{[\ol{T}/\ol{\type{X}}]\ol{S}} <:
|
|
\wctype{\ol{\wildcard{X}{U}{L}}}{C}{\ol{S}}
|
|
\end{array}
|
|
\end{array}$
|
|
\caption{Subtyping}\label{fig:subtyping}
|
|
\end{figure}
|
|
|
|
\begin{figure}[tp]
|
|
\begin{center}
|
|
$\begin{array}{l}
|
|
\typerule{WF-Bot}\\
|
|
\begin{array}{@{}c}
|
|
\Delta \vdash \bot \ \ok
|
|
\end{array}
|
|
\end{array}$
|
|
$\begin{array}{l}
|
|
\typerule{WF-Top}\\
|
|
\begin{array}{@{}c}
|
|
\Delta \vdash \ol{L}, \ol{U} \ \ok
|
|
\\
|
|
\hline
|
|
\vspace*{-0.3cm}\\
|
|
\Delta \vdash \overline{\wildcard{W}{U}{L}}.\texttt{Object}
|
|
\end{array}
|
|
\end{array}$
|
|
$\begin{array}{l}
|
|
\typerule{WF-Var}\\
|
|
\begin{array}{@{}c}
|
|
\wildcard{W}{U}{L} \in \Delta \quad \quad
|
|
\Delta \vdash \ol{L}, \ol{U} \ \ok
|
|
\\
|
|
\hline
|
|
\vspace*{-0.3cm}\\
|
|
\Delta \vdash \wildcard{W}{U}{L} \ \ok
|
|
\end{array}
|
|
\end{array}$
|
|
\\[1em]
|
|
$\begin{array}{l}
|
|
\typerule{WF-Class}\\
|
|
\begin{array}{@{}c}
|
|
\Delta' = \ol{\wildcard{W}{U}{L}} \quad \quad
|
|
\Delta, \Delta' \vdash \ol{T}, \ol{L}, \ol{U} \ \ok \quad \quad
|
|
\Delta, \Delta' \vdash \ol{L} <: \ol{U} \\
|
|
\Delta, \Delta' \vdash \ol{T} <: [\ol{T}/\ol{X}] \ol{U'} \quad \quad
|
|
\texttt{class}\ \exptype{C}{\ol{X \triangleleft U'}} \triangleleft \type{N} \ \{ \ldots \}
|
|
\\
|
|
\hline
|
|
\vspace*{-0.3cm}\\
|
|
\Delta \vdash \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}} \ \ok
|
|
\end{array}
|
|
\end{array}$
|
|
\end{center}
|
|
\caption{Well-formedness}\label{fig:well-formedness}
|
|
\end{figure}
|
|
%TODO: Proof that well-formed (ok) implies that a type is 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$.
|
|
|
|
%Not necessary!
|
|
% Additionally we do not allow nested wildcards. %TODO: Unify cannot create them (or does it?) What is when the input contains them
|
|
|
|
% The \unify{} algorithm is not capable of generating types like $\wctype{\rwildcard{X}, \wildcard{Y}{\bot}{\rwildcard{X}}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$.
|
|
% %But they could be created in intermidiate types (\ol{S}) in method calls by capture conversion:
|
|
% class WList<A> extends List<List<? extends A>>
|
|
% m(List<X> l) % TODO
|
|
% m(X.Wlist<X>) % S = Y^X.List<Y>
|
|
|
|
% X.WList<X> <. List<x?>
|
|
% X.List<Y^X.List<Y>> <. List<x?>
|
|
% x =. Y^X.List<Y>
|
|
|
|
% %TODO: do we need \Delta' \Delta \vdash T, L ,U ok ? or is \Delta \vdashh ... sufficient?
|
|
% %<A> m(List<? extends A> l)
|
|
% %This is important because it means different things maybe for the proof of our OK being more restrictive than "witnessed"
|
|
|
|
% % where can nested wildcards occur?
|
|
% WBox<X> extends Box<Box<? extends X>>
|
|
% WBox<?> => Y.WBox<Y> <: Y.Box<X^Y.Box<X>>
|
|
|
|
% Everything else regarding subtyping stays the same as in \cite{WildcardsNeedWitnessProtection}.
|
|
% \begin{lemma}
|
|
% If $\Delta \vdash $
|
|
% \end{lemma}
|
|
|
|
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.
|
|
|
|
\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}
|
|
|
|
|