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

Cleanup and Restructure. Remove polymorphic recursion exclusion from Type Rules

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-05-13 23:58:42 +02:00
parent 5f33fa4711
commit 77f3fbedfa
6 changed files with 369 additions and 631 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

114
conclusion.tex
View File

@ -1,3 +1,117 @@
\section{Properties of the Algorithm}
\section{Soundness}\label{sec:soundness}
\section{Completeness}\label{sec:completeness}
The algorithm can find a solution to every program which the Unify by Plümicke finds
a correct solution aswell.
It will not infer intermediat type like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X},\rwildcard{X}}$.
There is propably some loss of completeness when capture constraints get deleted.
This happens because constraints of the form $\tv{a} \lessdotCC \exptype{C}{\wtv{x}}$ are kept as long as possible.
Here the variable $\tv{a}$ maybe could hold a wildcard type,
but it gets resolved to a $\generics{\type{A} \triangleleft \type{N}}$.
This combined with a constraint $\type{N} \lessdot \wtv{x}$ looses a possible solution.
This is our result:
\begin{verbatim}
class List<X> {
<Y extends X> void addTo(List<Y> l){
l.add(this.get());
}
}
\end{verbatim}
$
\tv{l} \lessdotCC \exptype{List}{\wtv{y}},
\type{X} \lessdot \wtv{y}
$
But the most general type would be:
\begin{verbatim}
class List<X> {
void addTo(List<? super X> l){
l.add(this.get());
}
}
\end{verbatim}
\subsection{Discussion Pair Example}
\begin{verbatim}
<X> Pair<X,X> make(List<X> l){ ... }
<X> boolean compare(Pair<X,X> p) { ... }
List<?> l;
Pair<?,?> p;
compare(make(l)); // Valid
compare(p); // Error
\end{verbatim}
Our type inference algorithm is not able to solve this example.
When we convert this to \TamedFJ{} and generate constraints we end up with:
\begin{lstlisting}[style=tamedfj]
let m = let x = l in make(x) in compare(m)
\end{lstlisting}
\begin{constraintset}$
\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \ntv{x},
\ntv{x} \lessdotCC \exptype{List}{\wtv{a}}
\exptype{Pair}{\wtv{a}, \wtv{a}} \lessdot \ntv{m}, %% TODO: Mark this constraint
\ntv{m} \lessdotCC \exptype{Pair}{\wtv{b}, \wtv{b}}
$\end{constraintset}
$\ntv{x}$ will get the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and
from the constraint
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
\unify{} deducts $\wtv{a} \doteq \rwildcard{X}$ leading to
$\exptype{Pair}{\rwildcard{X}, \rwildcard{X}} \lessdot \ntv{m}$.
Finding a supertype to $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ is the crucial part.
The correct substition for $\ntv{m}$ would be $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$.
But this leads to additional branching inside the \unify{} algorithm and increases runtime.
%We refrain from using that type, because it is not denotable with Java syntax.
%Types used for normal type placeholders should be expressable Java types. % They are not!
The prefered way of dealing with this example in our opinion would be the addition of a multi-let statement to the syntax.
\begin{lstlisting}[style=letfj]
let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l, m = make(x) in compare(make(x))
\end{lstlisting}
We can make it work with a special rule in the \unify{}.
But this will only help in this specific example and not generally solve the issue.
A type $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ has atleast two immediate supertypes:
$\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ and
$\wctype{\rwildcard{X}, \rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$.
Imagine a type $\exptype{Triple}{\rwildcard{X},\rwildcard{X},\rwildcard{X}}$ already has
% TODO: how many supertypes are there?
%X.Triple<X,X,X> <: X,Y.Triple<X,Y,X> <:
%X,Y,Z.Triple<X,Y,Z>
% TODO example:
\begin{lstlisting}[style=java]
<X> Triple<X,X,X> sameL(List<X> l)
<X,Y> Triple<X,Y,Y> sameP(Pair<X,Y> l)
<X,Y> void triple(Triple<X,Y,Y> tr){}
Pair<?,?> p ...
List<?> l ...
make(t) { return t; }
triple(make(sameP(p)));
triple(make(sameL(l)));
\end{lstlisting}
\begin{constraintset}
$
\exptype{Triple}{\rwildcard{X}, \rwildcard{X}, \rwildcard{X}} \lessdot \ntv{t},
\ntv{t} \lessdotCC \exptype{Triple}{\wtv{a}, \wtv{b}, \wtv{b}}, \\
(\textit{This constraint is added later: } \exptype{Triple}{\rwildcard{X}, \rwildcard{Y}, \rwildcard{Y}} \lessdot \ntv{t})
$
% Triple<X,X,X> <. t
% ( Triple<X,Y,Y> <. t ) <- this constraint is added later
% t <. Triple<a?, b?, b?>
% t =. x.Triple<X,X,X>
\end{constraintset}
\section{Conclusion and Further Work} \section{Conclusion and Further Work}
% we solved the problems given in the introduction (see examples TODO give names to examples) % we solved the problems given in the introduction (see examples TODO give names to examples)
The problems introduced in the openening \ref{challenges} can be solved via our \unify{} algorithm (see examples \ref{example1} and \ref{example2}). The problems introduced in the openening \ref{challenges} can be solved via our \unify{} algorithm (see examples \ref{example1} and \ref{example2}).

101
constraints.tex
View File

@ -13,23 +13,104 @@
% But it can be easily adapted to Featherweight Java or Java. % But it can be easily adapted to Featherweight Java or Java.
% We add T <. a for every return of an expression anyway. If anything returns a Generic like X it is not directly used in a method call like X <c T % We add T <. a for every return of an expression anyway. If anything returns a Generic like X it is not directly used in a method call like X <c T
The constraint generation works on the \TamedFJ{} language. \begin{description}
This step is mostly same as in \cite{TIforFGJ} except for field access and method invocation. \item[input] \TamedFJ{} program in A-Normal form
We will focus on those parts. \item[output] Constraints
Here the new capture constraints and wildcard type placeholders are introduced. \end{description}
Generally subtype constraints for an expression mirror the subtype relations in the premise of the respective type rule introduced in section \ref{sec:tifj} The constraint generation works on the \TamedFJ{} language.
Unknown types at the time of the constraint generation step are replaced with type placeholders. This step is mostly the same as in \cite{TIforFGJ} except for field access and method invocation.
\begin{verbatim} We will focus on those two parts where also the new capture constraints and wildcard type placeholders are introduced.
%In \TamedFJ{} capture conversion is implicit.
%To emulate Java's behaviour we assume the input program not to contain any let statements.
%They will be added by an ANF transformation (see chapter \ref{sec:anfTransformation}).
Before generating constraints the input is transformed by an ANF transformation (see section \ref{sec:anfTransformation}).
Capture conversion is only needed for wildcard types,
but we don't know which expressions will spawn wildcard types because there are no type annotations yet.
We preemptively enclose every expression in a let statement before using it as a method argument.
%Constraints are generated on the basis of the program in A-Normal form.
%After adding the missing type annotations the resulting program is valid under the typing rules in \cite{WildFJ}.
%This is shown in chapter \ref{sec:soundness}
%\section{\TamedFJ{}: Syntax and Typing}\label{sec:tifj}
% The syntax forces every expression to undergo a capture conversion before it can be used as a method argument.
% Even variables have to be catched by a let statement first.
% This behaviour emulates Java's implicit capture conversion.
\subsection{ANF transformation}\label{sec:anfTransformation}
\newcommand{\anf}[1]{\ensuremath{\tau}(#1)}
%https://en.wikipedia.org/wiki/A-normal_form)
Featherweight Java's syntax involves no \texttt{let} statement
and terms can be nested freely similar to Java's syntax.
Our calculus \TamedFJ{} uses let statements to explicitly apply capture conversion to wildcard types,
but we don't know which expressions will spawn wildcard types because there are no type annotations yet.
To emulate Java's behaviour we have to preemptively add capture conversion in every suitable place.
%To convert it to \TamedFJ{} additional let statements have to be added.
This is done by a \textit{A-Normal Form} \cite{aNormalForm} transformation shown in figure \ref{fig:anfTransformation}.
After this transformation every method invocation is preceded by let statements which perform capture conversion on every argument before passing them to the method.
See the example in listings \ref{lst:anfinput} and \ref{lst:anfoutput}.
\begin{figure}
\begin{minipage}{0.45\textwidth}
\begin{lstlisting}[style=fgj,caption=\TamedFJ{} example,label=lst:anfinput]
m(l, v){ m(l, v){
let x = x in x.add(v) return l.add(v);
} }
\end{verbatim} \end{lstlisting}
\end{minipage}%
\hfill
\begin{minipage}{0.5\textwidth}
\begin{lstlisting}[style=tfgj,caption=converted to A-Normal form,label=lst:anfoutput]
m(l, v) =
let x1 = l in
let x2 = v in x1.add(x2)
\end{lstlisting}
\end{minipage}
\end{figure}
\begin{figure}
\begin{center}
$\begin{array}{lrcl}
%\text{ANF}
& \anf{\expr{x}} & = & \expr{x} \\
& \anf{\texttt{new} \ \type{C}(\overline{t})} & = & \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}}) \\
& \anf{t.f} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \expr{x}.f \\
& \anf{t.\texttt{m}(\overline{t})} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
& \anf{t_1 \elvis{} t_2} & = & \anf{t_1} \elvis{} \anf{t_2} \\
& \anf{\texttt{let}\ x = \expr{t}_1 \ \texttt{in}\ \expr{t}_2} & = & \texttt{let}\ x = \anf{\expr{t}_1} \ \texttt{in}\ \anf{\expr{t}_2}
\end{array}$
\end{center}
\caption{ANF Transformation}\label{fig:anfTransformation}
\end{figure}
\begin{figure}
$
\begin{array}{lrcl}
%\hline
\text{Terms} & t & ::= & \expr{x} \\
& & \ \ | & \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}_c}) \\
& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \expr{x}_c.f \\
& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \expr{x}_c.\texttt{m}(\overline{\expr{x}_c}) \\
& & \ \ | & t \elvis{} t \\
%\hline
\end{array}
$
\caption{A-Normal form}\label{fig:anf-syntax}
\end{figure}
\subsection{Constraint Generation Algorithm}
Generally subtype constraints for an expression mirror the subtype relations in the premise of the respective type rule introduced in section \ref{sec:tifj}.
Unknown types at the time of the constraint generation step are replaced with type placeholders.
The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call. 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. Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
The parameter types given to a generic method also affect their return type. The parameter types given to a generic method also affect their return type.
During constraint generation the algorithm does not know the parameter types yet. During constraint generation the algorithm does not know the parameter types yet.
We generate $\lessdotCC$ constraints and let \unify{} do the capture conversion. We generate $\lessdotCC$ constraints and let \unify{} do the capture conversion.

