121 lines
5.2 KiB
TeX
121 lines
5.2 KiB
TeX
|
|
%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. |