Cleanup, Fixes and Restructuring
This commit is contained in:
parent
7e1ef7b3c1
commit
c86dc891f3
@ -112,51 +112,26 @@
|
||||
|
||||
\input{tRules}
|
||||
|
||||
\input{typeinference}
|
||||
|
||||
%\input{tiRules}
|
||||
|
||||
\input{constraints}
|
||||
|
||||
\input{Unify}
|
||||
|
||||
\section{Limitations}
|
||||
|
||||
This example does not work:
|
||||
|
||||
\begin{minipage}{0.35\textwidth}
|
||||
\begin{verbatim}
|
||||
class Example{
|
||||
<A> Pair<A,A> make(List<A> l){...}
|
||||
<A> bool compare(Pair<A,A> p){...}
|
||||
|
||||
bool test(List<?> l){
|
||||
return compare(make(l));
|
||||
}
|
||||
}
|
||||
\end{verbatim}
|
||||
\end{minipage}%
|
||||
\hfill
|
||||
\begin{minipage}{0.55\textwidth}
|
||||
\begin{constraintset}
|
||||
\textbf{Constraints:}\\
|
||||
$
|
||||
\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{x}}, \\
|
||||
\exptype{Pair}{\wtv{x},\wtv{x}} \lessdot \tv{r}, \\
|
||||
\tv{r} \lessdot \exptype{Pair}{\tv{z}, \tv{z}}%,\\
|
||||
%\tv{y} \lessdot \tv{m}
|
||||
$\\
|
||||
\end{constraintset}
|
||||
\end{minipage}
|
||||
|
||||
\include{relatedwork}
|
||||
|
||||
\input{conclusion}
|
||||
|
||||
\include{soundness}
|
||||
%\include{termination}
|
||||
\include{relatedwork}
|
||||
|
||||
\bibliography{martin}
|
||||
|
||||
\appendix
|
||||
|
||||
\include{soundness}
|
||||
\include{helpers}
|
||||
%\include{examples}
|
||||
%\input{exampleWildcardParameter}
|
||||
%\input{commonPatternsProof}
|
||||
|
@ -9,7 +9,56 @@
|
||||
%TODO: how are the challenges solved: Describe this in the last chapter with examples!
|
||||
\section{Soundness}\label{sec:soundness}
|
||||
|
||||
\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}
|
||||
|
||||
To prove soundness we have to show two things.
|
||||
The vital parts are method calls and field access.
|
||||
The generated constraints have to resemble the \TamedFJ{}'s type system.
|
||||
|
||||
\section{Completeness}\label{sec:completeness}
|
||||
We couldn't verify it with an implementation yet, but we assume atleast the same functionality
|
||||
as the global type inference algorithm for Featherweight Java without Wildcards \cite{TIforFGJ}.
|
||||
|
||||
|
||||
\begin{example} Limitation:
|
||||
|
||||
This example does not work:
|
||||
|
||||
\begin{minipage}{0.35\textwidth}
|
||||
\begin{verbatim}
|
||||
class Example{
|
||||
<A> Pair<A,A> make(List<A> l){...}
|
||||
<A> bool compare(Pair<A,A> p){...}
|
||||
|
||||
bool test(List<?> l){
|
||||
return compare(make(l));
|
||||
}
|
||||
}
|
||||
\end{verbatim}
|
||||
\end{minipage}%
|
||||
\hfill
|
||||
\begin{minipage}{0.55\textwidth}
|
||||
\begin{constraintset}
|
||||
\textbf{Constraints:}\\
|
||||
$
|
||||
\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{x}}, \\
|
||||
\exptype{Pair}{\wtv{x},\wtv{x}} \lessdot \tv{r}, \\
|
||||
\tv{r} \lessdot \exptype{Pair}{\tv{z}, \tv{z}}%,\\
|
||||
%\tv{y} \lessdot \tv{m}
|
||||
$\\
|
||||
\end{constraintset}
|
||||
\end{minipage}
|
||||
\end{example}
|
||||
|
||||
The algorithm can find a solution to every program which the Unify by Plümicke finds
|
||||
a correct solution aswell.
|
||||
It will not infer intermediat type like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X},\rwildcard{X}}$.
|
||||
|
102
constraints.tex
102
constraints.tex
@ -1,70 +1,3 @@
|
||||
\subsection{Capture Constraints}
|
||||
%TODO: General Capture Constraint explanation
|
||||
|
||||
Capture Constraints are bound to a variable.
|
||||
For example a let statement like \lstinline{let x = v in x.get()} will create the capture constraint
|
||||
$\tv{x} \lessdotCC_x \exptype{List}{\wtv{a}}$.
|
||||
This time we annotated the capture constraint with an $x$ to show its relation to the variable \texttt{x}.
|
||||
Let's do the same with the constraints generated by the \texttt{concat} method invocation in listing \ref{lst:faultyConcat},
|
||||
creating the constraints \ref{lst:sameConstraints}.
|
||||
|
||||
\begin{figure}
|
||||
\begin{minipage}[t]{0.49\textwidth}
|
||||
\begin{lstlisting}[caption=Faulty Method Call,label=lst:faultyConcat]{tamedfj}
|
||||
List<?> v = ...;
|
||||
|
||||
let x = v in
|
||||
let y = v in
|
||||
concat(x, y) // Error!
|
||||
\end{lstlisting}\end{minipage}
|
||||
\hfill
|
||||
\begin{minipage}[t]{0.49\textwidth}
|
||||
\begin{lstlisting}[caption=Annotated constraints,mathescape=true,style=constraints,label=lst:sameConstraints]
|
||||
$\tv{x} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{x}$
|
||||
$\tv{y} \lessdotCC_\texttt{y} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{y}$
|
||||
\end{lstlisting}
|
||||
\end{minipage}
|
||||
\end{figure}
|
||||
|
||||
|
||||
During the \unify{} process it could happen that two syntactically equal capture constraints evolve,
|
||||
but they are not the same because they are each linked to a different let introduced variable.
|
||||
In this example this happens when we substitute $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\tv{x}$ and $\tv{y}$
|
||||
resulting in:
|
||||
%For example by substituting $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{x}]$ and $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{y}]$:
|
||||
\begin{displaymath}
|
||||
\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_x \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_y \exptype{List}{\wtv{a}}
|
||||
\end{displaymath}
|
||||
Thanks to the original annotations we can still see that those are different constraints.
|
||||
After \unify{} uses the \rulename{Capture} rule on those constraints
|
||||
it gets obvious that this constraint set is unsolvable:
|
||||
\begin{displaymath}
|
||||
\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}},
|
||||
\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}
|
||||
\end{displaymath}
|
||||
|
||||
%In this paper we do not annotate capture constraint with their source let statement.
|
||||
The rest of this paper will not annotate capture constraints with variable names.
|
||||
Instead we consider every capture constraint as distinct to other capture constraints even when syntactically the same,
|
||||
because we know that each of them originates from a different let statement.
|
||||
\textit{Hint:} An implementation of this algorithm has to consider that seemingly equal capture constraints are actually not the same
|
||||
and has to allow doubles in the constraint set.
|
||||
|
||||
% %We see the equality relation on Capture constraints is not reflexive.
|
||||
% A capture constraint is never equal to another capture constraint even when structurally the same
|
||||
% ($\type{T} \lessdotCC \type{S} \neq \type{T} \lessdotCC \type{S}$).
|
||||
% This is necessary to solve challenge \ref{challenge:1}.
|
||||
% A capture constraint is bound to a specific let statement.
|
||||
|
||||
\textit{Note:}
|
||||
In the special case \lstinline{let x = v in concat(x,x)} the constraints would look like
|
||||
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}},
|
||||
\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
|
||||
and we could actually delete one of them without loosing information.
|
||||
But this case will never occur in our algorithm, because the let
|
||||
statements for our input programs are generated by transformation to ANF (see \ref{sec:anfTransformation}).
|
||||
|
||||
|
||||
|
||||
\section{Constraint generation}\label{chapter:constraintGeneration}
|
||||
% Method names are not unique.
|
||||
@ -78,11 +11,6 @@ statements for our input programs are generated by transformation to ANF (see \r
|
||||
% But it can be easily adapted to Featherweight Java or Java.
|
||||
% We add T <. a for every return of an expression anyway. If anything returns a Generic like X it is not directly used in a method call like X <c T
|
||||
|
||||
\begin{description}
|
||||
\item[input] \TamedFJ{} program in A-Normal form
|
||||
\item[output] Constraints
|
||||
\end{description}
|
||||
|
||||
The constraint generation works on the \TamedFJ{} language.
|
||||
This step is mostly the same as in \cite{TIforFGJ} except for field access and method invocation.
|
||||
We will focus on those two parts where also the new capture constraints and wildcard type placeholders are introduced.
|
||||
@ -146,7 +74,7 @@ $\begin{array}{lrcl}
|
||||
& \anf{\texttt{let}\ x = \expr{t}_1 \ \texttt{in}\ \expr{t}_2} & = & \texttt{let}\ x = \anf{\expr{t}_1} \ \texttt{in}\ \anf{\expr{t}_2}
|
||||
\end{array}$
|
||||
\end{center}
|
||||
\caption{ANF Transformation}\label{fig:anfTransformation}
|
||||
\caption{ANF Transformation $\tau$}\label{fig:anfTransformation}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}
|
||||
@ -216,7 +144,7 @@ Those type variables count as regular types and can be held by normal type place
|
||||
\begin{figure}[tp]
|
||||
\begin{gather*}
|
||||
\begin{array}{@{}l@{}l}
|
||||
\fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\overline{\type{X} \triangleleft \type{N}}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\
|
||||
\fjtype & ({\mtypeEnvironment }, \mathtt{class } \ \exptype{C}{\overline{\type{X} \triangleleft \type{N}}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\
|
||||
& \begin{array}{ll@{}l}
|
||||
\textbf{let} & \ol{\methodAssumption} =
|
||||
\set{ \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \mid
|
||||
@ -238,11 +166,11 @@ Those type variables count as regular types and can be held by normal type place
|
||||
|
||||
\begin{displaymath}
|
||||
\begin{array}{@{}l@{}l}
|
||||
\typeExpr{} &({\mtypeEnvironment} , \texttt{e}.\texttt{f}, \tv{a}) = \\
|
||||
\typeExpr{} &({\mtypeEnvironment}, \Gamma , \texttt{e}.\texttt{f}, \tv{a}) = \\
|
||||
& \begin{array}{ll}
|
||||
\textbf{let}
|
||||
& \tv{r} \ \text{fresh} \\
|
||||
& \consSet_R = \typeExpr({\mtypeEnvironment}, \texttt{e}, \tv{r})\\
|
||||
& \consSet_R = \typeExpr({\mtypeEnvironment}, \Gamma, \texttt{e}, \tv{r})\\
|
||||
& \constraint = \begin{array}[t]{@{}l@{}l}
|
||||
\orCons\set{
|
||||
\set{ &
|
||||
@ -261,12 +189,12 @@ Those type variables count as regular types and can be held by normal type place
|
||||
|
||||
\begin{displaymath}
|
||||
\begin{array}{@{}l@{}l}
|
||||
\typeExpr{} &({\mtypeEnvironment} , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2, \tv{a}) = \\
|
||||
\typeExpr{} &({\mtypeEnvironment}, \Gamma , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2, \tv{a}) = \\
|
||||
& \begin{array}{ll}
|
||||
\textbf{let}
|
||||
& \tv{e}_1, \tv{e}_2, \tv{x} \ \text{fresh} \\
|
||||
& \consSet_1 = \typeExpr({\mtypeEnvironment}, \expr{e}_1, \tv{e}_1)\\
|
||||
& \consSet_2 = \typeExpr({\mtypeEnvironment} \cup \set{\expr{x} : \tv{x}}, \expr{e}_2, \tv{e}_2)\\
|
||||
& \consSet_1 = \typeExpr({\mtypeEnvironment}, \Gamma, \expr{e}_1, \tv{e}_1)\\
|
||||
& \consSet_2 = \typeExpr({\mtypeEnvironment } \cup \set{\expr{x} : \tv{x}}, \expr{e}_2, \tv{e}_2)\\
|
||||
& \constraint =
|
||||
\set{
|
||||
\tv{e}_1 \lessdot \tv{x}, \tv{e}_2 \lessdot \tv{a}
|
||||
@ -279,7 +207,7 @@ Those type variables count as regular types and can be held by normal type place
|
||||
|
||||
\begin{displaymath}
|
||||
\begin{array}{@{}l@{}l}
|
||||
\typeExpr{} & ({\mtypeEnvironment} , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\
|
||||
\typeExpr{} & ({\mtypeEnvironment}, \Gamma , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\
|
||||
& \begin{array}{ll}
|
||||
\textbf{let}
|
||||
& \tv{r}, \ol{\tv{r}} \text{ fresh} \\
|
||||
@ -289,7 +217,7 @@ Those type variables count as regular types and can be held by normal type place
|
||||
\mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T}) \\
|
||||
& \mathbf{where}\ \begin{array}[t]{l}
|
||||
\expr{v}, \ol{v} : \ol{S} \in \localVarAssumption \\
|
||||
\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T} \in {\mtypeEnvironment}
|
||||
\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T} \in {\mtypeEnvironment }
|
||||
\end{array}
|
||||
|
||||
\end{array}
|
||||
@ -390,12 +318,12 @@ cannot be used anywhere else then inside the constraints generated by the method
|
||||
|
||||
\begin{displaymath}
|
||||
\begin{array}{@{}l@{}l}
|
||||
\typeExpr{} &({\mtypeEnvironment} , e_1 \elvis{} e_2, \tv{a}) = \\
|
||||
\typeExpr{} &({\mtypeEnvironment}, \Gamma , e_1 \elvis{} e_2, \tv{a}) = \\
|
||||
& \begin{array}{ll}
|
||||
\textbf{let}
|
||||
& \tv{r}_1, \tv{r}_2 \ \text{fresh} \\
|
||||
& \consSet_1 = \typeExpr({\mtypeEnvironment}, e_1, \tv{r}_2)\\
|
||||
& \consSet_2 = \typeExpr({\mtypeEnvironment}, e_2, \tv{r}_2)\\
|
||||
& \consSet_1 = \typeExpr({\mtypeEnvironment}, \Gamma, e_1, \tv{r}_2)\\
|
||||
& \consSet_2 = \typeExpr({\mtypeEnvironment}, \Gamma, e_2, \tv{r}_2)\\
|
||||
{\mathbf{in}} & {
|
||||
\consSet_1 \cup \consSet_2 \cup
|
||||
\set{\tv{r}_1 \lessdot \tv{a}, \tv{r}_2 \lessdot \tv{a}}}
|
||||
@ -406,18 +334,18 @@ cannot be used anywhere else then inside the constraints generated by the method
|
||||
%We could skip wfresh here:
|
||||
\begin{displaymath}
|
||||
\begin{array}{@{}l@{}l}
|
||||
\typeExpr{} &({\mtypeEnvironment} , x, \tv{a}) =
|
||||
\typeExpr{} &({\mtypeEnvironment}, \Gamma , x, \tv{a}) =
|
||||
\mtypeEnvironment(x)
|
||||
\end{array}
|
||||
\end{displaymath}
|
||||
|
||||
\begin{displaymath}
|
||||
\begin{array}{@{}l@{}l}
|
||||
\typeExpr{} &({\mtypeEnvironment} , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\
|
||||
\typeExpr{} &({\mtypeEnvironment}, \Gamma , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\
|
||||
& \begin{array}{ll}
|
||||
\textbf{let}
|
||||
& \ol{\ntv{r}}, \ol{\ntv{a}} \ \text{fresh} \\
|
||||
& \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\ntv{r}}) \\
|
||||
& \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \Gamma, \overline{e}, \ol{\ntv{r}}) \\
|
||||
& C = \set{\ol{\ntv{r}} \lessdot [\ol{\ntv{a}}/\ol{X}]\ol{T}, \ol{\ntv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\
|
||||
{\mathbf{in}} & {
|
||||
\overline{\consSet} \cup
|
||||
|
34
helpers.tex
Normal file
34
helpers.tex
Normal file
@ -0,0 +1,34 @@
|
||||
|
||||
\section{Additional Functions}
|
||||
\begin{description}
|
||||
\item[$\tph{}$] returns all type placeholders inside a given type.
|
||||
|
||||
\textit{Example:} $\tph(\wctype{\wildcard{X}{\tv{a}}{\bot}}{Pair}{\wtv{b},\rwildcard{X}}) = \set{\tv{a}, \wtv{b}}$
|
||||
|
||||
%\textbf{Wildcard renaming}\\
|
||||
\item[Wildcard renaming:]
|
||||
The \rulename{Reduce} rule separates wildcards from their environment.
|
||||
At this point each wildcard gets a new and unique name.
|
||||
To only rename the respective wildcards the reduce rule renames wildcards up to alpha conversion:
|
||||
($[\ol{C}/\ol{B}]$ in the \rulename{reduce} rule)
|
||||
\begin{align*}
|
||||
[\type{A}/\type{B}]\type{B} &= \type{A} \\
|
||||
[\type{A}/\type{B}]\type{C} &= \type{C} & \text{if}\ \type{B} \neq \type{C}\\
|
||||
[\type{A}/\type{B}]\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} &= \wcNtype{\overline{\wildcard{X}{[\type{A}/\type{B}]\type{U}}{[\type{A}/\type{B}]\type{L}}}}{[\type{A}/\type{B}]N} & \text{if}\ \type{B} \notin \overline{\rwildcard{X}} \\
|
||||
[\type{A}/\type{B}]\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} &= \wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} & \text{if}\ \type{B} \in \overline{\rwildcard{X}} \\
|
||||
\end{align*}
|
||||
\item[Free Variables:]
|
||||
The $\text{fv}$ function assumes every wildcard type variable to be a free variable aswell.
|
||||
% TODO: describe a function which determines free variables? or do an example?
|
||||
\begin{align*}
|
||||
\text{fv}(\rwildcard{A}) &= \set{ \rwildcard{A} } \\
|
||||
\text{fv}(\tv{a}) &= \emptyset \\
|
||||
%\text{fv}(\wtv{a}) &= \set{\wtv{a}} \\
|
||||
\text{fv}(\wctype{\Delta}{C}{\ol{T}}) &= \set{\text{fv}(\type{T}) \mid \type{T} \in \ol{T}} / \text{dom}(\Delta) \\
|
||||
\end{align*}
|
||||
|
||||
\item[Fresh Wildcards:]
|
||||
$\text{fresh}\ \overline{\wildcard{A}{\tv{u}}{\tv{l}}}$ generates fresh wildcards.
|
||||
The new names $\ol{A}$ are fresh, aswell as the type variables $\ol{\tv{u}}$ and $\ol{\tv{l}}$,
|
||||
which are used for the upper and lower bounds.
|
||||
\end{description}
|
341
introduction.tex
341
introduction.tex
@ -383,344 +383,3 @@ let l1' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) =
|
||||
% Polymorphic method calls need to be wrapped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
|
||||
% In Java this is done implicitly in a process called capture conversion (as proposed in Wild FJ \cite{WildFJ}).
|
||||
|
||||
|
||||
\section{Global Type Inference Algorithm}
|
||||
\label{sec:glob-type-infer}
|
||||
|
||||
This section gives an overview of the global type inference algorithm
|
||||
with examples and identifies the challenges that we had to overcome in
|
||||
the design of the algorithm.
|
||||
|
||||
\begin{figure}[h]
|
||||
\begin{minipage}{0.49\textwidth}
|
||||
\begin{lstlisting}[style=tfgj, caption=Valid Java program, label=lst:addExample]
|
||||
<A> List<A> add(List<A> l, A v)
|
||||
|
||||
List<? super String> l = ...;
|
||||
add(l, "String");
|
||||
\end{lstlisting}
|
||||
\end{minipage}\hfill
|
||||
\begin{minipage}{0.49\textwidth}
|
||||
\begin{lstlisting}[style=tamedfj, caption=\TamedFJ{} representation, label=lst:addExampleLet]
|
||||
<A> List<A> add(List<A> l, A v)
|
||||
List<? super String> l = ...;
|
||||
let v:(*@$\tv{v}$@*) = l
|
||||
in add(v, "String");
|
||||
\end{lstlisting}
|
||||
\end{minipage}\\
|
||||
\begin{minipage}{0.49\textwidth}
|
||||
\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:addExampleCons]
|
||||
(*@$\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}} \lessdot \tv{v}$@*)
|
||||
(*@$\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$@*)
|
||||
(*@$\type{String} \lessdot \wtv{a}$@*)
|
||||
\end{lstlisting}
|
||||
\end{minipage}\hfill
|
||||
\begin{minipage}{0.49\textwidth}
|
||||
\begin{lstlisting}[style=letfj, caption=Type solution, label=lst:addExampleSolution]
|
||||
<A> List<A> add(List<A> l, A v)
|
||||
List<? super String> l = ...;
|
||||
let l2:(*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l
|
||||
in <X>add(l2, "String");
|
||||
\end{lstlisting}
|
||||
\end{minipage}
|
||||
\end{figure}
|
||||
|
||||
% \begin{description}
|
||||
% \item[input] \tifj{} program
|
||||
% \item[output] type solution
|
||||
% \item[postcondition] the type solution applied to the input must yield a valid \letfj{} program
|
||||
% \end{description}
|
||||
|
||||
%Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
|
||||
Listings~\ref{lst:addExample}, \ref{lst:addExampleLet}, \ref{lst:addExampleCons}, and
|
||||
\ref{lst:addExampleSolution} showcase the global type inference algorithm step by step.
|
||||
In the Java code in Listing~\ref{lst:addExample}, the type of variable
|
||||
\texttt{l} is an existential type so that it has to undergo a capture conversion
|
||||
before being passed to a method call.
|
||||
To this end we convert the program to A-Normal form (Listing~\ref{lst:addExampleLet}),
|
||||
which introduces a let statement defining a new variable \texttt{v}.
|
||||
As the type of \texttt{v} is unknown, the algorithm puts a type
|
||||
placeholder $\tv{v}$ for the type of \texttt{v} before generating constraints (see Listing~\ref{lst:addExampleCons}).
|
||||
These constraints mirror the typing rules of the \TamedFJ{} calculus (section~\ref{sec:tifj}).
|
||||
% During the constraint generation step the type of the variable \texttt{v} is unknown
|
||||
% and given the type placeholder $\tv{v}$.
|
||||
The call to \texttt{add} generates the \emph{capture constraint} $\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$.
|
||||
This constraint ($\lessdotCC$) is a kind of subtype constraint, which additionally
|
||||
expresses that the left side of the constraint is subject to a capture conversion.
|
||||
Next, the unification algorithm \unify{} (section~\ref{sec:unify}) solves the constraints.
|
||||
Initially, no type is assigned to $\tv{v}$.
|
||||
% During the course of \unify{} more and more types emerge.
|
||||
As soon as a concrete type for $\tv{v}$ is appears during constraint
|
||||
solving, \unify{} can conduct a capture conversion if needed.
|
||||
%The constraints where this is possible are marked as capture constraints.
|
||||
In this example, $\tv{v}$ will be set to
|
||||
$\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$
|
||||
leaving us with the following constraints:
|
||||
|
||||
\begin{displaymath}
|
||||
\prftree[r]{Capture}{
|
||||
\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}, \, \type{String} \lessdotCC \wtv{a}
|
||||
}{
|
||||
\wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
|
||||
}
|
||||
\end{displaymath}
|
||||
|
||||
%Capture Constraints $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ allow for a capture conversion,
|
||||
%which converts a constraint of the form $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ to $(\exptype{C}{\rwildcard{X}} \lessdot \type{T})$
|
||||
The constraint $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$
|
||||
allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
|
||||
The captured wildcard $\rwildcard{X}$ gets a fresh name \texttt{Y}, which is stored in the wildcard environment of the \unify{} algorithm.
|
||||
Substituting \texttt{Y} for $\wtv{a}$ yields the constraints almost
|
||||
solved: $\exptype{List}{\rwildcard{Y}} \lessdot
|
||||
\exptype{List}{\rwildcard{Y}}$, $\type{String} \lessdot
|
||||
\rwildcard{Y}$.
|
||||
The first constraint is obviously satisfied and $\type{String} \lessdot \rwildcard{Y}$ is satisfied
|
||||
because $\rwildcard{Y}$ has $\type{String}$ as lower bound.
|
||||
|
||||
|
||||
A correct Featherweight Java program including all type annotations and an explicit capture conversion via let statement is shown in Listing \ref{lst:addExampleSolution}.
|
||||
This program can be deduced from the solution of the \unify{} algorithm presented in Section~\ref{sec:unify}.
|
||||
In the body of the let statement the type $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$
|
||||
becomes $\exptype{List}{\rwildcard{X}}$ and the capture converted wildcard $\wildcard{X}{\type{Object}}{\type{String}}$ can be used as
|
||||
a type parameter of the call \texttt{<X>add(v, "String")}.
|
||||
|
||||
% The input to our type inference algorithm is a modified version of the calculus in \cite{WildcardsNeedWitnessProtection} (see chapter \ref{sec:tifj}).
|
||||
% First \fjtype{} (see section \ref{chapter:constraintGeneration}) generates constraints
|
||||
% and afterwards \unify{} (section \ref{sec:unify}) computes a solution for the given constraint set.
|
||||
% Constraints consist out of subtype constraints $(\type{T} \lessdot \type{T})$ and capture constraints $(\type{T} \lessdotCC \type{T})$.
|
||||
% \textit{Note:} a type $\type{T}$ can either be a named type, a type placeholder or a wildcard type placeholder.
|
||||
% A subtype constraint is satisfied if the left side is a subtype of the right side according to the rules in figure \ref{fig:subtyping}.
|
||||
% \textit{Example:} $\exptype{List}{\ntv{a}} \lessdot \exptype{List}{\type{String}}$ is fulfilled by replacing type placeholder $\ntv{a}$ with the type $\type{String}$.
|
||||
% Subtype constraints and type placeholders act the same as the ones used in \emph{Type Inference for Featherweight Generic Java} \cite{TIforFGJ}.
|
||||
% The novel capture constraints and wildcard placeholders are needed for method invocations involving wildcards.
|
||||
|
||||
% The central piece of this type inference algorithm, the \unify{} process, is described with implication rules (chapter \ref{sec:unify}).
|
||||
% We try to keep the branching at a minimal amount to improve runtime behavior.
|
||||
% Also the transformation steps of the \unify{} algorithm are directly related to the subtyping rules of our calculus.
|
||||
% There are no informal parts in our \unify{} algorithm.
|
||||
% It solely consist out of transformation rules which are bound to simple checks.
|
||||
|
||||
\subsection{Challenges}\label{challenges}
|
||||
%TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
|
||||
|
||||
% Wildcards are not reflexive.
|
||||
% ( on the equals property ), every wildcard has to be capture converted when leaving its scope
|
||||
|
||||
% do not substitute free type variables
|
||||
|
||||
Global type inference for Featherweight Generic Java without wildcards
|
||||
has been considered elsewher \cite{TIforFGJ}.
|
||||
Adding wildcards to the calculus created new problems, which have not
|
||||
been recognized by existing work on type unification for Java with wildcards~\cite{plue09_1}.
|
||||
% what is the problem?
|
||||
% Java does invisible capture conversion steps
|
||||
Java's wildcard types are represented as existential types that have to be opened before they can be used.
|
||||
Opening can either be done implicitly
|
||||
(\cite{aModelForJavaWithWildcards}, \cite{javaTIisBroken}) or
|
||||
explicitly via a let statement (\cite{WildcardsNeedWitnessProtection}).
|
||||
For all variations it is vital to know the argument types with which a method is called.
|
||||
In the absence of type annotations,
|
||||
we do not know where an existential type will emerge and where a capture conversion is necessary.
|
||||
Rather, the type inference algorithm has to figure out the placement
|
||||
of existentials.
|
||||
We identified three main challenges related to Java wildcards and global type inference.
|
||||
\begin{enumerate}
|
||||
\item \label{challenge:1}
|
||||
One challenge is to design the algorithm in a way that it finds a
|
||||
correct solution for programs like the one shown in Listing~\ref{lst:addExample}
|
||||
and rejects programs like the one in Listing~\ref{lst:concatError}.
|
||||
The first one is a valid Java program,
|
||||
because the type \texttt{List<? super String>} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$
|
||||
which is used as the generic method parameter for the call to \texttt{add} as shown in Listing~\ref{lst:addExampleLet}.
|
||||
Because we know that the type \texttt{String} is a subtype of the free variable $\rwildcard{X}$,
|
||||
it is safe to pass \texttt{"String"} for the first parameter of the function.
|
||||
|
||||
The second program shown in Listing~\ref{lst:concatError} is incorrect.
|
||||
The method call to \texttt{concat} with two wildcard lists is unsound.
|
||||
The element types of the lists may be unrelated, therefore the call to \texttt{concat} cannot succeed.
|
||||
The problem gets apparent if we try to write the \texttt{concat}
|
||||
method call in the \TamedFJ{} calculus
|
||||
(Listing~\ref{lst:concatTamedFJ}):
|
||||
\texttt{l1'} and \texttt{l2'} are two different lists inside the body of the let statements, namely
|
||||
$\exptype{List}{\rwildcard{X}}$ and $\exptype{List}{\rwildcard{Y}}$.
|
||||
For the method call \texttt{concat(x1, x2)} no replacement for the generic \texttt{A}
|
||||
exists to satisfy
|
||||
$\exptype{List}{\type{A}} <: \exptype{List}{\type{X}},
|
||||
\exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$.
|
||||
|
||||
% \textbf{Solution:}
|
||||
% Capture Conversion during Unify.
|
||||
|
||||
\item
|
||||
\unify{} transforms a constraint set into a correct type solution by
|
||||
gradually assigning types to type placeholders during that process.
|
||||
Solved constraints are removed and never considered again.
|
||||
In the following example, \unify{} solves the constraint generated by the expression
|
||||
\texttt{l.add(l.head())} first, which results in $\ntv{l} \lessdot \exptype{List}{\wtv{a}}$.
|
||||
\begin{verbatim}
|
||||
anyList() = new List<String>() :? new List<Integer>()
|
||||
|
||||
add(anyList(), anyList().head());
|
||||
\end{verbatim}
|
||||
The type for \texttt{l} can be an arbitrary list, but it has to be a invariant one.
|
||||
Assigning a \texttt{List<?>} for \texttt{l} is unsound, because the type list hiding behind
|
||||
\texttt{List<?>} could be a different one for the \texttt{add} call than the \texttt{head} method call.
|
||||
An additional constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
|
||||
is solved by removing the wildcard $\rwildcard{X}$ if possible.
|
||||
|
||||
This problem is solved by ANF transformation
|
||||
|
||||
\item
|
||||
% This problem is solved by assuming everything is a wildcard and lateron erasing excessive wildcards
|
||||
% this is solved by having wildcards bound to a type. But this makes it necessary to remove wildcards lateron otherwise Unify would have to backtrack
|
||||
The program in Listing~\ref{shuffleExample} exhibits a challenge involving wildcards and subtyping.
|
||||
The method call \texttt{shuffle(l)} is incorrect, because \texttt{l} has type
|
||||
$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ representing a list of unknown lists.
|
||||
However, $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ is a subtype of
|
||||
$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ which represents a list of lists, all of the same type $\rwildcard{X}$,
|
||||
and can be passed safely to \texttt{shuffle}.
|
||||
This behavior can also be explained by looking at the types and their capture converted versions:
|
||||
\begin{center}
|
||||
\begin{tabular}{l | l | l}
|
||||
Java type & \TamedFJ{} representation & Capture Conversion \\
|
||||
\hline
|
||||
$\exptype{List}{\exptype{List}{\texttt{?}}}$ & $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ & $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ \\
|
||||
$\exptype{List2D}{\texttt{?}}$ & $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ & $\exptype{List2D}{\rwildcard{X}}$ \\
|
||||
%Supertype of $\exptype{List2D}{\texttt{?}}$ & $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ & $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ \\
|
||||
\end{tabular}
|
||||
\end{center}
|
||||
%The direct supertype of $\exptype{List2D}{\rwildcard{X}}$ is $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
|
||||
%One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}.
|
||||
%A wildcard in the Java syntax has no name and is bound to its enclosing type:
|
||||
%$\exptype{List}{\exptype{List}{\type{?}}}$ equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
|
||||
%During type checking \emph{intermediate types}
|
||||
%can emerge, which have no equivalent in the Java syntax.
|
||||
|
||||
\begin{lstlisting}[style=java,label=shuffleExample,caption=Intermediate Types Example]
|
||||
class List<X> extends Object {...}
|
||||
class List2D<X> extends List<List<X>> {...}
|
||||
|
||||
<X> void shuffle(List<List<X>> list) {...}
|
||||
|
||||
List<List<?>> l = ...;
|
||||
List2D<?> l2d = ...;
|
||||
|
||||
shuffle(l); // Error
|
||||
shuffle(l2d); // Valid
|
||||
\end{lstlisting}
|
||||
% Java is using local type inference to allow method invocations which are not describable with regular Java types.
|
||||
% The \texttt{shuffle} method in this case is invoked with the type $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$
|
||||
% which is a subtype of $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
|
||||
% After capture conversion \texttt{l2d'} has the type $\exptype{List}{\exptype{List}{\rwildcard{X}}}$
|
||||
% and \texttt{shuffle} can be invoked with the type parameter $\rwildcard{X}$:
|
||||
% \begin{lstlisting}[style=TamedFJ]
|
||||
% let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in <X>shuffle(l2d')
|
||||
% \end{lstlisting}
|
||||
|
||||
% For the example shown in listing \ref{shuffleExample} the method call \texttt{shuffle(l2d)} creates the constraints:
|
||||
% \begin{constraintset}
|
||||
% \begin{center}
|
||||
% $
|
||||
% \begin{array}{l}
|
||||
% \wctype{\rwildcard{X}}{List2D}{\rwildcard{X}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
|
||||
% \\
|
||||
% \hline
|
||||
% \wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
|
||||
% \\
|
||||
% \hline
|
||||
% \textit{Capture Conversion:}\
|
||||
% \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\wtv{x}}}
|
||||
% \\
|
||||
% \hline
|
||||
% \textit{Solution:} \wtv{x} \doteq \rwildcard{X} \implies \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\rwildcard{X}}}
|
||||
% \end{array}
|
||||
% $
|
||||
% \end{center}
|
||||
% \end{constraintset}
|
||||
|
||||
Given such a program the type inference algorithm has to allow the call \texttt{shuffle(l2d)} and
|
||||
decline the call to \texttt{shuffle(l)}.
|
||||
|
||||
% The method call \texttt{shuffle(l)} is invalid however,
|
||||
% because \texttt{l} has the type
|
||||
% $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
|
||||
% There is no solution for the subtype constraint:
|
||||
% $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$
|
||||
|
||||
\item \label{challenge3} \textbf{Free variables cannot leave their scope}:
|
||||
Let's assume we have a variable \texttt{ls} with type $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$
|
||||
%When calling the \texttt{id} function with an element of this list we have to apply capture conversion.
|
||||
and the following program:
|
||||
|
||||
\noindent
|
||||
\begin{minipage}{0.62\textwidth}
|
||||
\begin{lstlisting}
|
||||
let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = ls.get(0) in id(x) : (*@$\ntv{z}$@*)
|
||||
\end{lstlisting}\end{minipage}
|
||||
\hfill
|
||||
\begin{minipage}{0.36\textwidth}
|
||||
\begin{lstlisting}[style=constraints]
|
||||
(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$@*),
|
||||
(*@$\exptype{List}{\wtv{x}} \lessdot \ntv{z},$@*)
|
||||
\end{lstlisting}
|
||||
\end{minipage}
|
||||
% the variable z has to
|
||||
|
||||
Take the Java program in listing \ref{lst:mapExample} for example.
|
||||
It uses map to apply a polymorphic method \texttt{id} to every element of a list
|
||||
$\expr{l} :
|
||||
\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$.
|
||||
|
||||
How do we get the \unify{} algorithm to determine the correct type for the
|
||||
variable \expr{l2}?
|
||||
Although we do not specify constraint generation for language constructs like
|
||||
lambda expressions used in this example,
|
||||
we can imagine that the constraints have to look like in Listing~\ref{lst:mapExampleCons}.
|
||||
|
||||
\begin{minipage}{0.45\textwidth}
|
||||
\begin{lstlisting}[caption=List Map Example,label=lst:mapExample]
|
||||
<X> List<X> id(List<X> l){ ... }
|
||||
List<List<?>> ls;
|
||||
l2 = l.map(x -> id(x));
|
||||
\end{lstlisting}\end{minipage}
|
||||
\hfill
|
||||
\begin{minipage}{0.45\textwidth}
|
||||
\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:mapExampleCons]
|
||||
(*@$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}$@*)
|
||||
(*@$\exptype{List}{\wtv{x}} \lessdot \tv{z},$@*)
|
||||
(*@$\exptype{List}{\tv{z}} \lessdot \tv{l2}$@*)
|
||||
\end{lstlisting}
|
||||
\end{minipage}
|
||||
|
||||
The constraints
|
||||
$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}},
|
||||
\exptype{List}{\wtv{x}} \lessdot \tv{z}$
|
||||
stem from the body of the lambda expression
|
||||
\texttt{id(x)}.
|
||||
\textit{For clarification:} This method call would be represented as the following expression in \letfj{}:
|
||||
\texttt{let x1 :$\wctype{\rwildcard{A}}{List}{\rwildcard{A}}$ = x in id(x) :$\tv{z}$}
|
||||
|
||||
The T-Let rule prevents us from using free variables created by the method call to \expr{id}
|
||||
to be used in the return type $\tv{z}$.
|
||||
But this restriction has to be communicated to the \unify{} algorithm,
|
||||
which does not know about the origin and context of
|
||||
the constraints.
|
||||
If we naively substitute $\sigma(\tv{z}) = \exptype{List}{\rwildcard{A}}$
|
||||
the return type of the \texttt{map} function would be the type
|
||||
$\exptype{List}{\exptype{List}{\rwildcard{A}}}$, which would be unsound.
|
||||
The type of \expr{l2} is the same as the one of \expr{l}:
|
||||
$\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
|
||||
|
||||
\textbf{Solution:}
|
||||
We solve this issue by distinguishing between wildcard placeholders
|
||||
and normal placeholders and introducing them as needed.
|
||||
$\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.
|
||||
|
||||
\end{enumerate}
|
||||
|
||||
%TODO: Move this part. or move the third challenge some underneath.
|
||||
|
||||
%%% Local Variables:
|
||||
%%% mode: latex
|
||||
%%% TeX-master: "TIforWildFJ"
|
||||
%%% End:
|
||||
|
578
soundness.tex
578
soundness.tex
@ -1,118 +1,109 @@
|
||||
\section{Soundness}
|
||||
|
||||
\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}
|
||||
% \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
|
||||
% 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>
|
||||
% <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<?>
|
||||
% 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
|
||||
% 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,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
|
||||
% <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
|
||||
% 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
|
||||
% 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
|
||||
% 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$.
|
||||
% 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.
|
||||
% 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}$.
|
||||
% \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}$
|
||||
% $|\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
|
||||
% \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$
|
||||
% 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}
|
||||
% \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.
|
||||
% \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}{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'$
|
||||
\item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = (\Delta', C)$
|
||||
and $(\Delta_u, \sigma) = \unify{}(\Delta', C)$ and let $\Delta= \Delta_u \cup \Delta'$
|
||||
$\Delta, \Delta' \vdash $
|
||||
% , 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})$
|
||||
%\item[then] there is a completion $|\texttt{e}|$ with $\Delta|\Gamma \vdash |\texttt{e}| : \sigma(\tv{a})$
|
||||
\item[then] $\Delta|\Gamma \vdash \texttt{e} : \sigma(\tv{a})$
|
||||
\end{description}
|
||||
\end{lemma}
|
||||
Regular type placeholders represent type annotations.
|
||||
@ -129,6 +120,16 @@ used in let statements and as type parameters for generic method calls.
|
||||
\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$]
|
||||
$\Delta|\Gamma \vdash \expr{t}_1: \type{T}_1$ by assumption.
|
||||
The body of the let statement will only use the free variables provided by $\Delta$ and $\Delta'$ (see lemma \ref{lemma:wildcardsStayInScope}).
|
||||
\item[$\expr{v}.\texttt{f}$]
|
||||
We are alowwed to use capture conversion for $\expr{v}$ here.
|
||||
|
||||
\item[$\texttt{let}\ \texttt{x} = \texttt{e} \ \texttt{in} \ \texttt{x}.\texttt{f}$]
|
||||
$\Delta|\Gamma \vdash \expr{e}: \type{T}$ by assumption.
|
||||
$\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ by lemma \ref{lemma:wildcardWellFormedness}.
|
||||
$\Delta, \Delta' | \Gamma, \expr{x} : \type{T} \vdash \texttt{x}.\texttt{f}$
|
||||
\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.
|
||||
@ -157,28 +158,29 @@ By structural induction over the expression $\texttt{e}$.
|
||||
% 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
|
||||
% S typeinference:
|
||||
% T <: [S/Y]U
|
||||
% We apply the following lemma
|
||||
% Lemma
|
||||
% if T ok and T <: S then S ok
|
||||
|
||||
and then we can say by
|
||||
Lemma:
|
||||
If [S/Y]U ok then S ok (TODO: proof!)
|
||||
% until
|
||||
% T = [S/Y]U
|
||||
|
||||
So we do not have to proof S ok (but T)
|
||||
% and then we can say by
|
||||
% Lemma:
|
||||
% If [S/Y]U ok then S ok (TODO: proof!)
|
||||
|
||||
% 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
|
||||
% So we do not have to proof S ok (but T)
|
||||
|
||||
$\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
|
||||
%Easy, because unify only generates substitutions for normal type placeholders which are OK
|
||||
% % 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.
|
||||
@ -194,7 +196,8 @@ $\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\
|
||||
% 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
|
||||
%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
|
||||
@ -206,12 +209,13 @@ which shows $\Delta, \Delta', \overline{\Delta} \vdash \overline{N} <: [\ol{S}/\
|
||||
$\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}.
|
||||
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.
|
||||
%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}
|
||||
@ -270,29 +274,45 @@ 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.
|
||||
% \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})$.
|
||||
|
||||
% 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}\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{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{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}
|
||||
@ -313,16 +333,30 @@ Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.
|
||||
% 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{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{}( C \cup C')$ and $\text{wtv}(C) \cap \text{wtv}(C') = \emptyset$
|
||||
\item[then] $ (\sigma', \Delta') = \unify{}( C')$
|
||||
\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}
|
||||
|
||||
If $\wcNtype{\Delta'}{N} \lessdot \tv{a}$
|
||||
\end{lemma}
|
||||
\textit{Proof:}
|
||||
|
||||
|
||||
|
||||
%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!
|
||||
@ -507,158 +541,158 @@ 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.
|
||||
% \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.
|
||||
% %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.
|
||||
% 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.
|
||||
% 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}.
|
||||
% %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.
|
||||
% 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}}$.
|
||||
% 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$.
|
||||
% 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}
|
||||
% \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 |