440
introduction.tex
View File

@ -10,8 +10,44 @@
% Capture Conversion % Capture Conversion
% Explain difference between local and global type inference % Explain difference between local and global type inference
\section{Global Type Inference} \section{Type Inference for Java}
Java already provides type inference in a restricted form namely local type inference. %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),
or allowing to write typeless Java code which is then type inferred 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 listing \ref{lst:intro-example-typeless}.
%In this case our algorithm would also be able to propose a solution including wildcards as shown in listing \ref{lst: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.
\subsection{Comparision to similar Type Inference Algorithms}
To outline the contributions in this paper we will list the advantages and improvements to smiliar type inference algorithms:
\begin{description}
\item[Global Type Inference for Featherweight Java] \cite{TIforFGJ} is a predecessor to our algorithm.
The algorithm presented in this paper is a improved version
with the biggest change being the added wildcard support.
% Proven sound on type rules of Featherweight Java, which are also proven to produce sound programs
% implication rules that follow the subtyping rules directly. Easy to understand soundness proof
% capture conversion is needed
\textit{Example:} The type inference algorithm for Generic Featherweight Java produces \texttt{Object} as the return type of the
\texttt{genBox} method in listing \ref{lst:intro-example-typeless}
whereas our type inference algorithm will infer the type solution shown in listing \ref{lst:intro-example-typed}.
\item[Type Unification for Java with Wildcards]
An existing unification algorithm for Java with wildcards \cite{plue09_1} states the same capabilities,
but exposes some errors when it comes to method invocations.
Especially the problems shown in chapter \ref{challenges} are handled incorrectly.
Whereas our type inference algorithm is based on a Featherweight Java calculus \cite{WildFJ} and it's proven sound subtyping rules.
%But they are all correctly solved by our new type inference algorithm presented in this paper.
The central piece of this type inference algorithm, the \unify{} process, is described with implication rules (chapter \ref{sec:unify}).
We try to keep the branching at a minimal amount to improve runtime behavior.
Also the transformation steps of the \unify{} algorithm are directly related to the subtyping rules of our calculus.
\item[Java Type Inference]
Java already provides type inference in a restricted form % namely {Local Type Inference}.
which only works for local environments where the surrounding context has knwon types.
But our global type inference algorithm is able to work on input programs which do not hold any type annotations at all. But our global type inference algorithm is able to work on input programs which do not hold any type annotations at all.
We will show the different capabilities with an example. We will show the different capabilities with an example.
In listing \ref{lst:tiExample} the method call \texttt{emptyList} is missing In listing \ref{lst:tiExample} the method call \texttt{emptyList} is missing
@ -46,114 +82,19 @@ The type inference algorithm presented in this paper will correctly replace the
method with \texttt{List<List<String>>} and proof this code snippet correct. method with \texttt{List<List<String>>} and proof this code snippet correct.
The local type inference algorithm based on matching cannot produce this solution. The local type inference algorithm based on matching cannot produce this solution.
Here our type inference algorithm based on unification is needed. Here our type inference algorithm based on unification is needed.
% \begin{verbatim}
% this.<List<String>>emptyList().add(new List<String>())
% .get(0)
% .get(0);
% \end{verbatim}
\end{description}
% %motivate constraints:
% To solve this example our Type Inference algorithm will create constraints
% $ % $
% \begin{array}[b]{c} % \exptype{List}{\tv{a}} \lessdot \tv{b},
% \begin{array}[b]{c} % \tv{b} \lessdot \exptype{List}{\tv{c}},
% \texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}} % \tv{c} \lessdot \exptype{List}{\tv{d}}
% \\
% \hline
% \texttt{emptyList().get()} : \exptype{List}{\type{String}}
% \end{array} \rulenameAfter{T-Call}
% \quad \generics{\type{X}}\exptype{List}{\type{X}} \to \type{X} \in \mtypeEnvironment{}(\texttt{get})1
% \\
% \hline
% \texttt{emptyList().get().get()} : \type{String}
% \end{array} \rulenameAfter{T-Call}
% $ % $
%motivate constraints:
To solve this example our Type Inference algorithm will create constraints
$
\exptype{List}{\tv{a}} \lessdot \tv{b},
\tv{b} \lessdot \exptype{List}{\tv{c}},
\tv{c} \lessdot \exptype{List}{\tv{d}}
$
% Local type inference cannot deal with type inference during the algorithm.
% If the left side contains unknown type parameters.
% \begin{verbatim} \subsection{Conclusion}
% import java.util.ArrayList;
% import java.util.stream.*;
% class Test {
% void test(){
% var s = new ArrayList<String>().stream().map(i -> 1);
% receive(s);
% }
% void receive(Stream<Object> l){}
% }
% \end{verbatim}
% TypeError:
% \begin{verbatim}
% void test(){
% var l = new ArrayList<String>();
% l.add("hi");
% var s = l.stream().map(i -> 1).collect(Collectors.toList());
% var s2 = l.stream().map(i -> "String").collect(Collectors.toList());
% receive(s, s2);
% }
% <A> void receive(List<A> l, List<A> l2){}
% \end{verbatim}
% Correct:
% \begin{verbatim}
% void test(){
% var l = new ArrayList<String>();
% l.add("hi");
% List<Object> s = l.stream().map(i -> 1).collect(Collectors.toList());
% List<Object> s2 = l.stream().map(i -> "String").collect(Collectors.toList());
% receive(s, s2);
% }
% <A> void receive(List<A> l, List<A> l2){}
% \end{verbatim}
% Error:
% \begin{verbatim}
% rrr(this.emptyBox().set(this.<Integer>emptyBox()).set(this.<String>emptyBox()));
% \end{verbatim}
% Correct:
% \begin{verbatim}
% rrr(this.<Box<?>>emptyBox().set(this.<Integer>emptyBox()).set(this.<String>emptyBox()));
% \end{verbatim}
% \begin{recap}{Java Local Type Inference}
% Local type inference is able to solve constraints of the form
% T <. b, b <. T where T are given types
% \end{recap}
% Local Type inference cannot infer F-Bounded types (TODO: we can, right?)
\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),
or allowing to write typeless Java code which is then type inferred 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 listing \ref{lst: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 presented in this paper is a improved version of the one in \cite{TIforFGJ} including wildcard support.
% Proven sound on type rules of Featherweight Java, which are also proven to produce sound programs
% implication rules that follow the subtyping rules directly. Easy to understand soundness proof
% capture conversion is needed
The type inference algorithm for Generic Featherweight Java \cite{TIforFGJ} produces \texttt{Object} as the return type of the
\texttt{genBox} method in listing \ref{lst:intro-example-typeless}
whereas our type inference algorithm will infer the type solution shown in listing \ref{lst:intro-example-typed}.
An existing unification algorithm for Java with wildcards \cite{plue09_1} states the same capabilities,
but exposes some when it comes to method invocations.
Especially the problems shown in chapter \ref{challenges} are handled incorrectly.
Whereas our type inference algorithm is based on a Featherweight Java calculus \cite{WildFJ} and it's proven sound subtyping rules.
%But they are all correctly solved by our new type inference algorithm presented in this paper.
\begin{itemize} \begin{itemize}
\item \item
We introduce the language \tifj{} (chapter \ref{sec:tifj}). We introduce the language \tifj{} (chapter \ref{sec:tifj}).
@ -201,7 +142,7 @@ genBox() {
\end{minipage}% \end{minipage}%
\hfill \hfill
\begin{minipage}{0.55\textwidth} \begin{minipage}{0.55\textwidth}
\begin{lstlisting}[style=tfgj,caption=Correct type,label=lst:intro-example-typed] \begin{lstlisting}[style=tfgj,caption=Type inference solution,label=lst:intro-example-typed]
Box<?> genBox() { Box<?> genBox() {
if( ... ) { if( ... ) {
return new Box<Integer>(1); return new Box<Integer>(1);
@ -221,7 +162,7 @@ Box<?> genBox() {
% \texttt{List<Object>} is not a valid return type for the method \texttt{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<?>}). % The type inference algorithm has to find the correct type involving wildcards (\texttt{List<?>}).
\subsection{Java Wildcards} \section{Java Wildcards}
Java has invariant subtyping for polymorphic types. Java has invariant subtyping for polymorphic types.
%but it incooperates use-site variance via so called wildcard types. %but it incooperates use-site variance via so called wildcard types.
@ -271,7 +212,7 @@ but there exists some unknown type $\exptype{List}{\rwildcard{A}}$, with $\rwild
Inside the body of the let statement \expr{v} is treated as a value with the constant type $\exptype{List}{\rwildcard{A}}$. Inside the body of the let statement \expr{v} is treated as a value with the constant type $\exptype{List}{\rwildcard{A}}$.
Existential types enable us to formalize \textit{Capture Conversion}. Existential types enable us to formalize \textit{Capture Conversion}.
Polymorphic method calls need to be wraped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}. 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. In Java this is done implicitly in a process called capture conversion (as proposed in Wild FJ \cite{WildFJ}).
\begin{figure} \begin{figure}
\begin{minipage}{0.4\textwidth} \begin{minipage}{0.4\textwidth}
@ -293,11 +234,6 @@ lo.add(new Integer(1)); // error!
\end{minipage} \end{minipage}
\end{figure} \end{figure}
\begin{recap}{\textbf{Capture Conversion}}
TODO %Explain Java Capture Conversion
\end{recap}
%show input and a correct letFJ representation %show input and a correct letFJ representation
%TODO: first show local type inference and explain lessdotCC constraints. then show example with global TI %TODO: first show local type inference and explain lessdotCC constraints. then show example with global TI
\begin{figure}[h] \begin{figure}[h]
@ -362,15 +298,17 @@ and \texttt{shuffle} can be invoked with the type parameter $\rwildcard{X}$:
let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in <X>shuffle(l2d') let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in <X>shuffle(l2d')
\end{lstlisting} \end{lstlisting}
\subsection{Global Type Inference} \section{Global Type Inference Algorithm}
\begin{description} % \begin{description}
\item[input] \tifj{} program % \item[input] \tifj{} program
\item[output] type solution % \item[output] type solution
\item[postcondition] the type solution applied to the input must yield a valid \letfj{} program % \item[postcondition] the type solution applied to the input must yield a valid \letfj{} program
\end{description} % \end{description}
The input to our type inference algorithm is a modified version of the \letfj{}\cite{WildcardsNeedWitnessProtection} calculus (see chapter \ref{sec:tifj}). %Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
The input to our type inference algorithm is a modified version of the calculus in \cite{WildcardsNeedWitnessProtection} (see chapter \ref{sec:tifj}).
First \fjtype{} generates constraints First \fjtype{} generates constraints
and afterwards \unify{} computes a solution for the given constraint set. 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})$. Constraints consist out of subtype constraints $(\type{T} \lessdot \type{T})$ and capture constraints $(\type{T} \lessdotCC \type{T})$.
@ -501,71 +439,6 @@ $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype
% List<?> m() = new List<String>() :? new List<Integer>() :? id(m()); % List<?> m() = new List<String>() :? new List<Integer>() :? id(m());
% \end{verbatim} % \end{verbatim}
\subsection{\TamedFJ{}}
%LetFJ -> Output language!
%TamedFJ -> ANF transformed input langauge
%Input language only described here. It is standard Featherweight Java
% we use the transformation to proof soundness. this could also be moved to the end.
% the constraint generation step assumes every method argument to be encapsulated in a let statement. This is the way Java is doing capture conversion
The input to our algorithm is a typeless version of Featherweight Java.
Method parameters and return types are optional.
We still require type annotations for fields and generic class parameters.
This is a design choice by us,
as we consider them as data declarations which are given by the programmer.
% They are inferred in for example \cite{plue14_3b}
Note the \texttt{new} expression not requiring generic parameters,
which are also inferred by our algorithm.
The method call naturally has type inferred generic parameters aswell.
We add the elvis operator ($\elvis{}$) to the syntax mainly to showcase applications involving wildcard types.
The syntax is described in figure \ref{fig:outputSyntax} with optional type annotations highlighted in yellow.
It is possible to exclude all optional types.
% The output is a valid Featherweight Java program.
% We use the syntax of the version introduced in \cite{WildcardsNeedWitnessProtection}
% calling it \letfj{} for that it is a Featherweight Java variant including \texttt{let} statements.
\newcommand{\highlight}[1]{\begingroup\fboxsep=0pt\colorbox{yellow}{$\displaystyle #1$}\endgroup}
\begin{figure}
$
\begin{array}{lrcl}
\hline
\text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
\text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
\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} & ::= & \highlight{\generics{\overline{\type{X} \triangleleft \type{N}}}}\ \highlight{\type{T}}\ \texttt{m}(\overline{\highlight{\type{T}}\ \expr{x}}) \{ \texttt{return} \ \expr{e}; \} \\
\text{Terms} & \expr{e} & ::= & \expr{x} \\
& & \ \ | & \texttt{new} \ \type{C}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
& & \ \ | & \expr{e}.f\\
& & \ \ | & \expr{e}.\texttt{m}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
& & \ \ | & \texttt{let}\ \expr{x} \highlight{: \wcNtype{\Delta}{N}} = \expr{e} \ \texttt{in} \ \expr{e}\\
& & \ \ | & \expr{e} \elvis{} \expr{e}\\
\text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
\hline
\end{array}
$
\caption{Input Syntax with optional type annotations}\label{fig:outputSyntax}
\end{figure}
The output of our type inference algorithm is fully and correctly typed \TamedFJ{} program.
Before generating constraints the input is transformed by an ANF transformation (see section \ref{sec:anfTransformation}).
Constraints are generated on the basis of the program in A-Normal form.
After adding the missing type annotations the resulting program is valid under the typing rules in \cite{WildFJ}.
%This is shown in chapter \ref{sec:soundness}
Capture conversion is only needed for wildcard types,
but we don't know which expressions will spawn wildcard types because there are no type annotations yet.
We preemptively enclose every expression in a let statement before using it as a method argument.
We need the let statements to deal with possible Wildcard types.
The syntax used in our examples is the standard Featherweight Java syntax.
\subsection{Challenges}\label{challenges} \subsection{Challenges}\label{challenges}
%TODO: Wildcard subtyping is infinite see \cite{TamingWildcards} %TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
@ -778,202 +651,3 @@ $\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.
%TODO: Move this part. or move the third challenge some underneath. %TODO: Move this part. or move the third challenge some underneath.
The \unify{} algorithm only sees the constraints with no information about the program they originated from. 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(\wtv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}. 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}.
\section{Discussion Pair Example}
\begin{verbatim}
<X> Pair<X,X> make(List<X> l){ ... }
<X> boolean compare(Pair<X,X> p) { ... }
List<?> l;
Pair<?,?> p;
compare(make(l)); // Valid
compare(p); // Error
\end{verbatim}
Our type inference algorithm is not able to solve this example.
When we convert this to \TamedFJ{} and generate constraints we end up with:
\begin{lstlisting}[style=tamedfj]
let m = let x = l in make(x) in compare(m)
\end{lstlisting}
\begin{constraintset}$
\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \ntv{x},
\ntv{x} \lessdotCC \exptype{List}{\wtv{a}}
\exptype{Pair}{\wtv{a}, \wtv{a}} \lessdot \ntv{m}, %% TODO: Mark this constraint
\ntv{m} \lessdotCC \exptype{Pair}{\wtv{b}, \wtv{b}}
$\end{constraintset}
$\ntv{x}$ will get the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and
from the constraint
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
\unify{} deducts $\wtv{a} \doteq \rwildcard{X}$ leading to
$\exptype{Pair}{\rwildcard{X}, \rwildcard{X}} \lessdot \ntv{m}$.
Finding a supertype to $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ is the crucial part.
The correct substition for $\ntv{m}$ would be $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$.
But this leads to additional branching inside the \unify{} algorithm and increases runtime.
%We refrain from using that type, because it is not denotable with Java syntax.
%Types used for normal type placeholders should be expressable Java types. % They are not!
The prefered way of dealing with this example in our opinion would be the addition of a multi-let statement to the syntax.
\begin{lstlisting}[style=letfj]
let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l, m = make(x) in compare(make(x))
\end{lstlisting}
We can make it work with a special rule in the \unify{}.
But this will only help in this specific example and not generally solve the issue.
A type $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ has atleast two immediate supertypes:
$\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ and
$\wctype{\rwildcard{X}, \rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$.
Imagine a type $\exptype{Triple}{\rwildcard{X},\rwildcard{X},\rwildcard{X}}$ already has
% TODO: how many supertypes are there?
%X.Triple<X,X,X> <: X,Y.Triple<X,Y,X> <:
%X,Y,Z.Triple<X,Y,Z>
% TODO example:
\begin{lstlisting}[style=java]
<X> Triple<X,X,X> sameL(List<X> l)
<X,Y> Triple<X,Y,Y> sameP(Pair<X,Y> l)
<X,Y> void triple(Triple<X,Y,Y> tr){}
Pair<?,?> p ...
List<?> l ...
make(t) { return t; }
triple(make(sameP(p)));
triple(make(sameL(l)));
\end{lstlisting}
\begin{constraintset}
$
\exptype{Triple}{\rwildcard{X}, \rwildcard{X}, \rwildcard{X}} \lessdot \ntv{t},
\ntv{t} \lessdotCC \exptype{Triple}{\wtv{a}, \wtv{b}, \wtv{b}}, \\
(\textit{This constraint is added later: } \exptype{Triple}{\rwildcard{X}, \rwildcard{Y}, \rwildcard{Y}} \lessdot \ntv{t})
$
% Triple<X,X,X> <. t
% ( Triple<X,Y,Y> <. t ) <- this constraint is added later
% t <. Triple<a?, b?, b?>
% t =. x.Triple<X,X,X>
\end{constraintset}
%TODO
% The goal is to proof soundness in respect to the type rules introduced by \cite{aModelForJavaWithWildcards}
% and \cite{WildcardsNeedWitnessProtection}.
% \subsection{Capture Conversion}
% The \texttt{let} statements in \TamedFJ{} act as capture conversion for wildcard types.
% \begin{figure}
% \begin{minipage}{0.45\textwidth}
% \begin{lstlisting}[style=tfgj]
% <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=letfj]
% <X> List<X> clone(List<X> l);
% (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p) =
% 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}}$
% This spawns additional problems.
% \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} \lessdotCC \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$.
% 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}
%
% Wildcards are not reflexive. A box of type $\wctype{\rwildcard{X}}{Box}{\rwildcard{X}}$
% is able to hold a value of any type. It could be a $\exptype{Box}{String}$ or a $\exptype{Box}{Integer}$ etc.
% Also two of those boxes do not necessarily contain the same type.
% But there are situations where it is possible to assume that.
% For example the type $\wctype{\rwildcard{X}}{Pair}{\exptype{Box}{\rwildcard{X}}, \exptype{Box}{\rwildcard{X}}}$
% is a pair of two boxes, which always contain the same type.
% Inside the scope of the \texttt{Pair} type, the wildcard $\rwildcard{X}$ stays the same.

