Ecoop2024_TIforWildFJ/letfjTransformation.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.