stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Cleanup Introduction. Fix method environment in Type Rules

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-02-07 18:26:41 +01:00
parent 26678767c2
commit 10fcfcfea0
4 changed files with 88 additions and 172 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

109
constraints.tex
View File

@ -9,7 +9,21 @@
%\subsection{Well-Formedness}
The \fjtype{} algorithm assumes capture conversions for every method parameter.
There are two different types of constraints:
\begin{description}
\item[$\lessdot$] \textit{Example:}
$\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}$
\noindent
Those two constraints imply that we have to find a type replacement for type variable $\tv{a}$,
which is a supertype of $\exptype{List}{String}$ aswell as $\exptype{List}{Integer}$.
This paper describes a \unify{} algorithm to solve these constraints and calculate a type solution $\sigma$.
For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
\item[$\lessdotCC$] TODO
% The \fjtype{} algorithm assumes capture conversions for every method parameter.
\end{description}
%Why do we need a constraint generation step?
%% The problem is NP-Hard
@ -100,9 +114,6 @@ The \fjtype{} algorithm assumes capture conversions for every method parameter.
% <X, Y> Y m(Example<X> this, Example<Y> p){ ... }
% \end{verbatim}
The constraint generation step is the same as the one for regular Generic Featherweight Java.
Wildcard types are not used during the constraint generation step and have no influence on it.
\begin{displaymath}
\begin{array}{@{}l@{}l}
\typeExpr{} &({\mtypeEnvironment} , \texttt{e}.\texttt{f}, \tv{a}) = \\
@ -130,36 +141,6 @@ 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.
%Soundness: TODO
\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}
\{ \tv{r} \lessdot \exptype{C}{\ol{\wtv{a}}},
\overline{\tv{r}} \lessdot \ol{T},
\type{T} \lessdot \tv{a},
\overline{\wtv{a}} \lessdot \ol{N} \}
\end{array}\\
& \ |\
(\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \overline{\type{T}} \to \type{T}) \in
{\mtypeEnvironment}
, \, \overline{\wtv{a}} \text{ fresh} }
\end{array}\\
\mathbf{in} & \consSet_R \cup \overline{\consSet} \cup \constraint
\end{array}
\end{array}
\end{displaymath}
\begin{displaymath}
\begin{array}{@{}l@{}l}
\typeExpr{} & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a} ) = \\
@ -333,38 +314,38 @@ $\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as
% These constraints should fail!
\section{Result Generation}
If \unify{} returns atleast one type solution $(\Delta, \sigma)$
the last step of the type inference algorithm is to generate a typed class.
% \section{Result Generation}
% If \unify{} returns atleast one type solution $(\Delta, \sigma)$
% the last step of the type inference algorithm is to generate a typed class.
This section presents our type inference algorithm.
The algorithm is given method assumptions $\mv\Pi$ and applied to a
single class $\mv L$ at a time:
\begin{gather*}
\fjtypeinference(\mtypeEnvironment, \texttt{class}\ \exptype{C}{\ol{X}
\triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \\
\quad \quad \begin{array}[t]{rll}
\textbf{let}\
(\overline{\methodAssumption}, \consSet) &= \fjtype{}(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
\triangleleft \ol{N}} \triangleleft \type{N}\ \{ \ldots \}) &
\text{// constraint generation}\\
{(\Delta, \sigma)} &= \unify{}(\consSet,\, \ol{X} <: \ol{N}) & \text{// constraint solving}\\
\generics{\ol{Y} \triangleleft \ol{S}} &= \set{ \type{Y} \triangleleft \type{S} \mid \wildcard{Y}{\type{P}}{\bot} \in \Delta} \\
\ol{M'} &= \set{ \generics{\ol{Y} \triangleleft \ol{S}}\ \sigma(\tv{a}) \ \texttt{m}(\ol{\sigma(\tv{a})\ x}) = \texttt{e} \mid (\mathtt{m}(\ol{x})\ = \mv e) \in \ol{M}, (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
%TODO: Describe whole algorithm (Insert types, try out every unify solution by backtracking (describe it as Non Deterministic algorithm))
\end{array}\\
\textbf{in}\ \texttt{class}\ \exptype{C}{\ol{X}
\triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M'} \} \\
\textbf{in}\ \mtypeEnvironment \cup
\set{(\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \generics{\ol{Y} \triangleleft \ol{S}}\ \ol{\sigma(\tv{a})} \to \sigma(\tv{a})) \ |\ (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
% \fjtypeInsert(\overline{\methodAssumption}, (\sigma, \unifyGenerics{}) )
\end{gather*}
% This section presents our type inference algorithm.
% The algorithm is given method assumptions $\mv\Pi$ and applied to a
% single class $\mv L$ at a time:
% \begin{gather*}
% \fjtypeinference(\mtypeEnvironment, \texttt{class}\ \exptype{C}{\ol{X}
% \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \\
% \quad \quad \begin{array}[t]{rll}
% \textbf{let}\
% (\overline{\methodAssumption}, \consSet) &= \fjtype{}(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
% \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \ldots \}) &
% \text{// constraint generation}\\
% {(\Delta, \sigma)} &= \unify{}(\consSet,\, \ol{X} <: \ol{N}) & \text{// constraint solving}\\
% \generics{\ol{Y} \triangleleft \ol{S}} &= \set{ \type{Y} \triangleleft \type{S} \mid \wildcard{Y}{\type{P}}{\bot} \in \Delta} \\
% \ol{M'} &= \set{ \generics{\ol{Y} \triangleleft \ol{S}}\ \sigma(\tv{a}) \ \texttt{m}(\ol{\sigma(\tv{a})\ x}) = \texttt{e} \mid (\mathtt{m}(\ol{x})\ = \mv e) \in \ol{M}, (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
% %TODO: Describe whole algorithm (Insert types, try out every unify solution by backtracking (describe it as Non Deterministic algorithm))
% \end{array}\\
% \textbf{in}\ \texttt{class}\ \exptype{C}{\ol{X}
% \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M'} \} \\
% \textbf{in}\ \mtypeEnvironment \cup
% \set{(\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \generics{\ol{Y} \triangleleft \ol{S}}\ \ol{\sigma(\tv{a})} \to \sigma(\tv{a})) \ |\ (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
% % \fjtypeInsert(\overline{\methodAssumption}, (\sigma, \unifyGenerics{}) )
% \end{gather*}
The overall algorithm is nondeterministic. The function $\unify{}$ may
return finitely many times as there may be multiple solutions for a constraint
set. A local solution for class $\mv C$ may not
be compatible with the constraints generated for a subsequent class. In this case, we have to backtrack to $\mv C$ and proceed to the next
local solution; if thats fail we have to backtrack further to an earlier class.
% The overall algorithm is nondeterministic. The function $\unify{}$ may
% return finitely many times as there may be multiple solutions for a constraint
% set. A local solution for class $\mv C$ may not
% be compatible with the constraints generated for a subsequent class. In this case, we have to backtrack to $\mv C$ and proceed to the next
% local solution; if thats fail we have to backtrack further to an earlier class.
% \begin{gather*}
% \textbf{ApplyTypes}(\mtypeEnvironment, \texttt{class}\ \exptype{C}{\ol{X}

129
introduction.tex
View File

@ -7,32 +7,15 @@ or allowing to write typeless Java code which is then type infered and thereby t
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}.
This paper extends a type inference algorithm for Featherweight Java (\cite{TIforFGJ}) by adding wildcards.
The last step to create a type inference algorithm compatible to the Java type system.
The algorithm is a modified version of the \unify{} algorithm presented in \cite{plue09_1}.
The algorithm is a slightly improved version of the one in \cite{TIforFGJ} and added wildcard support.
Wildcards are existential types which have to be \textit{unpacked} before they can be used.
In Java this is done implicitly by a process called capture conversion \cite{JavaLanguageSpecification}.
The type system in \cite{WildcardsNeedWitnessProtection} makes this process explicit by using \texttt{let} statements.
Our type inference algorithm will accept an input program without let statements and add them where necessary.
%This paper extends a type inference algorithm for Featherweight Java \cite{TIforFGJ} by adding wildcards.
%The last step to create a type inference algorithm compatible to the Java type system.
The algorithm presented in this paper is a slightly improved version of the one in \cite{TIforFGJ} including wildcard support.
%a modified version of the \unify{} algorithm presented in \cite{plue09_1}.
The input to the type inference algorithm is a Featherweight Java program (example in figure \ref{fig:nested-list-example-typeless}) conforming to the syntax shown in figure \ref{fig:syntax}.
Type inference adds \texttt{let} statements in a fashion similar to the Java capture conversion \cite{WildFJ}.
We wrap every parameter of a method invocation in \texttt{let} statement unknowing if a capture conversion is necessary (see figure \ref{fig:nested-list-example-let}).
The \fjtype{} algorithm calculates constraints based on this intermediate representation,
which are then solved by the \unify{} algorithm
resulting in a correctly typed program (see figure \ref{fig:nested-list-example-typed}).
We figured the \texttt{let} statements to be obsolete for our use case.
Once the type inference algorithm found a correct type solution they can be inferred by the given type annotations.
% 1. Constraint generation
% 2. Insert typing
% # Showing soundness
% Every program in our calculus can be converted to a WildcardsNeedWitnessProtection program
\begin{figure}[tp]
\begin{subfigure}[t]{\linewidth}
\begin{lstlisting}[style=fgj]
@ -52,45 +35,31 @@ class Example {
\label{fig:nested-list-example-typeless}
\end{subfigure}
~
\begin{subfigure}[t]{\linewidth}
\begin{lstlisting}[style=tfgj]
class List<A> {
List<A> add(A v) { ... }
}
% \begin{subfigure}[t]{\linewidth}
% \begin{lstlisting}[style=tfgj]
% class List<A> {
% List<A> add(A v) { ... }
% }
class Example {
m(l, la, lb){
return let r2 : (*@$\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$@*) = {
let r1 : (*@$\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$@*) = l in {
let p1 : (*@$\exptype{List}{\type{Integer}}$@*) = {
let xa = la in xa.add(1)
} in x1.add(p1)
} in {
let p2 = {
let xb = lb in xb.add("str")
} in x2.add(p2)
};
}
}
\end{lstlisting}
\begin{lstlisting}[style=tfgj]
class List<A> {
List<A> add(A v) { ... }
}
class Example {
m((*@$\exptype{List}{\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}}$@*) l, List<Integer> la, List<String> lb){
return l
.add(la.add(1))
.add(lb.add("str"));
}
}
\end{lstlisting}
\caption{Featherweight Java Representation}
\label{fig:nested-list-example-let}
\end{subfigure}
~
% class Example {
% m(l, la, lb){
% return let r2 : (*@$\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$@*) = {
% let r1 : (*@$\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$@*) = l in {
% let p1 : (*@$\exptype{List}{\type{Integer}}$@*) = {
% let xa = la in xa.add(1)
% } in x1.add(p1)
% } in {
% let p2 = {
% let xb = lb in xb.add("str")
% } in x2.add(p2)
% };
% }
% }
% \end{lstlisting}
% \caption{Featherweight Java Representation}
% \label{fig:nested-list-example-let}
% \end{subfigure}
% ~
\begin{subfigure}[t]{\linewidth}
\begin{lstlisting}[style=tfgj]
class List<A> {
@ -149,35 +118,6 @@ List<?> genList() {
%\label{fig:intro-example-code}
\end{figure}
Existential types have to be \textit{unpacked} before they can be used \cite{WildcardsNeedWitnessProtection}.
In Java this is done implicitly.
%Our type inference algorithm has to add let statements surrounding method invocations.
\begin{figure}[tp]
\begin{constraintset}
\begin{subfigure}[t]{\linewidth}
\begin{lstlisting}[style=fgj]
List<? super Integer> ls = ...;
ls.add(new Integer());
\end{lstlisting}
\caption{Method invocation}
\label{fig:intro-example-typeless}
\end{subfigure}
\end{constraintset}
\begin{constraintset}
\begin{subfigure}[t]{\linewidth}
\begin{lstlisting}[style=tfgj]
List<? super Integer> ls = ...;
let x : (*@ $\wctype{\wildcard{X}{\texttt{Object}}{\texttt{Integer}}}{List}{\rwildcard{X}}$ @*) = ls in x.add(new Integer());
\end{lstlisting}
\caption{Capture Conversion by \texttt{let}-statement}
\label{fig:intro-example-typed}
\end{subfigure}
\end{constraintset}
\end{figure}
% \subsection{Wildcards}
% Java subtyping involving generics is invariant.
% For example \texttt{List<String>} is not a subtype of \texttt{List<Object>}.
@ -201,19 +141,6 @@ In this case the name is $\rwildcard{X}$ and it's bound to the the type \texttt{
% 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{Constraints}
Constraints consist of normal types and type variables:
$\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}$
\noindent
Those two constraints imply that we have to find a type replacement for type variable $\tv{a}$,
which is a supertype of $\exptype{List}{String}$ aswell as $\exptype{List}{Integer}$.
This paper describes a \unify{} algorithm to solve these constraints and calculate a type solution $\sigma$.
For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
\subsection{Challenges}\label{challenges}
The introduction of wildcards adds additional challenges.

8
soundness.tex
View File

@ -423,6 +423,14 @@ Same as Subst
\subsection{Converting to Wild FJ}
Wildcards are existential types which have to be \textit{unpacked} before they can be used.
In Java this is done implicitly by a process called capture conversion \cite{JavaLanguageSpecification}.
The type system in \cite{WildcardsNeedWitnessProtection} makes this process explicit by using \texttt{let} statements.
Our type inference algorithm will accept an input program without let statements and add them where necessary.
%Type inference adds \texttt{let} statements in a fashion similar to the Java capture conversion \cite{WildFJ}.
%We wrap every parameter of a method invocation in \texttt{let} statement unknowing if a capture conversion is necessary.
Figure \ref{fig:tletexpr} shows type rules for fields and method calls.
They have been merged with let statements and simplified.

14
tRules.tex
View File

@ -246,28 +246,28 @@ $\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
%\text{dom}(\triangle) = \ol{X} \quad \quad
\triangle' = \overline{\type{Y} : \bot .. \type{P}} \quad \quad
\triangle, \triangle' \vdash \ol{U}, \type{T}, \ol{T} \ \ok \\
\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' | \ol{x : T}, \texttt{this} : \exptype{C}{\ol{X}} \vdash \texttt{e} : \type{S} \quad \quad
\triangle \vdash \type{S} <: \type{T}
\\
\hline
\vspace*{-0.3cm}\\
\triangle \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \text{ in C with } \generics{\ol{Y \triangleleft P}}
\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-Class}\\
\begin{array}{@{}c}
\mathtt{\Pi}' = \mathtt{\Pi} \cup \set{ \texttt{m} \mapsto (\exptype{C}{\ol{X}} \to \ol{T}_\texttt{m} \to \type{T}_\texttt{m}) \mid \texttt{m} \in \ol{M}} \\
\mathtt{\Pi}'' = \mathtt{\Pi} \cup \set{ \texttt{m} \mapsto
\generics{\ol{X \triangleleft \type{N}}, \ol{Y \triangleleft P}}(\exptype{C}{\ol{X}} \to \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} : \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} } \\
\triangle = \overline{\type{X} : \bot .. \type{U}} \quad \quad
\triangle \vdash \ol{U}, \ol{T}, \type{N} \ \ok \quad \quad
\triangle \vdash \ol{M} \ \ok \text{ in C with} \ \generics{\ol{Y \triangleleft P}}
\mathtt{\Pi}' | \triangle \vdash \ol{M} \ \ok \text{ in C with} \ \generics{\ol{Y \triangleleft P}}
\\
\hline
\vspace*{-0.3cm}\\