11
martin.bib
View File

@ -558,3 +558,14 @@ Computing Concepts},
url = {https://www.dhbw-stuttgart.de/forschung-transfer/technik/schriftenreihe-insights} url = {https://www.dhbw-stuttgart.de/forschung-transfer/technik/schriftenreihe-insights}
} }
@article{wells1999typability,
title={Typability and type checking in System F are equivalent and undecidable},
author={Wells, Joe B},
journal={Annals of Pure and Applied Logic},
volume={98},
number={1-3},
pages={111--156},
year={1999},
publisher={Elsevier}
}

284
tRules.tex
View File

@ -1,34 +1,46 @@
\section{Syntax and Typing}\label{sec:tifj}
The input syntax for our algorithm is shown in figure \ref{fig:syntax} \section{\TamedFJ{}}\label{sec:tifj}
%LetFJ -> Output language!
%TamedFJ -> ANF transformed input langauge
%Input language only described here. It is standard Featherweight Java
% we use the transformation to proof soundness. this could also be moved to the end.
% the constraint generation step assumes every method argument to be encapsulated in a let statement. This is the way Java is doing capture conversion
The input to our algorithm is a typeless version of Featherweight Java.
The syntax is shown in figure \ref{fig:syntax}
and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}. and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}.
Our calculus is a subset of the calculus defined by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection} Method parameters and return types are optional.
with the exception that type annotations are optional in our calculus. We still require type annotations for fields and generic class parameters.
This is a design choice by us,
as we consider them as data declarations which are given by the programmer.
% They are inferred in for example \cite{plue14_3b}
Note the \texttt{new} expression not requiring generic parameters,
which are also inferred by our algorithm.
The method call naturally has type inferred generic parameters aswell.
We add the elvis operator ($\elvis{}$) to the syntax mainly to showcase applications involving wildcard types.
The syntax is described in figure \ref{fig:syntax} with optional type annotations highlighted in yellow.
It is possible to exclude all optional types.
\TamedFJ{} is a subset of the calculus defined by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection}.
%The language is designed to showcase type inference involving existential types.
The idea is for our type inference algorithm to calculate all missing types and output a fully and correctly typed \TamedFJ{} program,
which by default is also a correct Featherweight Java program (see chapter \ref{sec:soundness}).
Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm. \noindent
The input language is designed to showcase type inference involving existential types. \textit{Notes:}
Method call rule T-Call is the most interesting part, because it emulates the behaviour of a Java method call, \begin{itemize}
where existential types are implicitly \textit{opened} and \textit{closed}. \item The calculus does not include method overriding for simplicity reasons.
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.
Type inference for that is described in \cite{TIforFGJ} and can be added to this algorithm accordingly. Type inference for that is described in \cite{TIforFGJ} and can be added to this algorithm accordingly.
Our algorithm is designed for extensibility with the final goal of full support for Java. Our algorithm is designed for extensibility with the final goal of full support for Java.
\unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}. \unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}. Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
%\textit{Note:}
\item The typing rules for expressions shown in figure \ref{fig:expressionTyping} refrain from restricting polymorphic recursion.
Type inference for polymorphic recursion is undecidable \cite{wells1999typability} and when proofing completeness like in \cite{TIforFGJ} the calculus
needs to be restricted in that regard.
Our algorithm is not complete (see discussion in chapter \ref{sec:completeness}) and without the respective proof we can keep the \TamedFJ{} calculus as simple as possible
and as close to it's Featherweight Java correspondent \cite{WildcardsNeedWitnessProtection} as possible.
Our soundness proof works either way.
\end{itemize}
%Additional features like overriding methods and method overloading can be added by copying the respective parts from there. %Additional features like overriding methods and method overloading can be added by copying the respective parts from there.
%Additional features can be easily added by generating the respective constraints (Plümicke hier zitieren) %Additional features can be easily added by generating the respective constraints (Plümicke hier zitieren)
@ -40,200 +52,37 @@ Additional language constructs can be added by implementing the respective const
% on overriding methods, because their type is already determined. % on overriding methods, because their type is already determined.
% Allowing overriding therefore has no implication on our type inference algorithm. % Allowing overriding therefore has no implication on our type inference algorithm.
The syntax forces every expression to undergo a capture conversion before it can be used as a method argument. % The output is a valid Featherweight Java program.
Even variables have to be catched by a let statement first. % We use the syntax of the version introduced in \cite{WildcardsNeedWitnessProtection}
This behaviour emulates Java's implicit capture conversion. % calling it \letfj{} for that it is a Featherweight Java variant including \texttt{let} statements.
\newcommand{\highlight}[1]{\begingroup\fboxsep=0pt\colorbox{yellow}{$\displaystyle #1$}\endgroup}
\begin{figure} \begin{figure}
\par\noindent\rule{\textwidth}{0.4pt}
\center
$ $
\begin{array}{lrcl} \begin{array}{lrcl}
\hline %\hline
\text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\ \text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
\text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\ \text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
\text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\ \text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
\text{Type variable contexts} & \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\ \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{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} & ::= & \texttt{m}(\overline{\expr{x}}) \set{ \texttt{return}\ t;} \\ \text{Method declarations} & \texttt{M} & ::= & \highlight{\generics{\overline{\type{X} \triangleleft \type{N}}}}\ \highlight{\type{T}}\ \texttt{m}(\overline{\highlight{\type{T}}\ \expr{x}}) \{ \texttt{return} \ \expr{e}; \} \\
\text{Terms} & t & ::= & \expr{x} \\ \text{Terms} & \expr{e} & ::= & \expr{x} \\
& & \ \ | & \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}_c}) \\ & & \ \ | & \texttt{new} \ \type{C}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \expr{x}_c.f \\ & & \ \ | & \expr{e}.f\\
& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \expr{x}_c.\texttt{m}(\overline{\expr{x}_c}) \\ & & \ \ | & \expr{e}.\texttt{m}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
& & \ \ | & t \elvis{} t \\ & & \ \ | & \texttt{let}\ \expr{x} \highlight{: \wcNtype{\Delta}{N}} = \expr{e} \ \texttt{in} \ \expr{e}\\
& & \ \ | & \expr{e} \elvis{} \expr{e}\\
\text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\ \text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
\hline %\hline
\end{array} \end{array}
$ $
\caption{\TamedFJ{} Syntax}\label{fig:syntax} \par\noindent\rule{\textwidth}{0.4pt}
\caption{Input Syntax with optional type annotations}\label{fig:syntax}
\end{figure} \end{figure}
% \begin{figure}
% $
% \begin{array}{lrcl}
% \hline
% \text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
% \text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
% \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} & ::= & \texttt{m}(\overline{\expr{x}}) = t \\
% \text{Values} & v & ::= & \expr{x} \\
% \text{Terms} & t & ::= & v \\
% & & \ \ | & \texttt{let} \ \expr{x} = \texttt{new} \ \type{C}(\overline{v}) \ \texttt{in} \ t \\
% & & \ \ | & \texttt{let} \ \expr{x} = v.f \ \texttt{in} \ t \\
% & & \ \ | & \texttt{let} \ \expr{x} = v.\texttt{m}(\overline{v}) \ \texttt{in} \ t \\
% & & \ \ | & \texttt{let} \ \expr{x} = v \elvis{} v \ \texttt{in} \ t \\
% \text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
% \hline
% \end{array}
% $
% \caption{Input Syntax}\label{fig:syntax}
% \end{figure}
% \begin{figure}
% $
% \begin{array}{lrcl}
% \hline
% \text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
% \text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
% \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} & ::= & \texttt{m}(\overline{\expr{x}}) = t \\
% \text{Terms} & t & ::= & \expr{x} \\
% & & \ \ | & \texttt{let} \ \expr{x} = t \ \texttt{in} \ t \\
% & & \ \ | & \expr{x}.f \\
% & & \ \ | & \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
% & & \ \ | & t \elvis{} t \\
% \text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
% \hline
% \end{array}
% $
% \caption{Input Syntax}\label{fig:syntax}
% \end{figure}
% \begin{figure}
% $
% \begin{array}{lrcl}
% \hline
% \text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
% \text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
% \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} & ::= & \texttt{m}(\overline{x}) = t \\
% \text{Terms} & t & ::= & x \\
% & & \ \ | & \texttt{new} \ \type{C}(\overline{t})\\
% & & \ \ | & t.f\\
% & & \ \ | & t.\texttt{m}(\overline{t})\\
% & & \ \ | & t \elvis{} t\\
% \text{Variable contexts} & \Gamma & ::= & \overline{x:\type{T}}\\
% \hline
% \end{array}
% $
% \caption{Input Syntax}\label{fig:syntax}
% \end{figure}
\subsection{ANF transformation}\label{sec:anfTransformation}
\newcommand{\anf}[1]{\ensuremath{\tau}(#1)}
%https://en.wikipedia.org/wiki/A-normal_form)
Featherweight Java's syntax involves no \texttt{let} statement
and terms can be nested freely.
This is similar to Java's syntax.
To convert it to \TamedFJ{} additional let statements have to be added.
This is done by a \textit{A-Normal Form} \cite{aNormalForm} transformation shown in figure \ref{fig:anfTransformation}.
The input of this transformation is a Featherweight Java program in the syntax given \ref{fig:inputSyntax}
and the output is a \TamedFJ{} program.
\textit{Example:}\\
\noindent
\begin{minipage}{0.45\textwidth}
\begin{lstlisting}[style=fgj,caption=Featherweight Java]
m(l, v){
return l.add(v);
}
\end{lstlisting}
\end{minipage}%
\hfill
\begin{minipage}{0.5\textwidth}
\begin{lstlisting}[style=tfgj,caption=\TamedFJ{} representation]
m(l, v) =
let x1 = l in
let x2 = v in x1.add(x2)
\end{lstlisting}
\end{minipage}
% $
% \begin{array}{|lrcl|l}
% \hline
% & & & \textbf{Featherweight Java Terms}\\
% \text{Terms} & t & ::=
% & \expr{x}
% \\
% & & \ \ |
% & \texttt{new} \ \type{C}(\overline{t})
% \\
% & & \ \ |
% & t.f
% \\
% & & \ \ |
% & t.\texttt{m}(\overline{t})
% \\
% & & \ \ |
% & t \elvis{} t\\
% %
% \hline
% \end{array}
% $
\begin{figure}
\begin{center}
$\begin{array}{lrcl}
%\text{ANF}
& \anf{\expr{x}} & = & \expr{x} \\
& \anf{\texttt{new} \ \type{C}(\overline{t})} & = & \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}}) \\
& \anf{t.f} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \expr{x}.f \\
& \anf{t.\texttt{m}(\overline{t})} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
& \anf{t_1 \elvis{} t_2} & = & \anf{t_1} \elvis{} \anf{t_2}
\end{array}$
\end{center}
\caption{ANF Transformation}\label{fig:anfTransformation}
\end{figure}
% $
% \begin{array}{lrcl|l}
% \hline
% & & & \textbf{Featherweight Java} & \textbf{A-Normal form} \\
% \text{Terms} & t & ::=
% & \expr{x}
% & \expr{x}
% \\
% & & \ \ |
% & \texttt{new} \ \type{C}(\overline{t})
% & \texttt{let}\ \overline{x} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{x})
% \\
% & & \ \ |
% & t.f
% & \texttt{let}\ x = t \ \texttt{in}\ x.f
% \\
% & & \ \ |
% & t.\texttt{m}(\overline{t})
% & \texttt{let}\ x_1 = t \ \texttt{in}\ \texttt{let}\ \overline{x} = \overline{t} \ \texttt{in}\ x_1.\texttt{m}(\overline{x})
% \\
% & & \ \ |
% & t \elvis{} t
% & t \elvis{} t\\
% %
% \hline
% \end{array}
% $
% Each class type has a set of wildcard types $\overline{\Delta}$ attached to it.
% The type $\wctype{\overline{\Delta}}{C}{\ol{T}}$ defines a set of wildcards $\overline{\Delta}$,
% which can be used inside the type parameters $\ol{T}$.
\begin{figure}[tp] \begin{figure}[tp]
\begin{center} \begin{center}
$\begin{array}{l} $\begin{array}{l}
@ -500,9 +349,10 @@ $\begin{array}{l}
$\begin{array}{l} $\begin{array}{l}
\typerule{T-Method}\\ \typerule{T-Method}\\
\begin{array}{@{}c} \begin{array}{@{}c}
(\type{T'},\ol{T}) \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\ldots} \quad \quad
\triangle' = \overline{\type{Y} : \bot .. \type{P}} \quad \quad \generics{\ol{Y \triangleleft \type{N}}}(\exptype{C}{\ol{X}},\ol{T}) \to \type{T} \in \mathtt{\Pi}(\texttt{m}) \quad \quad
\triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \\ \triangle' = \overline{\type{Y} : \bot .. \type{P}} \\
\triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \quad \quad
\text{dom}(\triangle) = \ol{X} \quad \quad \text{dom}(\triangle) = \ol{X} \quad \quad
%\texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \ \{ \ldots \} \\ %\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 \mathtt{\Pi} | \triangle, \triangle' | \ol{x : T}, \texttt{this} : \exptype{C}{\ol{X}} \vdash \texttt{e} : \type{S} \quad \quad
@ -510,37 +360,33 @@ $\begin{array}{l}
\\ \\
\hline \hline
\vspace*{-0.3cm}\\ \vspace*{-0.3cm}\\
\mathtt{\Pi} | \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}) \set{ \texttt{return}\ \texttt{e}; } \ \ok \ \text{in C}
\end{array} \end{array}
\end{array}$ \end{array}$
\\[1em] \\[1em]
$\begin{array}{l} $\begin{array}{l}
\typerule{T-Class}\\ \typerule{T-Class}\\
\begin{array}{@{}c} \begin{array}{@{}c}
\mathtt{\Pi}' = \mathtt{\Pi} \cup \set{ \texttt{m} : (\exptype{C}{\ol{X}}, \ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M}} \\ %\forall \texttt{m} \in \ol{M} : \mathtt{\Pi}(\texttt{m}) = \generics{\ol{X \triangleleft \type{N}}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{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 = \overline{\type{X} : \bot .. \type{U}} \quad \quad
\triangle \vdash \ol{U}, \ol{T}, \type{N} \ \ok \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}} \mathtt{\Pi}' | \triangle \vdash \ol{M} \ \ok \text{ in C}
\\ \\
\hline \hline
\vspace*{-0.3cm}\\ \vspace*{-0.3cm}\\
\texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \} : \mathtt{\Pi}'' \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \} : \mathtt{\Pi}
\end{array} \end{array}
\end{array}$ \end{array}$
\\[1em] %\\[1em]
\hfill
$\begin{array}{l} $\begin{array}{l}
\typerule{T-Program}\\ \typerule{T-Program}\\
\begin{array}{@{}c} \begin{array}{@{}c}
\emptyset \vdash \texttt{L}_1 : \mathtt{\Pi}_1 \quad \quad \mathtt{\Pi} = \overline{\texttt{m} : \generics{\ol{X \triangleleft \type{N}}}\ol{T} \to \type{T}}
\mathtt{\Pi}_1 \vdash \texttt{L}_2 : \mathtt{\Pi}_1 \quad \quad
\ldots \quad \quad
\mathtt{\Pi}_{n-1} \vdash \texttt{L}_n : \mathtt{\Pi}_n \quad \quad
\\ \\
\hline \hline
\vspace*{-0.3cm}\\ \vspace*{-0.3cm}\\
\vdash \ol{L} : \mathtt{\Pi}_n \overline{D : \mathtt{\Pi}}
\end{array} \end{array}
\end{array}$ \end{array}$
\end{center} \end{center}

