Compare commits
12 Commits
70131d064d
...
9daf5ce8ef
| Author | SHA1 | Date | |
|---|---|---|---|
|
9daf5ce8ef | ||
|
|
5055364de5 | ||
|
b1ce0f771b | ||
|
903b2405b1 | ||
|
|
323f2c0163 | ||
|
|
ecd2975129 | ||
|
|
e49b87b549 | ||
|
|
4547fbab40 | ||
|
|
cbba453a73 | ||
|
|
e15d61cdae | ||
|
|
3904304a1d | ||
|
|
4eb7b1ce19 |
288
TIforWildFJ.tex
288
TIforWildFJ.tex
@ -36,6 +36,7 @@
|
||||
\usepackage{cancel}
|
||||
\usepackage{tcolorbox}
|
||||
\usepackage{arydshln}
|
||||
\usepackage{dashbox}
|
||||
|
||||
\input{prolog}
|
||||
|
||||
@ -101,126 +102,7 @@ TODO: Abstract
|
||||
|
||||
\input{introduction}
|
||||
|
||||
%We could do a translation from Java to \wildFJ explaining implicit capture conversion
|
||||
|
||||
\section{Soundness of Typing}
|
||||
|
||||
|
||||
We show soundness with the type rules statet in \cite{WildcardsNeedWitnessProtection}.
|
||||
A correct \FGJGT{} program can be converted to a correct \wildFJ{} program.
|
||||
|
||||
\begin{figure}
|
||||
$\begin{array}{rcl}
|
||||
| \texttt{x} |
|
||||
& = & \texttt{x} \\
|
||||
| \texttt{let} \ \texttt{x} : \type{T} = \texttt{e},\, \ol{x} : \ol{T} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x}) |
|
||||
& = & |\texttt{e}|.\texttt{m}(\ol{|e|}) \\
|
||||
| \texttt{let} \ \texttt{x} : \type{T} = \texttt{e}\ \texttt{in}\ \texttt{x}.\texttt{f} |
|
||||
& = & |\texttt{e}|.\texttt{f} \\
|
||||
| \texttt{e} \elvis{} \texttt{e} |
|
||||
& = & |\texttt{e}| \elvis{} |\texttt{e}| \\
|
||||
\end{array}$
|
||||
\caption{Erasure} \label{fig:erasure}
|
||||
\end{figure}
|
||||
|
||||
% A constraint Pair<A,B> <. a, then a has infinite possibilities:
|
||||
% a =. X.Pair<X,X>
|
||||
% a =. X,Y.Pair<X,Y>
|
||||
% a =. X.Pair<Pair<X,X>,X>
|
||||
% a =. X,Y.Pair<Pair<X,Y>,X>
|
||||
% a =. X,Y.Pair<Pair<X,Y>,Y>
|
||||
|
||||
% There is no way to try out every single one of them.
|
||||
|
||||
Starting with the parameters of the method we gradually add every expression which only contains already captured expressions.
|
||||
|
||||
We have a typed expression
|
||||
|
||||
$|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} : \type{T} = \texttt{x in}$
|
||||
$|\texttt{e.f}, \texttt{r}| = |\texttt{e}, x| \texttt{let} r = x.\texttt{f} \ \texttt{in}$
|
||||
$|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} = \texttt{x in}$
|
||||
%TODO: write the transform rules:
|
||||
% |e.f, ret| = |e, r| let ret = r.f in
|
||||
% |x, ret| = let ret = x in
|
||||
% |e.m(e_), ret| = |e, r| |e_, a_| let ret = r.m(a_) in
|
||||
|
||||
Erasure functions:
|
||||
$|\texttt{x}| = \texttt{let r} : \wcNtype{\Delta}{N} = \texttt{x in r}$
|
||||
|
||||
$\texttt{x} \longmapsto \texttt{let}\ \texttt{xx} : \type{T} = \texttt{x in xx}$
|
||||
$\texttt{x}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in xf}$
|
||||
|
||||
$\begin{array}{l}
|
||||
\texttt{e} \longmapsto \texttt{let}\ \texttt{xe} : \type{T} = \texttt{e}' \ \texttt{in xe} \\
|
||||
\hline
|
||||
\vspace*{-0.4cm}\\
|
||||
\texttt{e}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in x}.f
|
||||
\end{array}$
|
||||
|
||||
Example:
|
||||
m(a, b) = a.m(b.f);
|
||||
|
||||
let xa = a in let xb = b in let xf = xb.f in let xm = xa.m(xf) in xm
|
||||
|
||||
% TODO: Now we have to proof that there is a LetFJ program for every TIFJ program!
|
||||
% |let xr : T = x1.m(x2) in e| = [x1.m(x2)/xr]|e|
|
||||
% |let xf : T = x1.f in e| = [x1.f/xf]|e|
|
||||
% |let xr : T = x in e| = [xr/x]|e|
|
||||
% |new C(x)| = new C(x)
|
||||
|
||||
% | let xr : T' = x in let xf : T = xr.f | = x.f
|
||||
|
||||
|
||||
% let x : T' = e' in x = |e|
|
||||
% ---------------------------------
|
||||
% | let xr : T' = x in let xf : T = xr.f | = x.f
|
||||
|
||||
|
||||
|
||||
% let x : T' = e' in x = |e|
|
||||
% -----------
|
||||
% =
|
||||
|
||||
We need a language which only has let statemnts and expressions on capture converted variables
|
||||
|
||||
The idea is to use wildcard placeholders inside the method. Also in the bounds of wildcards.
|
||||
This makes it possible to replace wildcards with free variables by setting upper and lower bound to that free variable.
|
||||
Free variables then can flow freely inside the method body.
|
||||
We have to show that a type solution implies that there is a possible transformation to a correct typed letFJ program.
|
||||
If there is a possible method type then there must exist a let configuration.
|
||||
% By starting with the parameter types and capturing them. Afterwards every capture creates free variables which are used inside
|
||||
% TODO: Proof!
|
||||
|
||||
The normal type placeholders represent denotable types.
|
||||
|
||||
%TODO: the type rules stay the same. We generate let statements in a fashion which removes all wildcard types.
|
||||
% what about wildcards getting returned by untyped methods? they can also be captured
|
||||
% TODO: try soundness proof on the original type rules!
|
||||
|
||||
Removing of extensive wildcards:
|
||||
$
|
||||
\wctype{\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{X}, \rwildcard{Y}}
|
||||
\lessdot \wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}} \\
|
||||
\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \wtv{x}, \rwildcard{Y} \doteq \wtv{x} \\
|
||||
\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \rwildcard{Y} \\
|
||||
\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
|
||||
\implies \wctype{\wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{Y}, \rwildcard{Y}}, \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
|
||||
$
|
||||
|
||||
%e.f leads to constraints: r <c C<x> with return type equals the field type T.
|
||||
% T can contain free variables from r. but also it can be used in another constraint and get free variables from inner let statements
|
||||
% X.C<X> <c C<x> -> then T contains X variables
|
||||
|
||||
% let x1 = p1, x2 = p2 in
|
||||
% let r1 = x1 in let r2 = p2 in let f1 = r2.f in let r3 = x1 in let m2 = r3.m2() let ret = r1.m(f1,m2)
|
||||
% in ret
|
||||
|
||||
What about method invocation with no type yet. m2 :: a -> a
|
||||
they are also encased in let expression so the return type can be capture converted.
|
||||
Those methods and the parameter types of the current method are the only things not typed.
|
||||
All the other types cannot change their type. The captured wildcards can only flow from top to bottom.
|
||||
The return type of untyped methods has to be well-formed and cannot contain free variables.
|
||||
Therefore no free variables will flow into those types.
|
||||
%\input{letfjTransformation}
|
||||
|
||||
\input{tRules}
|
||||
|
||||
@ -228,172 +110,6 @@ Therefore no free variables will flow into those types.
|
||||
|
||||
\input{constraints}
|
||||
|
||||
\section{Capture Conversion}
|
||||
The input to our type inference algorithm does not contain let statements.
|
||||
Those are added after computing a type solution.
|
||||
Let statements act as capture conversion and only have to be applied in method calls involving wildcard types.
|
||||
|
||||
\begin{figure}
|
||||
\begin{minipage}{0.45\textwidth}
|
||||
\begin{lstlisting}[style=fgj]
|
||||
<X> List<X> clone(List<X> l);
|
||||
example(p){
|
||||
return clone(p);
|
||||
}
|
||||
\end{lstlisting}
|
||||
\end{minipage}%
|
||||
\hfill
|
||||
\begin{minipage}{0.5\textwidth}
|
||||
\begin{lstlisting}[style=tfgj]
|
||||
(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
|
||||
return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in
|
||||
clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
|
||||
}
|
||||
\end{lstlisting}
|
||||
\end{minipage}
|
||||
\caption{Type inference adding capture conversion}\label{fig:addingLetExample}
|
||||
\end{figure}
|
||||
|
||||
Figure \ref{fig:addingLetExample} shows a let statement getting added to the typed output.
|
||||
The method \texttt{clone} cannot be called with the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
|
||||
After a capture conversion \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ with $\rwildcard{X}$ being a free variable.
|
||||
Afterwards we have to find a supertype of $\exptype{List}{\rwildcard{X}}$, which does not contain free variables
|
||||
($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in this case).
|
||||
|
||||
During the constraint generation step most types are not known yet and are represented by a type placeholder.
|
||||
During a methodcall like the one in the \texttt{example} method in figure \ref{fig:ccExample} the type of the parameter \texttt{p}
|
||||
is not known yet.
|
||||
The type \texttt{List<?>} would be one possibility as a parameter type for \texttt{p}.
|
||||
To make wildcards work for our type inference algorithm \unify{} has to apply capture conversions if necessary.
|
||||
|
||||
The type placeholder $\tv{r}$ is the return type of the \texttt{example} method.
|
||||
One possible type solution is $\tv{p} \doteq \tv{r} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$,
|
||||
which leads to:
|
||||
\begin{verbatim}
|
||||
List<?> example(List<?> p){
|
||||
return clone(p);
|
||||
}
|
||||
\end{verbatim}
|
||||
|
||||
But by substituting $\tv{p} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in the constraint
|
||||
$\tv{p} \lessdot \exptype{List}{\wtv{x}}$ leads to
|
||||
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{x}}$.
|
||||
|
||||
To make this typing possible we have to introduce a capture conversion via a let statement:
|
||||
$\texttt{return}\ (\texttt{let}\ \texttt{x} : \wctype{\rwildcard{X}}{List}{\rwildcard{X}} = \texttt{p}\ \texttt{in} \
|
||||
\texttt{clone}\generics{\rwildcard{X}}(x) : \wctype{\rwildcard{X}}{List}{\rwildcard{X}})$
|
||||
|
||||
Inside the let statement the variable \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$
|
||||
|
||||
$
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \rwildcard{G}}\\
|
||||
\hline
|
||||
[\type{G}/\wtv{a}]\wildcardEnv \vdash [\type{G}/\wtv{a}]C \cup \set{\tv{a} \doteq \type{G}}
|
||||
\end{array}
|
||||
$
|
||||
|
||||
This spawns additional problems.
|
||||
%TODO
|
||||
%we need the constraint set to be a list
|
||||
%not on every constraint CC is allowed. The unify algorithm does not know the context in which a constraint was generated
|
||||
%free type variables cannot leave the scope of the method call
|
||||
|
||||
\begin{figure}
|
||||
\begin{minipage}{0.45\textwidth}
|
||||
\begin{verbatim}
|
||||
<X> List<X> clone(List<X> l){...}
|
||||
|
||||
example(p){
|
||||
return clone(p);
|
||||
}
|
||||
\end{verbatim}
|
||||
\end{minipage}%
|
||||
\hfill
|
||||
\begin{minipage}{0.35\textwidth}
|
||||
\begin{constraintset}
|
||||
\textbf{Constraints:}\\
|
||||
$
|
||||
\tv{p} \lessdot \exptype{List}{\wtv{x}}, \\
|
||||
\tv{p} \lessdot \tv{r}, \\
|
||||
\tv{p} \lessdot \type{Object},
|
||||
\tv{r} \lessdot \type{Object}
|
||||
$
|
||||
\end{constraintset}
|
||||
\end{minipage}
|
||||
|
||||
\caption{Type inference example}\label{fig:ccExample}
|
||||
\end{figure}
|
||||
|
||||
In addition with free variables this leads to unwanted behaviour.
|
||||
Take the constraint
|
||||
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ for example.
|
||||
After a capture conversion from $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ to $\exptype{List}{\rwildcard{Y}}$ and a substitution $\wtv{a} \doteq \rwildcard{Y}$
|
||||
we get
|
||||
$\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$.
|
||||
Which is correct if we apply capture conversion to the left side:
|
||||
$\exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$
|
||||
If the input constraints did not intend for this constraint to undergo a capture conversion then \unify{} would produce an invalid
|
||||
type solution due to:
|
||||
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \nless: \exptype{List}{\rwildcard{X}}$
|
||||
The reason for this is the \texttt{S-Exists} rule's premise
|
||||
$\text{dom}(\Delta') \cap \text{fv}(\exptype{List}{\rwildcard{X}}) = \emptyset$.
|
||||
|
||||
Additionally free variables are not allowed to leave the scope of a capture conversion
|
||||
introduced by a let statement.
|
||||
%TODO we combat both of this with wildcard type placeholders (? flag)
|
||||
|
||||
Type placeholders which are not flagged as possible free variables ($\wtv{a}$) can never hold a free variable or a type containing free variables.
|
||||
Constraint generation places these standard place holders at method return types and parameter types.
|
||||
\begin{lstlisting}[style=fgj]
|
||||
<X> List<X> clone(List<X> l);
|
||||
(*@$\red{\tv{r}}$@*) example((*@$\red{\tv{p}}$@*) p){
|
||||
return clone(p);
|
||||
}
|
||||
\end{lstlisting}
|
||||
This prevents type solutions that contain free variables in parameter and return types.
|
||||
When calling a method which already has a type annotation we have to consider adding a capture conversion in form of a let statement.
|
||||
The constraint $\tv{p} \lessdot \exptype{List}{\wtv{x}}$ signals the \unify{} algorithm that here a capture conversion is possible.
|
||||
$\sigma(\tv{p}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, \sigma(\tv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, $ is a possible solution.
|
||||
But only when adding a capture conversion:
|
||||
\begin{lstlisting}[style=fgj]
|
||||
<X> List<X> clone(List<X> l);
|
||||
(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
|
||||
return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
|
||||
}
|
||||
\end{lstlisting}
|
||||
\unify{}'s type solution for constraints involving free variables only holds under special circumstances.
|
||||
Constraint $\tv{p} \lessdot \exptype{List}{\wtv{x}}$ only holds when a capture conversion is applied to the left side:
|
||||
$\Delta, \Delta' \vdash CC(\sigma(\tv{p})) <: \sigma(\exptype{List}{\wtv{x}})$
|
||||
and there is a an environment $\Delta'$ holding all type variables used inside the subtype relation.
|
||||
This is done by packing the method call inside a let statement, which performs a capture conversion on all expressions used as parameters.
|
||||
%TODO: Explain (do soundness and TYPE algorithm first)
|
||||
|
||||
A type solution of the \unify{} algorithm only guarantees correct subtyping for constraints not containing free variables.
|
||||
Constraints like $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ only guarantee
|
||||
$\Delta, \Delta' \vdash \sigma(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) <: \sigma(\exptype{List}{\wtv{a}})$ when
|
||||
adding a $\Delta'$ environment and applying a capture conversion on the left side.
|
||||
In this case the type solution would be $\tv{a} \to \rwildcard{X}$ leading to:
|
||||
$\Delta, \set{\rwildcard{X}} \vdash \exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$
|
||||
|
||||
This is the reason input constraints containing free variables cannot be stored in a set.
|
||||
$\wtv{a} \lessdot \wtv{b}$ is not the same as $\wtv{a} \lessdot \wtv{b}$.
|
||||
Both constraints will end up the same after a substitution for both placeholders $\tv{a}$ and $\tv{b}$.
|
||||
But afterwards a capture conversion is applied, which can generate different types on the left sides.
|
||||
\begin{itemize}
|
||||
\item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Y}}$
|
||||
\item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Z}}$
|
||||
\end{itemize}
|
||||
|
||||
|
||||
Also the subtype relation is not symmetric for types involving free type variables.
|
||||
$\type{T} \lessdot \type{S}$ and $\type{S} \lessdot \type{T}$ doesnt mean $\type{T} = \type{S}$, because we apply a capture conversion on every constraint.
|
||||
Only for constraints without free variables symmetry is given.
|
||||
|
||||
% Can untyped methods also get a capture conversion? NO!
|
||||
|
||||
%TODO: Explain why capture conversion is needed (also in respect to martins algorithm)
|
||||
|
||||
\input{Unify}
|
||||
|
||||
\section{Limitations}
|
||||
|
||||
@ -9,6 +9,20 @@
|
||||
|
||||
%\subsection{Well-Formedness}
|
||||
|
||||
Constraint generation step is the same as in \cite{TIforFGJ} except for field access and method invocation.
|
||||
Here \fjtype{} generates capture constraints instead of normal subtype constraints.
|
||||
|
||||
Subtype constraints are created according to the type rules defined in section \ref{sec:tifj}.
|
||||
The \typeExpr{} function creates constraints for a given expression.
|
||||
|
||||
$\begin{array}{c}
|
||||
\typeExpr(\texttt{t}_1, \ntv{b}) = C_l \quad \quad \typeExpr(\texttt{t}_2, \ntv{c}) = C_l \quad \quad \ntv{b}, \ntv{c} \ \text{fresh}
|
||||
\\
|
||||
\hline
|
||||
\typeExpr(\texttt{t}_1 \texttt{?:} \texttt{t}_2, \tv{a}) = C_l \cup C_r \cup \set{\ntv{b} \lessdot \tv{a}, \ntv{c} \lessdot \tv{a}}
|
||||
\end{array}
|
||||
$
|
||||
|
||||
The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
|
||||
Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
|
||||
|
||||
@ -138,7 +152,8 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
|
||||
\orCons\set{
|
||||
\set{ &
|
||||
\tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}} ,
|
||||
[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} , \ol{\wtv{a}} \lessdot [\overline{\wtv{a}}/\ol{X}]\ol{N}
|
||||
[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} ,
|
||||
\ol{\wtv{a}} \lessdot [\overline{\wtv{a}}/\ol{X}]\ol{N}
|
||||
} \\
|
||||
& \quad \mid \mv{T}\ \mv{f} \in \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}
|
||||
, \, \overline{\wtv{a}} \text{ fresh}
|
||||
@ -153,9 +168,10 @@ The set of method assumptions returned by the \textit{mtypes} function is used t
|
||||
|
||||
There are two kinds of method calls.
|
||||
The ones to already typed methods and calls to untyped methods.
|
||||
|
||||
\begin{displaymath}
|
||||
\begin{array}{@{}l@{}l}
|
||||
\typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}})) = \\
|
||||
\typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a}) = \\
|
||||
& \begin{array}{ll}
|
||||
\textbf{let}
|
||||
& \tv{r}, \ol{\tv{r}} \text{ fresh} \\
|
||||
@ -165,57 +181,19 @@ The ones to already typed methods and calls to untyped methods.
|
||||
& \begin{array}{@{}l@{}l}
|
||||
\constraint = \orCons\set{ &
|
||||
\begin{array}[t]{l}
|
||||
%[\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdot \wctype{\ol{\wildcard{X}{\ntv{u}}{\ntv{l}}}}{C}{\ol{X}}, \wctype{\ol{\wildcard{X}{\ntv{u}}{\ntv{l}}}}{C}{\ol{X}} \lessdotCC \exptype{C}{\ol{X}},
|
||||
[\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdotCC \exptype{C}{\ol{X}},
|
||||
\overline{\tv{r}} \lessdotCC \ol{T},
|
||||
\ol{X} \lessdot \ol{N},
|
||||
\ol{Y} \lessdot \ol{N'} \}
|
||||
\overline{\tv{r}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a},
|
||||
\ol{Y} \lessdot \ol{N} \}
|
||||
\end{array}\\
|
||||
& \ |\
|
||||
(\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N'}}\overline{\type{T}} \to \type{T}) \in
|
||||
{\mtypeEnvironment}, \, |\ol{T}| = |\ol{e}|
|
||||
, \, \overline{\wtv{a}} \text{ fresh}, \, \overline{\wtv{b}} \text{ fresh} }
|
||||
(\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T}) \in
|
||||
{\mtypeEnvironment} %, \, |\ol{T}| = |\ol{e}|
|
||||
, \, \overline{\wtv{a}} \text{ fresh}}
|
||||
\end{array}\\
|
||||
\mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T})
|
||||
\end{array}
|
||||
\end{array}
|
||||
\end{displaymath}
|
||||
% \begin{displaymath}
|
||||
% \typeExpr{}' ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a} ) = \
|
||||
% \typeExpr{} ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \wtv{b} ) \cup \set{ \wtv{b} \lessdot \tv{a}}
|
||||
% \end{displaymath}
|
||||
|
||||
\begin{displaymath}
|
||||
\typeExpr{}' ({\mtypeEnvironment} , \texttt{return e;}, \tv{a} ) = \
|
||||
\typeExpr{} ({\mtypeEnvironment} , \texttt{e}, \wtv{b} ) \cup \set{ \wtv{b} \lessdot \tv{a}} \quad \quad \tv{a}, \wtv{b} \ \text{fresh}
|
||||
\end{displaymath}
|
||||
% \begin{displaymath}
|
||||
% \begin{array}{@{}l@{}l}
|
||||
% \typeExpr{} & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a} ) = \\
|
||||
% & \begin{array}{ll}
|
||||
% \textbf{let}
|
||||
% & \tv{r}, \ol{\tv{r}} \text{ fresh} \\
|
||||
% & \consSet_R = \typeExpr(({\mtypeEnvironment} ;
|
||||
% \overline{\localVarAssumption}), \texttt{e}, \tv{r})\\
|
||||
% & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \ol{e}, \ol{\tv{r}}) \\
|
||||
% & \begin{array}{@{}l@{}l}
|
||||
% \constraint = \orCons\set{ &
|
||||
% \begin{array}[t]{l}
|
||||
% [\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdot \exptype{C}{\ol{X}},
|
||||
% \overline{\tv{r}} \lessdot \ol{T},
|
||||
% \type{T} \lessdot \tv{a},
|
||||
% \ol{X} \lessdot \ol{N},
|
||||
% \ol{Y} \lessdot \ol{N'} \}
|
||||
% \end{array}\\
|
||||
% & \ |\
|
||||
% (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N'}}\overline{\type{T}} \to \type{T}) \in
|
||||
% {\mtypeEnvironment}
|
||||
% , \, \overline{\wtv{a}} \text{ fresh}, \, \overline{\wtv{b}} \text{ fresh} }
|
||||
% \end{array}\\
|
||||
% \mathbf{in} & \consSet_R \cup \overline{\consSet} \cup \constraint
|
||||
% \end{array}
|
||||
% \end{array}
|
||||
% \end{displaymath}
|
||||
\\[1em]
|
||||
\noindent
|
||||
\textbf{Example:}
|
||||
|
||||
609
introduction.tex
609
introduction.tex
@ -7,7 +7,7 @@
|
||||
\section{Type Inference for Java}
|
||||
%The goal is to find a correct typing for a given Java program.
|
||||
Type inference for Java has many use cases and could be used to help programmers by inserting correct types for them,
|
||||
Finding better type solutions for already typed Java programs (for example more generical ones),
|
||||
finding better type solutions for already typed Java programs (for example more generical ones),
|
||||
or allowing to write typeless Java code which is then type infered and thereby type checked by our algorithm.
|
||||
The algorithm proposed in this paper can determine a correct typing for the untyped Java source code example shown in figure \ref{fig:intro-example-typeless}.
|
||||
Our algorithm is also capable of finding solutions involving wildcards as shown in figure \ref{fig:intro-example-typed}.
|
||||
@ -21,41 +21,38 @@ The \fjtype{} algorithm calculates constraints based on this intermediate repres
|
||||
which are then solved by the \unify{} algorithm
|
||||
resulting in a correctly typed program (see figure \ref{fig:nested-list-example-typed}).
|
||||
|
||||
\begin{itemize}
|
||||
\item
|
||||
We introduce the language \tifj{} (chapter \ref{sec:tifj}).
|
||||
A Featherweight Java derivative including Generics, Wildcards and Type Inference.
|
||||
\item
|
||||
We support capture conversion and Java style method calls.
|
||||
This requires existential types in a form which is not denotable by Java syntax \cite{aModelForJavaWithWildcards}.
|
||||
The algorithm is able find the correct type for the method \texttt{m} in the following example:
|
||||
\begin{verbatim}
|
||||
<X> Pair<X,X> make(List<X> l)
|
||||
Boolean compare(Pair<X,X> p)
|
||||
|
||||
List<?> b;
|
||||
Boolean m() = this.compare(this.make(b));
|
||||
\end{verbatim}
|
||||
|
||||
|
||||
\item
|
||||
We present a novel approach to deal with existential types and capture conversion during constraint unification.
|
||||
The algorithm is split in two parts. A constraint generation step and an unification step.
|
||||
|
||||
\item
|
||||
We proof soundness and aim for a good compromise between completeness and time complexity.
|
||||
Our algorithm finds a correct type solution for the following example, where the Java local type inference fails:
|
||||
\begin{verbatim}
|
||||
class SuperPair<A,B>{
|
||||
A a;
|
||||
B b;
|
||||
}
|
||||
class Pair<A,B> extends SuperPair<B,A>{
|
||||
A a;
|
||||
B b;
|
||||
\end{itemize}
|
||||
% Our algorithm finds a correct type solution for the following example, where the Java local type inference fails:
|
||||
% \begin{verbatim}
|
||||
% class SuperPair<A,B>{
|
||||
% A a;
|
||||
% B b;
|
||||
% }
|
||||
% class Pair<A,B> extends SuperPair<B,A>{
|
||||
% A a;
|
||||
% B b;
|
||||
|
||||
<X> X choose(X a, X b){ return b; }
|
||||
% <X> X choose(X a, X b){ return b; }
|
||||
|
||||
String m(List<? extends Pair<Integer, String>> a, List<? extends Pair<Integer, String>> b){
|
||||
return choose(choose(a,b).value.a,b.value.b);
|
||||
}
|
||||
}
|
||||
\end{verbatim}
|
||||
% String m(List<? extends Pair<Integer, String>> a, List<? extends Pair<Integer, String>> b){
|
||||
% return choose(choose(a,b).value.a,b.value.b);
|
||||
% }
|
||||
% }
|
||||
% \end{verbatim}
|
||||
|
||||
\begin{figure}[tp]
|
||||
\begin{figure}%[tp]
|
||||
\begin{subfigure}[t]{\linewidth}
|
||||
\begin{lstlisting}[style=fgj]
|
||||
class List<A> {
|
||||
@ -125,7 +122,7 @@ class Example {
|
||||
% The goal is to proof soundness in respect to the type rules introduced by \cite{aModelForJavaWithWildcards}
|
||||
% and \cite{WildcardsNeedWitnessProtection}.
|
||||
|
||||
\begin{figure}[tp]
|
||||
\begin{figure}%[tp]
|
||||
\begin{subfigure}[t]{0.49\linewidth}
|
||||
\begin{lstlisting}[style=fgj]
|
||||
genList() {
|
||||
@ -165,43 +162,210 @@ List<?> genList() {
|
||||
% \texttt{List<Object>} is not a valid return type for the method \texttt{genList}.
|
||||
% The type inference algorithm has to find the correct type involving wildcards (\texttt{List<?>}).
|
||||
|
||||
\subsection{Java Wildcards}
|
||||
Wildcards are expressed by a \texttt{?} in Java and can be used as type parameters.
|
||||
Wildcards add variance to Java type parameters.
|
||||
Generally Java has invariant subtyping for polymorphic types.
|
||||
A \texttt{List<String>} is not a subtype of \texttt{List<Object>} for example
|
||||
even though it seems intuitive with \texttt{String} being a subtype of \texttt{Object}.
|
||||
|
||||
Wildcards can be formalized as existential types \cite{WildFJ}.
|
||||
\texttt{List<? extends Object>} and \texttt{List<? super String>} are both wildcard types
|
||||
denoted in our syntax by $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$ and
|
||||
$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
|
||||
|
||||
The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound at the same time,
|
||||
and a type they are bound to.
|
||||
In this case the name is $\rwildcard{X}$ and it's bound to the the type \texttt{List}.
|
||||
|
||||
Those properties are needed to formalize capture conversion.
|
||||
Polymorphic method calls need to be wraped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
|
||||
In Java this is done implicitly in a process called capture conversion.
|
||||
|
||||
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}
|
||||
%like $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$
|
||||
%or $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$
|
||||
can emerge, which have no equivalent in the Java syntax.
|
||||
%Our type inference algorithm uses existential types internally but spawns type solutions compatible with Java.
|
||||
|
||||
Example: % This program is not typable with the Type Inference algorithm from Plümicke
|
||||
\begin{verbatim}
|
||||
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{verbatim}
|
||||
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=letfj]
|
||||
let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in <X>shuffle(l2d')
|
||||
\end{lstlisting}
|
||||
|
||||
The respective constraints are:
|
||||
\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}
|
||||
|
||||
\texttt{l} however has the type
|
||||
$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
|
||||
The method call \texttt{shuffle(l)} is not correct, because there is no solution for the subtype constraint:
|
||||
|
||||
$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$
|
||||
|
||||
\section{Type Inference for Capture Conversion}
|
||||
why do we need a lessdotCC constraint
|
||||
\dbox{Eine dashbox!}
|
||||
input is e.m(e);
|
||||
\begin{recap}\textbf{TI for FGJ without Wildcards:}
|
||||
- usually the type of e must be subtypes of the method parameters
|
||||
- in case of a polymorphic method: type placeholders resemble type parameters
|
||||
\end{recap}
|
||||
involving wildcards:
|
||||
- depending on the type of e a capture conversion must be applied first
|
||||
- the captured type N must be a subtype of the method parameters
|
||||
- type parameters: can be set to free variables!
|
||||
- but must afterwards be closed again
|
||||
- the free variables can only be used inside the let statement
|
||||
- we align the let statements in a way thate mimics Java capture conversion:
|
||||
|
||||
|
||||
% $\exptype{List}{String} <: \wctype{\wildcard{X}{\bot}{\type{Object}}}{List}{\rwildcard{X}}$
|
||||
% means \texttt{List<String>} is a subtype of \texttt{List<? extend Object>}.
|
||||
|
||||
\subsection{Global Type Inference}
|
||||
A global type inference algorithm works on an input with no type annotations at all.
|
||||
%TODO: Describe global type inference and lateron why it is so hard to
|
||||
Global type inference means that there are no type annotations at all.
|
||||
\begin{verbatim}
|
||||
m(l) {
|
||||
return l.add(l);
|
||||
}
|
||||
\end{verbatim}
|
||||
% A global type inference algorithm works on an input with no type annotations at all.
|
||||
% \begin{verbatim}
|
||||
% m(l) {
|
||||
% return l.add(l);
|
||||
% }
|
||||
% \end{verbatim}
|
||||
|
||||
$\tv{l} \lessdotCC \exptype{List}{\wtv{x}}, \tv{l} \lessdotCC \wtv{x}$
|
||||
% $\tv{l} \lessdotCC \exptype{List}{\wtv{x}}, \tv{l} \lessdotCC \wtv{x}$
|
||||
|
||||
\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}
|
||||
|
||||
No capture conversion for methods in the same class:
|
||||
Given two methods without type annotations like
|
||||
\begin{verbatim}
|
||||
// m :: () -> r
|
||||
m() = new List<String>() :? new List<Integer>();
|
||||
The input to our type inference algorithm is a modified version of the \letfj{}\cite{WildcardsNeedWitnessProtection} calculus (see chapter \ref{sec:tifj}).
|
||||
First \fjtype{} generates constraints
|
||||
and afterwards \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 also be a type placeholders $\ntv{a}$ or a wildcard type placeholder $\wtv{a}$.
|
||||
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.
|
||||
|
||||
// id :: (a) -> a
|
||||
id(a) = a
|
||||
\end{verbatim}
|
||||
%show input and a correct letFJ representation
|
||||
%TODO: first show local type inference and explain lessdotCC constraints. then show example with global TI
|
||||
\begin{figure}[h]
|
||||
\begin{subfigure}[t]{0.47\textwidth}
|
||||
\centering
|
||||
\begin{lstlisting}[style=tfgj, caption=Valid Java program, label=lst:addExample]
|
||||
<A> List<A> add(List<A> l, A v) ...
|
||||
|
||||
and a method call \texttt{id(m())} would lead to the constraints:
|
||||
$\exptype{List}{\type{String}} \lessdot \ntv{r},
|
||||
\exptype{List}{\type{Integer}} \lessdot \ntv{r},
|
||||
\ntv{r} \lessdot \ntv{a}$
|
||||
List<? super String> l = ...;
|
||||
add(l, "String");
|
||||
\end{lstlisting}
|
||||
\end{subfigure}\hfill
|
||||
\begin{subfigure}[t]{0.47\textwidth}
|
||||
\centering
|
||||
\begin{lstlisting}[style=letfj, caption=\letfj{} representation, label=lst:addExampleLet]
|
||||
<A> List<A> add(List<A> l, A v)
|
||||
|
||||
In this example capture conversion is not applicable,
|
||||
because the \texttt{id} method is not polymorphic.
|
||||
The type solution provided by \unify{} for this constraint set is:
|
||||
$\sigma(\ntv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}},
|
||||
\sigma(\ntv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$
|
||||
\begin{verbatim}
|
||||
List<?> m() = new List<String>() :? new List<Integer>();
|
||||
List<?> id(List<?> a) = a
|
||||
\end{verbatim}
|
||||
let l2 : (*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l
|
||||
in <X>add(l2, "String");
|
||||
\end{lstlisting}
|
||||
\end{subfigure}
|
||||
\end{figure}
|
||||
|
||||
The Example in listing \ref{lst:addExample} is a valid Java program. Here Java uses local type inference \cite{JavaLocalTI}
|
||||
to determine the type parameters to the \texttt{add} method call.
|
||||
In \letfj{} there is no local type inference and all type parameters for a method call are mandatory (see listing \ref{lst:addExampleLet}).
|
||||
If wildcards are involved the so called capture conversion has to be done manually via let statements.
|
||||
%A let statement \emph{opens} an existential type.
|
||||
In the body of the let statement the \textit{capture type} $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$
|
||||
becomes $\exptype{List}{\rwildcard{X}}$ and the wildcard $\wildcard{X}{\type{Object}}{\type{String}}$ is free and can be used as
|
||||
a type parameter to \texttt{<X>add(...)}.
|
||||
%This is a valid Java program where the type parameters for the polymorphic method \texttt{add}
|
||||
%are determined by local type inference.
|
||||
Our type inference algorithm has to add let statements if necessary, including the capture types.
|
||||
|
||||
Lets have a look at the constraints generated by \fjtype{} for the example in listing \ref{lst:addExample}:
|
||||
\begin{constraintset}
|
||||
\begin{center}
|
||||
$\begin{array}{c}
|
||||
\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}, \, \type{String} \lessdotCC \wtv{a}
|
||||
\\
|
||||
\hline
|
||||
\textit{Capture Conversion:}\ \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
|
||||
\\
|
||||
\hline
|
||||
\textit{Solution:}\ \wtv{a} \doteq \rwildcard{X} \implies \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\rwildcard{X}}, \, \type{String} \lessdot \rwildcard{X}
|
||||
\end{array}
|
||||
$
|
||||
\end{center}
|
||||
\end{constraintset}
|
||||
%Why do we need the lessdotCC constraints here?
|
||||
The type of \texttt{l} can be capture converted by a let statement if needed (see listing \ref{lst:addExampleLet}).
|
||||
Therefore we assign the constraint $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$
|
||||
which allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
|
||||
\textit{Note:} The constraint $\type{String} \lessdot \rwildcard{X}$ is satisfied because $\rwildcard{X}$ has $\type{String}$ as lower bound.
|
||||
|
||||
% No capture conversion for methods in the same class:
|
||||
% Given two methods without type annotations like
|
||||
% \begin{verbatim}
|
||||
% // m :: () -> r
|
||||
% m() = new List<String>() :? new List<Integer>();
|
||||
|
||||
% // id :: (a) -> a
|
||||
% id(a) = a
|
||||
% \end{verbatim}
|
||||
|
||||
% and a method call \texttt{id(m())} would lead to the constraints:
|
||||
% $\exptype{List}{\type{String}} \lessdot \ntv{r},
|
||||
% \exptype{List}{\type{Integer}} \lessdot \ntv{r},
|
||||
% \ntv{r} \lessdotCC \ntv{a}$
|
||||
|
||||
% In this example capture conversion is not applicable,
|
||||
% because the \texttt{id} method is not polymorphic.
|
||||
% The type solution provided by \unify{} for this constraint set is:
|
||||
% $\sigma(\ntv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}},
|
||||
% \sigma(\ntv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$
|
||||
% \begin{verbatim}
|
||||
% List<?> m() = new List<String>() :? new List<Integer>();
|
||||
% List<?> id(List<?> a) = a
|
||||
% \end{verbatim}
|
||||
|
||||
The following example has the \texttt{id} method already typed and the method \texttt{m}
|
||||
extended by a recursive call \texttt{id(m())}:
|
||||
@ -227,85 +391,10 @@ List<?> m() = new List<String>() :? new List<Integer>() :? id(m());
|
||||
\end{verbatim}
|
||||
|
||||
|
||||
\subsection{Java Wildcards}
|
||||
Wildcards are expressed by a \texttt{?} in Java and can be used as parameter types.
|
||||
Wildcards can be formalized as existential types \cite{WildFJ}.
|
||||
\texttt{List<? extends Object>} and \texttt{List<? super String>} are both wildcard types
|
||||
denoted in our syntax by $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$ and
|
||||
$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
|
||||
|
||||
Wildcards add variance to Java type parameters.
|
||||
Generally Java has invariant subtyping for polymorphic types.
|
||||
A \texttt{List<String>} is not a subtype of \texttt{List<Object>} for example
|
||||
even though it seems intuitive with \texttt{String} being a subtype of \texttt{Object}.
|
||||
|
||||
|
||||
$\exptype{List}{String} <: \wctype{\wildcard{X}{\bot}{\type{Object}}}{List}{\rwildcard{X}}$
|
||||
means \texttt{List<String>} is a subtype of \texttt{List<? extend Object>}.
|
||||
The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound at the same time,
|
||||
and a type they are bound to.
|
||||
In this case the name is $\rwildcard{X}$ and it's bound to the the type \texttt{List}.
|
||||
|
||||
Those properties are needed to formalize capture conversion.
|
||||
Polymorphic method calls need to be wraped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
|
||||
In Java this is done implicitly in a process called capture conversion.
|
||||
When calling a polymorphic method like \texttt{<X> List<X> m(List<X> l1, List<X> l2)} with a \texttt{List<?>}
|
||||
it is not possible to substitute \texttt{?} for \texttt{X}.
|
||||
This would lead to the method header \texttt{List<?> m(List<?> l1, List<?> l2)}
|
||||
where now a method invocation with \texttt{List<String>} and \texttt{List<Integer>} would be possible,
|
||||
because both are subtypes of \texttt{List<?>}.
|
||||
Capture conversion solves this problem by generating a fresh type variable for every wildcard.
|
||||
Calling \texttt{<X> X head(List<X> l1)} with the type \texttt{List<?>} ($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$)
|
||||
creates a fresh type variable $\rwildcard{Y}$ resulting in
|
||||
$\generics{\rwildcard{Y}}\texttt{head}(\exptype{List}{\rwildcard{Y}})$
|
||||
with $\rwildcard{Y}$ being used as generic parameter \texttt{X}.
|
||||
The $\rwildcard{Y}$ in $\exptype{List}{\rwildcard{Y}}$ is a free variable now.
|
||||
|
||||
%TODO: Read taming wildcards and see if we solve some of the problems presented in section 5 and 6
|
||||
|
||||
% Additionally they can hold a upper or lower bound restriction like \texttt{List<? super String>}.
|
||||
% Our representation of this type is: $\wctype{\wildcard{X}{\type{String}}{\type{Object}}}{List}{\rwildcard{X}}$
|
||||
% Every wildcard has a name ($\rwildcard{X}$ in this case) and an upper and lower bound (respectively \texttt{Object} and \texttt{String}).
|
||||
|
||||
% \subsection{Extensibility} % NOTE: this thing is useless, because final local variables do not need to contain wildcards
|
||||
% In \cite{WildcardsNeedWitnessProtection} capture converson is made explicit with \texttt{let} statements.
|
||||
% We chain let statements in a way that emulates Java behaviour. Allowing the example in \cite{aModelForJavaWithWildcards}
|
||||
% % TODO: Explain the advantage of constraints and how we control the way capture conversion is executed
|
||||
% But it would be also possible to alter the constraint generation step to include additional features.
|
||||
% Final variables or effectively final variables could be expressed with a
|
||||
% \begin{verbatim}
|
||||
% <X> concat(List<X> l1, List<X> l2){...}
|
||||
% \end{verbatim}
|
||||
% \begin{minipage}{0.50\textwidth}
|
||||
% Java:
|
||||
% \begin{verbatim}
|
||||
% final List<?> l = ...;
|
||||
% concat(l, l);
|
||||
% \end{verbatim}
|
||||
% \end{minipage}%
|
||||
% \begin{minipage}{0.50\textwidth}
|
||||
% Featherweight Java:
|
||||
% \begin{verbatim}
|
||||
% let l : X.List<X> = ... in
|
||||
% concat(l, l)
|
||||
% \end{verbatim}
|
||||
% \end{minipage}
|
||||
|
||||
|
||||
|
||||
|
||||
\subsection{Challenges}\label{challenges}
|
||||
%TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
|
||||
|
||||
|
||||
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.
|
||||
\texttt{List<List<?>>} equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
|
||||
During type checking intermediate types like $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$
|
||||
or $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ can emerge, which have no equivalent in the Java syntax.
|
||||
Our type inference algorithm uses existential types internally but spawns type solutions compatible with Java.
|
||||
|
||||
|
||||
The introduction of wildcards adds additional challenges.
|
||||
% we cannot replace every type variable with a wildcard
|
||||
Type variables can also be used as type parameters, for example
|
||||
@ -330,19 +419,11 @@ Knowing that the type \texttt{String} is a subtype of any type the wildcard \tex
|
||||
it is safe to pass \texttt{"String"} for the first parameter of the function.
|
||||
|
||||
\begin{verbatim}
|
||||
<A> List<A> add(A a, List<A> la) {}
|
||||
<A> List<A> add(List<A> l, A v) {}
|
||||
|
||||
List<? super String> list = ...;
|
||||
add("String", list);
|
||||
List<? super String> list = ...;
|
||||
add("String", list);
|
||||
\end{verbatim}
|
||||
The constraints representing this code snippet are:
|
||||
|
||||
\begin{displaymath}
|
||||
\type{String} \lessdotCC \wtv{a},\,
|
||||
\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}
|
||||
\end{displaymath}
|
||||
|
||||
Here $\sigma(\tv{a}) = \rwildcard{X}$ is a valid solution.
|
||||
\end{example}
|
||||
|
||||
\item \begin{example}\label{intro-example2}
|
||||
@ -350,117 +431,169 @@ This example displays an incorrect Java program.
|
||||
The method call to \texttt{concat} with two wildcard lists is unsound.
|
||||
Each list could be of a different kind and therefore the \texttt{concat} cannot succeed.
|
||||
\begin{verbatim}
|
||||
<A> List<A> concat(List<A> l1, List<A> l2) {}
|
||||
<A> List<A> concat(List<A> l1, List<A> l2) { ... }
|
||||
|
||||
List<?> list = ... ;
|
||||
concat(list, list);
|
||||
List<?> list = ... ;
|
||||
concat(list, list);
|
||||
\end{verbatim}
|
||||
The constraints for this example are:
|
||||
|
||||
$\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}, \\
|
||||
\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
|
||||
%$\exptype{List}{?} \lessdot \exptype{List}{\tv{a}},
|
||||
%\exptype{List}{?} \lessdot \exptype{List}{\tv{a}}$
|
||||
|
||||
Remember that the given constraints cannot have a valid solution.
|
||||
%This is due to the fact that the wildcard variables cannot leave their scope.
|
||||
In this example the \unify{} algorithm should not replace $\tv{a}$ with the captured wildcard $\rwildcard{X}$.
|
||||
% $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}, \\
|
||||
% \wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
|
||||
\end{example}
|
||||
|
||||
\item
|
||||
\unify{} can only remove wildcards, but never add wildcards to an existing type.
|
||||
Java subtyping is invariant.
|
||||
The type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ cannot be a subtype of $\exptype{List}{\tv{a}}$
|
||||
% \item
|
||||
% \unify{} morphs a constraint set into a correct type solution
|
||||
% 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>()
|
||||
|
||||
\unify{} morphs a constraint set into a correct type solution
|
||||
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}
|
||||
List<?> l = ...;
|
||||
|
||||
m2() {
|
||||
l.add(l.head());
|
||||
}
|
||||
\end{verbatim}
|
||||
The type for \texttt{l} can be any kind of 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.
|
||||
% add(anyList(), anyList().head());
|
||||
% \end{verbatim}
|
||||
% The type for \texttt{l} can be any kind of 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.
|
||||
|
||||
|
||||
\end{itemize}
|
||||
|
||||
The \unify{} algorithm only sees the constraints with no information about the program they originated from.
|
||||
The main challenge was to find an algorithm which computes $\sigma(\tv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}.
|
||||
% Solution: A type variable can only take one type and not a wildcard type.
|
||||
% A wildcard type is only treated like a wildcard while his definition is in scope (during the reduce rule)
|
||||
The main challenge was to find an algorithm which computes $\sigma(\wtv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}.
|
||||
|
||||
\subsection{Capture Conversion}
|
||||
The input to our type inference algorithm does not contain let statements.
|
||||
Those are added after computing a type solution.
|
||||
Let statements act as capture conversion and only have to be applied in method calls involving wildcard types.
|
||||
|
||||
\begin{figure}
|
||||
\begin{minipage}{0.45\textwidth}
|
||||
\begin{lstlisting}[style=fgj]
|
||||
<X> List<X> clone(List<X> l);
|
||||
example(p){
|
||||
return clone(p);
|
||||
}
|
||||
\end{lstlisting}
|
||||
\end{minipage}%
|
||||
\hfill
|
||||
\begin{minipage}{0.5\textwidth}
|
||||
\begin{lstlisting}[style=tfgj]
|
||||
(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
|
||||
return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in
|
||||
clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
|
||||
}
|
||||
\end{lstlisting}
|
||||
\end{minipage}
|
||||
\caption{Type inference adding capture conversion}\label{fig:addingLetExample}
|
||||
\end{figure}
|
||||
|
||||
Figure \ref{fig:addingLetExample} shows a let statement getting added to the typed output.
|
||||
The method \texttt{clone} cannot be called with the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
|
||||
After a capture conversion \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ with $\rwildcard{X}$ being a free variable.
|
||||
Afterwards we have to find a supertype of $\exptype{List}{\rwildcard{X}}$, which does not contain free variables
|
||||
($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in this case).
|
||||
|
||||
During the constraint generation step most types are not known yet and are represented by a type placeholder.
|
||||
During a methodcall like the one in the \texttt{example} method in figure \ref{fig:ccExample} the type of the parameter \texttt{p}
|
||||
is not known yet.
|
||||
The type \texttt{List<?>} would be one possibility as a parameter type for \texttt{p}.
|
||||
To make wildcards work for our type inference algorithm \unify{} has to apply capture conversions if necessary.
|
||||
|
||||
The type placeholder $\tv{r}$ is the return type of the \texttt{example} method.
|
||||
One possible type solution is $\tv{p} \doteq \tv{r} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$,
|
||||
which leads to:
|
||||
\begin{verbatim}
|
||||
List<?> example(List<?> p){
|
||||
return clone(p);
|
||||
}
|
||||
\end{verbatim}
|
||||
|
||||
But by substituting $\tv{p} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in the constraint
|
||||
$\tv{p} \lessdotCC \exptype{List}{\wtv{x}}$ leads to
|
||||
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$.
|
||||
|
||||
To make this typing possible we have to introduce a capture conversion via a let statement:
|
||||
$\texttt{return}\ (\texttt{let}\ \texttt{x} : \wctype{\rwildcard{X}}{List}{\rwildcard{X}} = \texttt{p}\ \texttt{in} \
|
||||
\texttt{clone}\generics{\rwildcard{X}}(x) : \wctype{\rwildcard{X}}{List}{\rwildcard{X}})$
|
||||
|
||||
Inside the let statement the variable \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$
|
||||
|
||||
|
||||
% \subsection{Capture Conversion}
|
||||
% \begin{verbatim}
|
||||
% <A> List<A> add(A a, List<A> la) {}
|
||||
This spawns additional problems.
|
||||
|
||||
% List<? super String> list = ...;
|
||||
\begin{figure}
|
||||
\begin{minipage}{0.45\textwidth}
|
||||
\begin{verbatim}
|
||||
<X> List<X> clone(List<X> l){...}
|
||||
|
||||
% add("String", list);
|
||||
% \end{verbatim}
|
||||
% The constraints representig this code snippet are:
|
||||
% $\type{String} \lessdot \tv{a},
|
||||
% \wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\tv{a}}$
|
||||
% Under the hood the typechecker has to find a replacement for the generic method parameter \texttt{A}.
|
||||
example(p){
|
||||
return clone(p);
|
||||
}
|
||||
\end{verbatim}
|
||||
\end{minipage}%
|
||||
\hfill
|
||||
\begin{minipage}{0.35\textwidth}
|
||||
\begin{constraintset}
|
||||
\textbf{Constraints:}\\
|
||||
$
|
||||
\tv{p} \lessdotCC \exptype{List}{\wtv{x}}, \\
|
||||
\tv{p} \lessdot \tv{r}, \\
|
||||
\tv{p} \lessdot \type{Object},
|
||||
\tv{r} \lessdot \type{Object}
|
||||
$
|
||||
\end{constraintset}
|
||||
\end{minipage}
|
||||
|
||||
% Java allows a method \texttt{<A> List<A> add(A a, List<A> la)} to be called with
|
||||
% \texttt{String} and \texttt{List<? super String>}.
|
||||
% A naive approach would be to treat wildcards like any other type and replace \texttt{A}
|
||||
% with \texttt{? super String}.
|
||||
% Generating the method type \texttt{List<? super String> add(? super String a, List<? super String> la)}.
|
||||
\caption{Type inference example}\label{fig:ccExample}
|
||||
\end{figure}
|
||||
|
||||
% This does not work for a method like
|
||||
% \texttt{<A> void merge(List<A> l1, List<A> l2)}.
|
||||
% It is crucial for this method to be called with two lists of the same type.
|
||||
% Substituting a wildcard for the generic \texttt{A} leads to
|
||||
% \texttt{void merge(List<?> l1, List<?> l2)},
|
||||
% which is unsound.
|
||||
In addition with free variables this leads to unwanted behaviour.
|
||||
Take the constraint
|
||||
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ for example.
|
||||
After a capture conversion from $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ to $\exptype{List}{\rwildcard{Y}}$ and a substitution $\wtv{a} \doteq \rwildcard{Y}$
|
||||
we get
|
||||
$\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$.
|
||||
Which is correct if we apply capture conversion to the left side:
|
||||
$\exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$
|
||||
If the input constraints did not intend for this constraint to undergo a capture conversion then \unify{} would produce an invalid
|
||||
type solution due to:
|
||||
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \nless: \exptype{List}{\rwildcard{X}}$
|
||||
The reason for this is the \texttt{S-Exists} rule's premise
|
||||
$\text{dom}(\Delta') \cap \text{fv}(\exptype{List}{\rwildcard{X}}) = \emptyset$.
|
||||
|
||||
% Capture conversion utilizes the fact that instantiated classes always have an actual type.
|
||||
% \texttt{new List<String>()} and \texttt{new List<Object>()} are
|
||||
% valid instances.
|
||||
% \texttt{new List<? super String>()} is not.
|
||||
% Every type $\wcNtype{\Delta}{N}$ contains an underlying instance of a type $\type{N}$.
|
||||
% Knowing this fact allows to make additional assumptions.
|
||||
Additionally free variables are not allowed to leave the scope of a capture conversion
|
||||
introduced by a let statement.
|
||||
%TODO we combat both of this with wildcard type placeholders (? flag)
|
||||
|
||||
% \wildFJ{} type rules allow for generic parameters to be replaced by wildcard types.
|
||||
% This is possible because wildcards are split into two parts.
|
||||
% Their declaration at the environment part $\Delta$ of a type $\wcNtype{\Delta}{N}$
|
||||
% and their actual use in the body of the type $\type{N}$.
|
||||
% Replacing the generic \texttt{A} in the type \texttt{List<A>}
|
||||
% by a wildcard $\type{X}$ will not generate the type \texttt{List<?>}.
|
||||
% \texttt{List<?>} is the equivalent of $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\type{X}}$.
|
||||
% The generated type here is $\exptype{List}{\type{X}}$, which has different subtype properties.
|
||||
% There is no information about what the type $\exptype{List}{\type{X}}$ actually is.
|
||||
% It has itself as a subtype and for example a type like $\exptype{ArrayList}{\type{X}}$.
|
||||
|
||||
% A method call for example only works with values, which are correct instances of classes.
|
||||
% Capture conversion automatically converts wildcard type to a concrete class type,
|
||||
% which then can be used as a parameter for a method call.
|
||||
|
||||
% In \wildFJ{} this is done via let statements.
|
||||
|
||||
% Written in FJ syntax: $\type{N}$ is a initialized type and
|
||||
% $\wcNtype{\Delta}{N}$ is a type containing wildcards $\Delta$.
|
||||
|
||||
% It is crucial for the wildcard names to never be used twice.
|
||||
% Otherwise the members of a list with type $\wctype{\type{X}}{List}{\type{X}}$ and
|
||||
% a list with type $\wctype{\type{X}}{List}{\type{X}}$ would be the same. $\type{X}$ in fact.
|
||||
|
||||
% The let statement adds wildcards to the environment.
|
||||
% Those wildcards are not allowed to escape the scope of the let statement.
|
||||
% Which is a problem for our type inference algorithm.
|
||||
|
||||
% The capture converted version of the type $\wctype{\rwildcard{X}}{Box}{\rwildcard{X}}$ is
|
||||
% $\exptype{Box}{\rwildcard{X}}$.
|
||||
% The captured type is only used as an intermediate type during a method call.
|
||||
Type placeholders which are not flagged as possible free variables ($\wtv{a}$) can never hold a free variable or a type containing free variables.
|
||||
Constraint generation places these standard place holders at method return types and parameter types.
|
||||
\begin{lstlisting}[style=fgj]
|
||||
<X> List<X> clone(List<X> l);
|
||||
(*@$\red{\tv{r}}$@*) example((*@$\red{\tv{p}}$@*) p){
|
||||
return clone(p);
|
||||
}
|
||||
\end{lstlisting}
|
||||
This prevents type solutions that contain free variables in parameter and return types.
|
||||
When calling a method which already has a type annotation we have to consider adding a capture conversion in form of a let statement.
|
||||
The constraint $\tv{p} \lessdot \exptype{List}{\wtv{x}}$ signals the \unify{} algorithm that here a capture conversion is possible.
|
||||
$\sigma(\tv{p}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, \sigma(\tv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, $ is a possible solution.
|
||||
But only when adding a capture conversion:
|
||||
\begin{lstlisting}[style=fgj]
|
||||
<X> List<X> clone(List<X> l);
|
||||
(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
|
||||
return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
|
||||
}
|
||||
\end{lstlisting}
|
||||
|
||||
Capture constraints cannot be stored in a set.
|
||||
$\wtv{a} \lessdotCC \wtv{b}$ is not the same as $\wtv{a} \lessdotCC \wtv{b}$.
|
||||
Both constraints will end up the same after a substitution for both placeholders $\tv{a}$ and $\tv{b}$.
|
||||
But afterwards a capture conversion is applied, which can generate different types on the left sides.
|
||||
\begin{itemize}
|
||||
\item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Y}}$
|
||||
\item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Z}}$
|
||||
\end{itemize}
|
||||
121
letfjTransformation.tex
Normal file
121
letfjTransformation.tex
Normal file
@ -0,0 +1,121 @@
|
||||
|
||||
%We could do a translation from Java to \wildFJ explaining implicit capture conversion
|
||||
|
||||
\section{Soundness of Typing}
|
||||
|
||||
|
||||
We show soundness with the type rules statet in \cite{WildcardsNeedWitnessProtection}.
|
||||
A correct \FGJGT{} program can be converted to a correct \wildFJ{} program.
|
||||
|
||||
\begin{figure}
|
||||
$\begin{array}{rcl}
|
||||
| \texttt{x} |
|
||||
& = & \texttt{x} \\
|
||||
| \texttt{let} \ \texttt{x} : \type{T} = \texttt{e},\, \ol{x} : \ol{T} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x}) |
|
||||
& = & |\texttt{e}|.\texttt{m}(\ol{|e|}) \\
|
||||
| \texttt{let} \ \texttt{x} : \type{T} = \texttt{e}\ \texttt{in}\ \texttt{x}.\texttt{f} |
|
||||
& = & |\texttt{e}|.\texttt{f} \\
|
||||
| \texttt{e} \elvis{} \texttt{e} |
|
||||
& = & |\texttt{e}| \elvis{} |\texttt{e}| \\
|
||||
\end{array}$
|
||||
\caption{Erasure} \label{fig:erasure}
|
||||
\end{figure}
|
||||
|
||||
% A constraint Pair<A,B> <. a, then a has infinite possibilities:
|
||||
% a =. X.Pair<X,X>
|
||||
% a =. X,Y.Pair<X,Y>
|
||||
% a =. X.Pair<Pair<X,X>,X>
|
||||
% a =. X,Y.Pair<Pair<X,Y>,X>
|
||||
% a =. X,Y.Pair<Pair<X,Y>,Y>
|
||||
|
||||
% There is no way to try out every single one of them.
|
||||
|
||||
Starting with the parameters of the method we gradually add every expression which only contains already captured expressions.
|
||||
|
||||
We have a typed expression
|
||||
|
||||
$|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} : \type{T} = \texttt{x in}$
|
||||
$|\texttt{e.f}, \texttt{r}| = |\texttt{e}, x| \texttt{let} r = x.\texttt{f} \ \texttt{in}$
|
||||
$|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} = \texttt{x in}$
|
||||
%TODO: write the transform rules:
|
||||
% |e.f, ret| = |e, r| let ret = r.f in
|
||||
% |x, ret| = let ret = x in
|
||||
% |e.m(e_), ret| = |e, r| |e_, a_| let ret = r.m(a_) in
|
||||
|
||||
Erasure functions:
|
||||
$|\texttt{x}| = \texttt{let r} : \wcNtype{\Delta}{N} = \texttt{x in r}$
|
||||
|
||||
$\texttt{x} \longmapsto \texttt{let}\ \texttt{xx} : \type{T} = \texttt{x in xx}$
|
||||
$\texttt{x}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in xf}$
|
||||
|
||||
$\begin{array}{l}
|
||||
\texttt{e} \longmapsto \texttt{let}\ \texttt{xe} : \type{T} = \texttt{e}' \ \texttt{in xe} \\
|
||||
\hline
|
||||
\vspace*{-0.4cm}\\
|
||||
\texttt{e}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in x}.f
|
||||
\end{array}$
|
||||
|
||||
Example:
|
||||
m(a, b) = a.m(b.f);
|
||||
|
||||
let xa = a in let xb = b in let xf = xb.f in let xm = xa.m(xf) in xm
|
||||
|
||||
% TODO: Now we have to proof that there is a LetFJ program for every TIFJ program!
|
||||
% |let xr : T = x1.m(x2) in e| = [x1.m(x2)/xr]|e|
|
||||
% |let xf : T = x1.f in e| = [x1.f/xf]|e|
|
||||
% |let xr : T = x in e| = [xr/x]|e|
|
||||
% |new C(x)| = new C(x)
|
||||
|
||||
% | let xr : T' = x in let xf : T = xr.f | = x.f
|
||||
|
||||
|
||||
% let x : T' = e' in x = |e|
|
||||
% ---------------------------------
|
||||
% | let xr : T' = x in let xf : T = xr.f | = x.f
|
||||
|
||||
|
||||
|
||||
% let x : T' = e' in x = |e|
|
||||
% -----------
|
||||
% =
|
||||
|
||||
We need a language which only has let statemnts and expressions on capture converted variables
|
||||
|
||||
The idea is to use wildcard placeholders inside the method. Also in the bounds of wildcards.
|
||||
This makes it possible to replace wildcards with free variables by setting upper and lower bound to that free variable.
|
||||
Free variables then can flow freely inside the method body.
|
||||
We have to show that a type solution implies that there is a possible transformation to a correct typed letFJ program.
|
||||
If there is a possible method type then there must exist a let configuration.
|
||||
% By starting with the parameter types and capturing them. Afterwards every capture creates free variables which are used inside
|
||||
% TODO: Proof!
|
||||
|
||||
The normal type placeholders represent denotable types.
|
||||
|
||||
%TODO: the type rules stay the same. We generate let statements in a fashion which removes all wildcard types.
|
||||
% what about wildcards getting returned by untyped methods? they can also be captured
|
||||
% TODO: try soundness proof on the original type rules!
|
||||
|
||||
Removing of extensive wildcards:
|
||||
$
|
||||
\wctype{\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{X}, \rwildcard{Y}}
|
||||
\lessdot \wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}} \\
|
||||
\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \wtv{x}, \rwildcard{Y} \doteq \wtv{x} \\
|
||||
\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \rwildcard{Y} \\
|
||||
\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
|
||||
\implies \wctype{\wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{Y}, \rwildcard{Y}}, \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
|
||||
$
|
||||
|
||||
%e.f leads to constraints: r <c C<x> with return type equals the field type T.
|
||||
% T can contain free variables from r. but also it can be used in another constraint and get free variables from inner let statements
|
||||
% X.C<X> <c C<x> -> then T contains X variables
|
||||
|
||||
% let x1 = p1, x2 = p2 in
|
||||
% let r1 = x1 in let r2 = p2 in let f1 = r2.f in let r3 = x1 in let m2 = r3.m2() let ret = r1.m(f1,m2)
|
||||
% in ret
|
||||
|
||||
What about method invocation with no type yet. m2 :: a -> a
|
||||
they are also encased in let expression so the return type can be capture converted.
|
||||
Those methods and the parameter types of the current method are the only things not typed.
|
||||
All the other types cannot change their type. The captured wildcards can only flow from top to bottom.
|
||||
The return type of untyped methods has to be well-formed and cannot contain free variables.
|
||||
Therefore no free variables will flow into those types.
|
||||
39
martin.bib
39
martin.bib
@ -388,4 +388,43 @@ numpages = {14},
|
||||
keywords = {existential types, joins, parametric types, single-instantiation inheritance, subtyping, type inference, wildcards}
|
||||
}
|
||||
|
||||
@inproceedings{10.1145/1449764.1449804,
|
||||
author = {Smith, Daniel and Cartwright, Robert},
|
||||
title = {Java type inference is broken: can we fix it?},
|
||||
year = {2008},
|
||||
isbn = {9781605582153},
|
||||
publisher = {Association for Computing Machinery},
|
||||
address = {New York, NY, USA},
|
||||
url = {https://doi.org/10.1145/1449764.1449804},
|
||||
doi = {10.1145/1449764.1449804},
|
||||
abstract = {Java 5, the most recent major update to the Java Programming Language, introduced a number of sophisticated features, including a major extension to the type system. While the technical details of these new features are complex, much of this complexity is hidden from the typical Java developer by an ambitious type inference mechanism. Unfortunately, the extensions to the Java 5 type system were so novel that their technical details had not yet been thoroughly investigated in the research literature. As a result, the Java 5 compiler includes a pragmatic but flawed type inference algorithm that is, by design, neither sound nor locally complete. The language specification points out that neither of these failures is catastrophic: the correctness of potentially-unsound results must be verified during type checking; and incompleteness can usually be worked around by manually providing the method type parameter bindings for a given call site.This paper dissects the type inference algorithm of Java 5 and proposes a signficant revision that is sound and able to calculate correct results where the Java 5 algorithm fails. The new algorithm is locally complete with the exception of a difficult corner case. Moreover, the new algorithm demonstrates that several arbitrary restrictions in the Java type system---most notably the ban on lower-bounded type parameter declarations and the limited expressibility of intersection types---are unnecessary. We hope that this work will spur the evolution of a more coherent, more comprehensive generic type system for Java.},
|
||||
booktitle = {Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications},
|
||||
pages = {505–524},
|
||||
numpages = {20},
|
||||
keywords = {bounded quantification, generics, intersection types, parameterized types, polymorphic methods, subtyping, type argument inference, type inference, union types, wildcards},
|
||||
location = {Nashville, TN, USA},
|
||||
series = {OOPSLA '08}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@article{JavaLocalTI,
|
||||
author = {Smith, Daniel and Cartwright, Robert},
|
||||
title = {Java type inference is broken: can we fix it?},
|
||||
year = {2008},
|
||||
issue_date = {September 2008},
|
||||
publisher = {Association for Computing Machinery},
|
||||
address = {New York, NY, USA},
|
||||
volume = {43},
|
||||
number = {10},
|
||||
issn = {0362-1340},
|
||||
url = {https://doi.org/10.1145/1449955.1449804},
|
||||
doi = {10.1145/1449955.1449804},
|
||||
abstract = {Java 5, the most recent major update to the Java Programming Language, introduced a number of sophisticated features, including a major extension to the type system. While the technical details of these new features are complex, much of this complexity is hidden from the typical Java developer by an ambitious type inference mechanism. Unfortunately, the extensions to the Java 5 type system were so novel that their technical details had not yet been thoroughly investigated in the research literature. As a result, the Java 5 compiler includes a pragmatic but flawed type inference algorithm that is, by design, neither sound nor locally complete. The language specification points out that neither of these failures is catastrophic: the correctness of potentially-unsound results must be verified during type checking; and incompleteness can usually be worked around by manually providing the method type parameter bindings for a given call site.This paper dissects the type inference algorithm of Java 5 and proposes a signficant revision that is sound and able to calculate correct results where the Java 5 algorithm fails. The new algorithm is locally complete with the exception of a difficult corner case. Moreover, the new algorithm demonstrates that several arbitrary restrictions in the Java type system---most notably the ban on lower-bounded type parameter declarations and the limited expressibility of intersection types---are unnecessary. We hope that this work will spur the evolution of a more coherent, more comprehensive generic type system for Java.},
|
||||
journal = {SIGPLAN Not.},
|
||||
month = {oct},
|
||||
pages = {505–524},
|
||||
numpages = {20},
|
||||
keywords = {wildcards, union types, type inference, type argument inference, subtyping, polymorphic methods, parameterized types, intersection types, generics, bounded quantification}
|
||||
}
|
||||
|
||||
|
||||
14
prolog.tex
14
prolog.tex
@ -4,16 +4,20 @@
|
||||
\lstset{language=Java,
|
||||
showspaces=false,
|
||||
showtabs=false,
|
||||
breaklines=true,
|
||||
%breaklines=true,
|
||||
showstringspaces=false,
|
||||
breakatwhitespace=true,
|
||||
%breakatwhitespace=true,
|
||||
basicstyle=\ttfamily\fontsize{8}{9.6}\selectfont, %\footnotesize
|
||||
escapeinside={(*@}{@*)},
|
||||
captionpos=b,
|
||||
captionpos=t,float,abovecaptionskip=-\medskipamount
|
||||
}
|
||||
\lstdefinestyle{fgj}{backgroundcolor=\color{lime!20}}
|
||||
\lstdefinestyle{tfgj}{backgroundcolor=\color{lightgray!20}}
|
||||
\lstdefinestyle{letfj}{backgroundcolor=\color{lightgray!20}}
|
||||
|
||||
\newtheorem{recap}[note]{Recap}
|
||||
|
||||
\newcommand{\tifj}{\texttt{TamedFJ}}
|
||||
|
||||
\newcommand\mv[1]{{\tt #1}}
|
||||
\newcommand{\ol}[1]{\overline{\tt #1}}
|
||||
@ -98,6 +102,7 @@
|
||||
\newcommand{\localVarAssumption}{\ensuremath{\mathtt{\eta}}}
|
||||
\newcommand{\expandLB}{\textit{expandLB}}
|
||||
|
||||
\newcommand{\letfj}{\emph{LetFJ}}
|
||||
\newcommand{\tph}{\text{tph}}
|
||||
|
||||
\def\exptypett#1#2{\texttt{#1}\textrm{{\tt <#2}}\textrm{{\tt >}}\xspace}
|
||||
@ -111,7 +116,8 @@
|
||||
\newcommand{\wtypestore}[3]{\ensuremath{#1 = \wtype{#2}{#3}}}
|
||||
%\newcommand{\wtype}[2]{\ensuremath{[#1\ #2]}}
|
||||
\newcommand{\wtv}[1]{\ensuremath{\tv{#1}_?}}
|
||||
\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
|
||||
%\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
|
||||
\newcommand{\ntv}[1]{\tv{#1}}
|
||||
\newcommand{\wcstore}{\ensuremath{\Delta}}
|
||||
|
||||
%\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}_?}}
|
||||
|
||||
@ -14,6 +14,44 @@ TODO: Beforehand we have to show that $\Delta \cup \overline{\Delta} | \Theta \v
|
||||
Here $\Delta$ does not contain every $\overline{\Delta}$ ever created.
|
||||
%what prevents a free variable to emerge in \Delta.N example Y^Object |- C<String> <: X^Y.C<X>
|
||||
% if the Y is later needed for an equals: same(id(x), x2)
|
||||
Free wildcards do not move inwards. We can show that every new type is either well-formed and therefore does not contain any free variables.
|
||||
Or it is a generic method call: is it possible to use any free wildcards here?
|
||||
let empty
|
||||
|
||||
<X> Box<X> empty()
|
||||
same(Box<?>, empty())
|
||||
let p1 : X.Box<X> = Box<?> in let
|
||||
X.Box<X> <. Box<x>
|
||||
Box<e> <. Box<x>
|
||||
|
||||
boxin(empty()), Box2<?>
|
||||
|
||||
Where can a problem arise? When we use free wildcards before they are freed.
|
||||
But we can always CC them first. Exception two types: X.Pair<X, y> and Y.Pair<x, Y>
|
||||
Here y = Y and x = X but
|
||||
|
||||
<X,Y> void same(Pair<X,Y> a, Pair<X,Y> b){}
|
||||
<X> Pair<?, X> left() { return null; }
|
||||
<X> Pair<X, ?> right() { return null; }
|
||||
|
||||
<X> Box<X> id(Box<? extends Box<X>> x)
|
||||
here it could be beneficial to use a free wildcard as the parameter X to have it later
|
||||
Box<?> x = ...
|
||||
same(id(x), id(x)) <- this will be accepted by TI
|
||||
|
||||
let left : X,Y.Pair<X,Y> = left() in
|
||||
let right : Pair<X,Y> = right() in
|
||||
|
||||
Compromise:
|
||||
- Generate constraints so that they comply with LetFJ
|
||||
- Propose a version which is close to Java
|
||||
|
||||
Version for LetFJ:
|
||||
Is it still possible to do the capture conversion in form of constraints?
|
||||
X.C<X> <. C<x>
|
||||
T <. X.C<X>
|
||||
how to proof: X.C<X> ok
|
||||
|
||||
|
||||
If $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
|
||||
then there exists a $|\texttt{e}|$ with $\Delta | \Theta \vdash |\texttt{e}| : \wcNtype{\Delta'}{N}$ in LetFJ.
|
||||
|
||||
124
tRules.tex
124
tRules.tex
@ -1,4 +1,4 @@
|
||||
\section{Syntax and Typing}
|
||||
\section{Syntax and Typing}\label{sec:tifj}
|
||||
|
||||
The input syntax for our algorithm is shown in figure \ref{fig:syntax}
|
||||
and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}.
|
||||
@ -8,6 +8,18 @@ The input language is designed to showcase type inference involving existential
|
||||
Method call rule T-Call is the most interesting part, because it emulates the behaviour of a Java method call,
|
||||
where existential types are implicitly \textit{opened} and \textit{closed}.
|
||||
|
||||
Example: %TODO
|
||||
\begin{verbatim}
|
||||
class List<A> {
|
||||
A head;
|
||||
List<A> tail;
|
||||
|
||||
add(v) = new List(v, this);
|
||||
}
|
||||
\end{verbatim}
|
||||
|
||||
%The rules depicted here are type inference rules. It is not possible to derive a distinct typing from a given input program.
|
||||
|
||||
%The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}.
|
||||
%and is solely used for examples.
|
||||
The calculus does not include method overriding for simplicity reasons.
|
||||
@ -35,11 +47,11 @@ $
|
||||
\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{Method declarations} & \texttt{M} & ::= & \texttt{m}(\overline{x}) = t \\
|
||||
\text{Terms} & t & ::= & x \\
|
||||
& & \ \ | & \texttt{new} \ \exptype{C}{\ol{T}}(\overline{t})\\
|
||||
& & \ \ | & \texttt{new} \ \type{C}(\overline{t})\\
|
||||
& & \ \ | & t.f\\
|
||||
& & \ \ | & t.\generics{\ol{T}}\texttt{m}(\overline{t})\\
|
||||
& & \ \ | & t.\texttt{m}(\overline{t})\\
|
||||
& & \ \ | & t \elvis{} t\\
|
||||
\text{Variable contexts} & \Gamma & ::= & \overline{x:\type{T}}\\
|
||||
\hline
|
||||
@ -214,68 +226,19 @@ $\begin{array}{l}
|
||||
\triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em] % TODO: we need subtyping for FJ without let statements. Problem is \Delta \vdash T witnessed. The \Delta here contains all the let statements beforehand.
|
||||
% TODO: maybe do a rule which adds let statements at any place! Goal: a program which Unify calculates a type for is also correct under our type laws and can be converted to LefFJ
|
||||
% motivation: do not use normal types as intermediate types. Keep a Pair<X,X> as that and not convert to X,Y.Pair<X,Y>
|
||||
% it is possible because the parameters of the method are normal types. we can start capture converting them
|
||||
% is it possible to say there exists any \Delta which makes the method body possible?
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Call}\\
|
||||
\begin{array}{@{}c}
|
||||
\Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\type{T}} \ \ok \quad \quad
|
||||
\Delta \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
|
||||
\generics{\ol{X \triangleleft U'}} \type{N} \to \ol{U} \to \type{U} \in \Pi(\texttt{m}) \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{e} : \type{T}_r \mid \Delta_G \quad \quad
|
||||
\Delta | \Gamma \vdash \ol{e} : \ol{T} \mid \overline{\Delta_G} \quad \quad
|
||||
\Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
|
||||
\Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
|
||||
\\
|
||||
\overline{\Delta_G}, \Delta_G, \Delta, \Delta', \overline{\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 \texttt{e}.\texttt{m}(\ol{e}) : \type{T} \mid \Delta', \overline{\Delta}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em]
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Call}\\
|
||||
\begin{array}{@{}c}
|
||||
\Delta \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
|
||||
\generics{\ol{X \triangleleft U'}}\ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
|
||||
\Delta \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
|
||||
\\
|
||||
\Delta \vdash \ol{S} \ \ok \quad \quad
|
||||
\Delta | \Gamma \vdash \texttt{e}, \ol{e} : \ol{T} \mid \overline{\Delta'} \quad \quad
|
||||
\Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}} \quad \quad
|
||||
\Delta \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T}
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T} \mid \overline{\Delta}, \overline{\Delta'}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
% \Delta is not allowed to have wildcards depending on eachother. X^Y, Y^T for example
|
||||
\\[1em]
|
||||
\\[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
|
||||
\generics{\ol{X \triangleleft U'}} \type{N} \to \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
|
||||
\generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \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{e} : \type{T}_r \quad \quad
|
||||
\Delta | \Gamma \vdash \ol{e} : \ol{T} \quad \quad
|
||||
\Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
|
||||
\Delta | \Gamma \vdash \texttt{e}, \ol{e} : \ol{T} \quad \quad
|
||||
\Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
|
||||
\\
|
||||
\Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
|
||||
\Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
|
||||
\Delta, \Delta', \overline{\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})}
|
||||
@ -286,26 +249,6 @@ $\begin{array}{l}
|
||||
\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
|
||||
\generics{\ol{X \triangleleft U'}} \type{N} \to \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
|
||||
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \quad \quad
|
||||
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok
|
||||
\\
|
||||
\Delta | \Gamma \vdash \ol{e} : \ol{T} \quad \quad
|
||||
\Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}} \quad \quad
|
||||
\Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
|
||||
\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
|
||||
\overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\Delta | \Gamma \vdash \texttt{m}(\ol{e}) : \type{T}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em]
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Elvis}\\
|
||||
\begin{array}{@{}c}
|
||||
@ -325,28 +268,10 @@ $\begin{array}{l}
|
||||
|
||||
\begin{figure}
|
||||
\begin{center}
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Method}\\
|
||||
% TODO: do a rule that forbids variables in Delta which are not introduced by a capture conversion
|
||||
\begin{array}{@{}c}
|
||||
\exptype{C}{\ol{X}} \to \ol{T} \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad
|
||||
\triangle' = \overline{\type{Y} : \bot .. \type{P}} \quad \quad
|
||||
\triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \\
|
||||
\text{dom}(\triangle) = \ol{X} \quad \quad
|
||||
%\texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \ \{ \ldots \} \\
|
||||
\mathtt{\Pi} | \triangle, \triangle', \overline{\triangle} | \ol{x : T}, \texttt{this} : \exptype{C}{\ol{X}} \vdash \texttt{e} : \type{S} \mid \overline{\Delta} \quad \quad
|
||||
\triangle \vdash \type{S} <: \type{T}
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \text{ in C with } \generics{\ol{Y \triangleleft P}}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em]
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Method}\\
|
||||
\begin{array}{@{}c}
|
||||
\exptype{C}{\ol{X}} \to \ol{T} \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad
|
||||
(\type{T'},\ol{T}) \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad
|
||||
\triangle' = \overline{\type{Y} : \bot .. \type{P}} \quad \quad
|
||||
\triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \\
|
||||
\text{dom}(\triangle) = \ol{X} \quad \quad
|
||||
@ -363,9 +288,10 @@ $\begin{array}{l}
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Class}\\
|
||||
\begin{array}{@{}c}
|
||||
\mathtt{\Pi}' = \mathtt{\Pi} \cup \set{ \exptype{C}{\ol{X}}.\texttt{m} : \ol{T}_\texttt{m} \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M}} \\
|
||||
\mathtt{\Pi}'' = \mathtt{\Pi} \cup \set{ \exptype{C}{\ol{X}}.\texttt{m} :
|
||||
\generics{\ol{X \triangleleft \type{N}}, \ol{Y \triangleleft P}}\ol{T}_\texttt{m} \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M} } \\
|
||||
\mathtt{\Pi}' = \mathtt{\Pi} \cup \set{ \texttt{m} : (\type{T'_m}, \ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M}} \quad \quad
|
||||
\forall \texttt{m} \in \ol{M}: \Delta \vdash \exptype{C}{\ol{X}} <: \type{T'_m}\\
|
||||
\mathtt{\Pi}'' = \mathtt{\Pi} \cup \set{ \texttt{m} :
|
||||
\generics{\ol{X \triangleleft \type{N}}, \ol{Y \triangleleft P}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M} } \\
|
||||
\triangle = \overline{\type{X} : \bot .. \type{U}} \quad \quad
|
||||
\triangle \vdash \ol{U}, \ol{T}, \type{N} \ \ok \quad \quad
|
||||
\mathtt{\Pi}' | \triangle \vdash \ol{M} \ \ok \text{ in C with} \ \generics{\ol{Y \triangleleft P}}
|
||||
|
||||
25
unify.tex
25
unify.tex
@ -1,3 +1,28 @@
|
||||
% TODO: unify changes
|
||||
% a? <. T can be deleted in the last step
|
||||
% delete wildcard tphs a? when needed
|
||||
% aswell ass free variables:
|
||||
% a <. T with fv(T) not empty and not in \Delta' must be removed by U = L
|
||||
% also in T <. T constraints no free variables are allowed on both sides
|
||||
% the algorithm only removes wildcards, never adds them
|
||||
|
||||
% lessdotCC constraint cannot be removed. we do not know what to capture
|
||||
% example <X> add(List<X> l, X v)
|
||||
% here we need to generate constraints p1 <c List<x>, p2 <c x
|
||||
% because x can become List<a?>:
|
||||
|
||||
% class Box<X>{}
|
||||
|
||||
% class Test{
|
||||
|
||||
% static <X> Box<X> add(Box<X> b, X x){return null;}
|
||||
% static <X> Box<X> empty(){return null;}
|
||||
% static <X> Box<Box<X>> empty2(){return null;}
|
||||
% public static void main(String args[]){
|
||||
% Box<?> b = null;
|
||||
% Box<? extends Box<?>> b2 = add(empty2(), b);
|
||||
% }
|
||||
% }
|
||||
|
||||
\section{Unify}\label{sec:unify}
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user