50
unify.tex
View File

@ -330,6 +330,13 @@ Otherwise proceed with step 3.
%$\type{T} \lessdot \ntv{a}$ constraints have three and $\type{T} \lessdot \wtv{a}$ constraints have five possible transformations. %$\type{T} \lessdot \ntv{a}$ constraints have three and $\type{T} \lessdot \wtv{a}$ constraints have five possible transformations.
\textit{Hint:}
When implementing this step via backtracking
the rules \rulename{General} and \rulename{Super} should be tried first.
% is the Same rule really necessary?
The \rulename{Settle} and \rulename{Raise} rules should only be used when none of the rules in figure \ref{fig:step2-rules} can be applied.
\item[Step 3:] \item[Step 3:]
Apply the rules in figure \ref{fig:cleanup-rules} exhaustively. Apply the rules in figure \ref{fig:cleanup-rules} exhaustively.
\rulename{Ground} and \rulename{Flatten} deal with constraints containing free variables. \rulename{Ground} and \rulename{Flatten} deal with constraints containing free variables.
@ -648,7 +655,7 @@ Prepare, Capture, Reduce, Trim, Clear, Exclude, Adapt
\rulename{Bot} \rulename{Bot}
& $ & $
\begin{array}[c]{l} \begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \bot \lessdot_1 \type{T} } \\ \wildcardEnv \vdash C \cup \set{ \bot \lessdot \type{T} } \\
\hline \hline
\vspace*{-0.4cm}\\ \vspace*{-0.4cm}\\
\wildcardEnv \vdash C \wildcardEnv \vdash C
@ -658,7 +665,7 @@ Prepare, Capture, Reduce, Trim, Clear, Exclude, Adapt
\rulename{Pit} \rulename{Pit}
$ $
\begin{array}[c]{l} \begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot_1 \bot } \\ \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \bot } \\
\hline \hline
\vspace*{-0.4cm}\\ \vspace*{-0.4cm}\\
\wildcardEnv \vdash C \cup \set{ \tv{a} \doteq \bot } \wildcardEnv \vdash C \cup \set{ \tv{a} \doteq \bot }
@ -1081,23 +1088,28 @@ $\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \cap \Delta_{in}
% } % }
% \end{array} % \end{array}
% $ % $
\\\\ % \\\\
\cdashline{1-2} \\ % \cdashline{1-2} \\
\rulename{\generalizeRule{}W} %TODO: Change description for step 2! % \rulename{\generalizeRule{}W} %TODO: Change description for step 2!
& $ % & $
\begin{array}[c]{l} % \begin{array}[c]{l}
\wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \wtv{a}\\ % \wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \wtv{a}\\
\hline % \hline
\wildcardEnv \vdash C \cup \set{\wctype{\Delta}{C}{\ol{T}} \lessdot \wtv{a}, % \wildcardEnv \vdash C \cup \set{\wctype{\Delta}{C}{\ol{T}} \lessdot \wtv{a},
\wtv{a} \doteq \wctype{\overline{\wildcard{X}{\wtv{u}}{\wtv{l}}}}{C}{\overline{\rwildcard{X}}}, % \wtv{a} \doteq \wctype{\overline{\wildcard{X}{\wtv{u}}{\wtv{l}}}}{C}{\overline{\rwildcard{X}}},
%\overline{\tv{l} \lessdot \tv{u}}, % not needed, due to subst and reduce rule which are used afterwards % %\overline{\tv{l} \lessdot \tv{u}}, % not needed, due to subst and reduce rule which are used afterwards
\overline{\wtv{u} \lessdot \type{S}} % \overline{\wtv{u} \lessdot \type{S}}
} % }
\end{array} \quad \begin{array}[c]{l} % \end{array} \quad \begin{array}[c]{l}
\texttt{class} \ \exptype{C}{\ol{X \triangleleft \type{S}}} \triangleleft \exptype{D}{\ol{N}} \\ % \texttt{class} \ \exptype{C}{\ol{X \triangleleft \type{S}}} \triangleleft \exptype{D}{\ol{N}} \\
\text{fresh}\ \overline{\wildcard{X}{\wtv{u}}{\wtv{l}}} % \text{fresh}\ \overline{\wildcard{X}{\wtv{u}}{\wtv{l}}}
\end{array} % \end{array}
$ % $
% %The idea behind the GeneralW rule is, that a constraint X.Pair<X,X> <. a? can be resolved:
% % X.Pair<X,X> <. Y,Z.Pair<Y,Z>
% % X =. y, X =. z, y <. yu?, z <. zu?, yl? <. y, zl? <. z
% % X <. yu?, X <. zu?, yl? <. X, zl? <. X
% % ???
\end{tabular} \end{tabular}
} }
\end{center} \end{center}