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

Compare commits

base: stan:lncs
Branches Tags
stan:master stan:cctv stan:lncs stan:completeness stan:cleanup stan:MultiLet
..
compare: stan:completeness
Branches Tags
stan:master stan:cctv stan:lncs stan:completeness stan:cleanup stan:MultiLet

3 Commits
lncs ... completene

Author SHA1 Message Date
Andreas Stadelmeier
5371824a55 Comments 2024-04-03 00:50:59 +02:00
Andreas Stadelmeier
c6571879b7 Comments to Completeness 2024-04-03 00:46:29 +02:00
JanUlrich
3620f0c781 Change rules so Completeness proof is possible 2024-04-02 00:09:52 +02:00
18 changed files with 2988 additions and 4982 deletions
Expand all files Collapse all files

39
TIforWildFJ.tex
View File

@@ -1,5 +1,5 @@
\documentclass{llncs}
\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate]{lipics-v2021}
%This is a template for producing LIPIcs articles.
%See lipics-v2021-authors-guidelines.pdf for further information.
%for A4 paper format use option "a4paper", for US-letter use option "letterpaper"
@@ -40,7 +40,6 @@
\input{prolog}
\begin{document}
\bibliographystyle{plainurl}% the mandatory bibstyle
\title{Global Type Inference for Featherweight Java with Wildcards} %TODO Please add
@@ -55,16 +54,16 @@
\authorrunning{A. Stadelmeier and M. Plümicke and P. Thiemann} %TODO mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et al.'
%\Copyright{Andreas Stadelmeier and Martin Plümicke and Peter Thiemann} %TODO mandatory, please use full first names. LIPIcs license is "CC-BY"; http://creativecommons.org/licenses/by/3.0/
\Copyright{Andreas Stadelmeier and Martin Plümicke and Peter Thiemann} %TODO mandatory, please use full first names. LIPIcs license is "CC-BY"; http://creativecommons.org/licenses/by/3.0/
%\ccsdesc[500]{Software and its engineering~Language features}
\ccsdesc[500]{Software and its engineering~Language features}
%\ccsdesc[300]{Software and its engineering~Syntax}
\keywords{type inference, Java, subtyping, generics} %TODO mandatory; please add comma-separated list of keywords
%\category{} %optional, e.g. invited paper
\category{} %optional, e.g. invited paper
%\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
%\relatedversiondetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93]{Classification (e.g. Full Version, Extended Version, Previous Version}{URL to related version} %linktext and cite are optional
%\supplement{}%optional, e.g. related research data, source code, ... hosted on a repository like zenodo, figshare, GitHub, ...
@@ -78,20 +77,21 @@
% %Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \EventEditors{John Q. Open and Joan R. Access}
% \EventNoEds{2}
% \EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
% \EventShortTitle{CVIT 2016}
% \EventAcronym{CVIT}
% \EventYear{2016}
% \EventDate{December 24--27, 2016}
% \EventLocation{Little Whinging, United Kingdom}
% \EventLogo{}
% \SeriesVolume{42}
% \ArticleNo{23}
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\EventEditors{John Q. Open and Joan R. Access}
\EventNoEds{2}
\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
\EventShortTitle{CVIT 2016}
\EventAcronym{CVIT}
\EventYear{2016}
\EventDate{December 24--27, 2016}
\EventLocation{Little Whinging, United Kingdom}
\EventLogo{}
\SeriesVolume{42}
\ArticleNo{23}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
\maketitle
@@ -146,7 +146,6 @@ class Example{
\include{soundness}
%\include{termination}
\include{relatedwork}
\bibliography{martin}

BIN
cc-by.pdf Normal file
View File

Binary file not shown.

124
conclusion.tex
View File

@@ -1,132 +1,10 @@
\section{Properties of the Algorithm}
\begin{itemize}
\item 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}.
Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
\end{itemize}
%TODO: how are the challenges solved: Describe this in the last chapter with examples!
\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}
% 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}).
As you can see by the given examples our type inference algorithm can calculate
type solutions for programs involving wildcards.
Going further we try to prove soundness and completeness for \unify{}.
Going further we try to proof soundness and completeness for \unify{}.
% The tricks are:

238
constraints.tex
View File

@@ -1,71 +1,7 @@
\subsection{Capture Constraints}
%TODO: General Capture Constraint explanation
Capture Constraints are bound to a variable.
For example a let statement like \lstinline{let x = v in x.get()} will create the capture constraint
$\tv{x} \lessdotCC_x \exptype{List}{\wtv{a}}$.
This time we annotated the capture constraint with an $x$ to show its relation to the variable \texttt{x}.
Let's do the same with the constraints generated by the \texttt{concat} method invocation in listing \ref{lst:faultyConcat},
creating the constraints \ref{lst:sameConstraints}.
\begin{figure}
\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[caption=Faulty Method Call,label=lst:faultyConcat]{tamedfj}
List<?> v = ...;
let x = v in
let y = v in
concat(x, y) // Error!
\end{lstlisting}\end{minipage}
\hfill
\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[caption=Annotated constraints,mathescape=true,style=constraints,label=lst:sameConstraints]
$\tv{x} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{x}$
$\tv{y} \lessdotCC_\texttt{y} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{y}$
\end{lstlisting}
\end{minipage}
\end{figure}
During the \unify{} process it could happen that two syntactically equal capture constraints evolve,
but they are not the same because they are each linked to a different let introduced variable.
In this example this happens when we substitute $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\tv{x}$ and $\tv{y}$
resulting in:
%For example by substituting $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{x}]$ and $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{y}]$:
\begin{displaymath}
\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_x \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_y \exptype{List}{\wtv{a}}
\end{displaymath}
Thanks to the original annotations we can still see that those are different constraints.
After \unify{} uses the \rulename{Capture} rule on those constraints
it gets obvious that this constraint set is unsolvable:
\begin{displaymath}
\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}},
\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}
\end{displaymath}
%In this paper we do not annotate capture constraint with their source let statement.
The rest of this paper will not annotate capture constraints with variable names.
Instead we consider every capture constraint as distinct to other capture constraints even when syntactically the same,
because we know that each of them originates from a different let statement.
\textit{Hint:} An implementation of this algorithm has to consider that seemingly equal capture constraints are actually not the same
and has to allow doubles in the constraint set.
% %We see the equality relation on Capture constraints is not reflexive.
% A capture constraint is never equal to another capture constraint even when structurally the same
% ($\type{T} \lessdotCC \type{S} \neq \type{T} \lessdotCC \type{S}$).
% This is necessary to solve challenge \ref{challenge:1}.
% A capture constraint is bound to a specific let statement.
\textit{Note:}
In the special case \lstinline{let x = v in concat(x,x)} the constraints would look like
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}},
\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
and we could actually delete one of them without loosing information.
But this case will never occur in our algorithm, because the let statements for our input programs are generated by a ANF transformation (see \ref{sec:anfTransformation}).
\section{Constraint generation}\label{chapter:constraintGeneration}
% Our type inference algorithm is split into two parts.
% A constraint generation step \textbf{TYPE} and a \unify{} step.
% Method names are not unique.
% It is possible to define the same method in multiple classes.
% The \TYPE{} algorithm accounts for that by generating Or-Constraints.
@@ -77,105 +13,27 @@ But this case will never occur in our algorithm, because the let statements for
% 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
\begin{description}
\item[input] \TamedFJ{} program in A-Normal form
\item[output] Constraints
\end{description}
The constraint generation works on the \TamedFJ{} language.
This step is mostly the same as in \cite{TIforFGJ} except for field access and method invocation.
We will focus on those two parts where also the new capture constraints and wildcard type placeholders are introduced.
This step is mostly same as in \cite{TIforFGJ} except for field access and method invocation.
We will focus on those parts.
Here 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}).
%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]
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.
\begin{verbatim}
m(l, v){
return l.add(v);
let x = x in x.add(v)
}
\end{lstlisting}
\end{minipage}%
\hfill
\begin{minipage}{0.5\textwidth}
\begin{lstlisting}[style=tfgj,caption=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}
\end{verbatim}
\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}
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.
\begin{figure}
\center
$
\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{Syntax of a \TamedFJ{} program in 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.
% 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.
During constraint generation the algorithm does not know the parameter types yet.
We generate $\lessdotCC$ constraints and let \unify{} do the capture conversion.
$\lessdotCC$ constraints are kept until they reach the form $\type{G} \lessdotCC \type{G}$ and a capture conversion is possible.
% TODO: Challenge examples!
At points where a well-formed type is needed we use a normal type placeholder.
Inside a method call expression sub expressions (receiver, parameter) wildcard placeholders are used.
@@ -184,12 +42,25 @@ A normal type placeholder cannot hold types containing free variables.
Normal type placeholders are assigned types which are also expressible with Java syntax.
So no types like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ or $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
It is possible to feed the \unify{} algorithm a set of free variables with predefined bounds.
This is used for class generics see figure \ref{fig:constraints-for-classes}.
The \fjtype{} function returns a set of constraints aswell as an initial environment $\Delta$
containing the generics declared by this class.
Type variables declared in the class header are passed to \unify{}.
Those type variables count as regular types and can be held by normal type placeholders.
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
%% a method call, does not know which type it will produce
@@ -197,37 +68,42 @@ Those type variables count as regular types and can be held by normal type place
%NO equals constraints during the constraint generation step!
\begin{figure}[tp]
\center
\begin{tabular}{lcll}
$C $ &$::=$ &$\overline{c}$ & Constraint set \\
$c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \lessdotCC \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
$\type{T}, \type{U}, \type{L} $ & $::=$ & $\tv{a} \mid \gtype{G}$ & Type placeholder or Type \\
$\tv{a}$ & $::=$ & $\ntv{a} \mid \wtv{a}$ & Normal and wildcard type placeholder \\
$\gtype{G}$ & $::=$ & $\type{X} \mid \ntype{N}$ & Wildcard, or Class Type \\
$\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\triangle}{C}{\ol{T}} $ & Class Type \\
$\triangle$ & $::=$ & $\overline{\wtype{W}}$ & Wildcard Environment \\
$\wtype{W}$ & $::=$ & $\wildcard{X}{U}{L}$ & Wildcard \\
\end{tabular}
\caption{Syntax of types and constraints used by \fjtype{} and \unify{}}
\begin{align*}
% Type
\type{T}, \type{U} &::= \tv{a} \mid \wtv{a} \mid \mv{X} \mid {\wcNtype{\Delta}{N}} && \text{types and type placeholders}\\
\type{N} &::= \exptype{C}{\ol{T}} && \text{class type (with type variables)} \\
% Constraints
\constraint &::= \type{T} \lessdot \type{U} \mid \type{T} \lessdotCC \type{U} && \text{Constraint}\\
\consSet &::= \set{\constraints} && \text{constraint set}\\
% Method assumptions:
\methodAssumption &::= \texttt{m} : \exptype{}{\ol{Y}
\triangleleft \ol{P}}\ \ol{\type{T}} \to \type{T} &&
\text{method
type assumption}\\
\localVarAssumption &::= \texttt{x} : \itype{T} && \text{parameter
assumption}\\
\mtypeEnvironment & ::= \overline{\methodAssumption} &
& \text{method type environment} \\
\typeAssumptionsSymbol &::= ({\mtypeEnvironment} ; \overline{\localVarAssumption})
\end{align*}
\caption{Syntax of constraints and type assumptions}
\label{fig:syntax-constraints}
\end{figure}
\begin{figure}[tp]
\begin{gather*}
\begin{array}{@{}l@{}l}
\fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\overline{\type{X} \triangleleft \type{N}}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\
\fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\ol{X} \triangleleft \ol{N}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\
& \begin{array}{ll@{}l}
\textbf{let} & \ol{\methodAssumption} =
\set{ \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \mid
\set{ \mv{m}(\ol{x}) = \expr{e} } \in \ol{M}, \, \tv{a}, \ol{\tv{a}}\ \text{fresh} } \\
& \Delta = \set{ \overline{\wildcard{X}{\type{N}}{\bot}} } \\
& C = \begin{array}[t]{l}
\textbf{in}
& \begin{array}[t]{l}
\set{ \typeExpr(\mtypeEnvironment \cup \ol{\methodAssumption} \cup \set{\mv{this} :
\exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}} }, \texttt{e}, \tv{a})
\\ \quad \quad \quad \quad \mid \set{ \mv{m}(\ol{x}) = \expr{e} } \in \ol{M},\, \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \in \ol{\methodAssumption}}
\end{array} \\
\textbf{in}
& (\Delta, C)
\end{array}
\end{array}
\end{array}
\end{gather*}
@@ -415,12 +291,12 @@ cannot be used anywhere else then inside the constraints generated by the method
\typeExpr{} &({\mtypeEnvironment} , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\
& \begin{array}{ll}
\textbf{let}
& \ol{\ntv{r}}, \ol{\ntv{a}} \ \text{fresh} \\
& \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\ntv{r}}) \\
& C = \set{\ol{\ntv{r}} \lessdot [\ol{\ntv{a}}/\ol{X}]\ol{T}, \ol{\ntv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\
& \ol{\tv{r}} \ \text{fresh} \\
& \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\tv{r}}) \\
& C = \set{\ol{\tv{r}} \lessdot [\ol{\tv{a}}/\ol{X}]\ol{T}, \ol{\tv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\
{\mathbf{in}} & {
\overline{\consSet} \cup
\set{\tv{a} \doteq \exptype{C}{\ol{\ntv{a}}}}}
\set{\tv{a} \doteq \exptype{C}{\ol{a}}}}
\end{array}
\end{array}
\end{displaymath}

BIN
fig1.eps
View File

Binary file not shown.

1069
introduction.tex
View File

File diff suppressed because it is too large Load Diff

BIN
lipics-logo-bw.pdf Normal file
View File

Binary file not shown.

1260
lipics-v2021.cls Normal file
View File

File diff suppressed because it is too large Load Diff

1244
llncs.cls
View File

File diff suppressed because it is too large Load Diff

117
martin.bib
View File

@@ -50,8 +50,6 @@ keywords = {subtyping, type inference, principal types}
SERIES = {Lecture Notes in Artificial Intelligence}
}
@article{DM82,
author={Luis Damas and Robin Milner},
title={Principal type-schemes for functional programs},
@@ -67,39 +65,14 @@ keywords = {subtyping, type inference, principal types}
pages={23-41},
month=Jan,
year={1965}}
@article{DBLP:journals/jcss/Milner78,
author = {Robin Milner},
title = {A Theory of Type Polymorphism in Programming},
journal = {Journal of Computer and Systems Sciences},
volume = {17},
number = {3},
pages = {348--375},
year = {1978},
url = {https://doi.org/10.1016/0022-0000(78)90014-4},
doi = {10.1016/0022-0000(78)90014-4},
timestamp = {Tue, 16 Feb 2021 14:04:22 +0100},
biburl = {https://dblp.org/rec/journals/jcss/Milner78.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{MM82,
author = {Martelli, Alberto and Montanari, Ugo},
title = {An Efficient Unification Algorithm},
year = {1982},
issue_date = {April 1982},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {4},
number = {2},
issn = {0164-0925},
url = {https://doi.org/10.1145/357162.357169},
doi = {10.1145/357162.357169},
journal = {ACM Trans. Program. Lang. Syst.},
month = {apr},
pages = {258–282},
numpages = {25}
}
author={A. Martelli and U. Montanari},
title={An Efficient Unification Algorithm},
journal={ACM Transactions on Programming Languages and Systems},
volume={4},
pages={258-282},
year={1982}}
@InProceedings{Plue07_3,
author = {Martin Pl{\"u}micke},
@@ -353,14 +326,6 @@ articleno = {138},
numpages = {22},
keywords = {Null, Java Wildcards, Existential Types}
}
@inproceedings{AT16,
author = {Amin, Nada and Tate, Ross},
year = {2016},
month = {10},
pages = {838-848},
title = {Java and scala's type systems are unsound: the existential crisis of null pointers},
doi = {10.1145/2983990.2984004}
}
@InProceedings{TIforFGJ,
author = {Stadelmeier, Andreas and Pl\"{u}micke, Martin and Thiemann, Peter},
title = {{Global Type Inference for Featherweight Generic Java}},
@@ -387,16 +352,6 @@ doi = {10.1145/2983990.2984004}
publisher={Addison-Wesley Professional}
}
@Book{GoJoStBrBuSm23,
author = {Gosling, James and Joy, Bill and Steele, Guy and Bracha, Gilad and Buckley, Alex and Smith, Daniel},
title = "{The Java\textsuperscript{\textregistered} {L}anguage {S}pecification}",
Optpublisher = "Addison-Wesley",
url = {https://docs.oracle.com/javase/specs/jls/se21/jls21.pdf},
edition = {{J}ava {S}{E} 21},
year = 2023,
OPtseries = {The Java series}
}
@inproceedings{semanticWildcardModel,
title={Towards a semantic model for Java wildcards},
author={Summers, Alexander J and Cameron, Nicholas and Dezani-Ciancaglini, Mariangiola and Drossopoulou, Sophia},
@@ -433,7 +388,7 @@ numpages = {14},
keywords = {existential types, joins, parametric types, single-instantiation inheritance, subtyping, type inference, wildcards}
}
@inproceedings{javaTIisBroken,
@inproceedings{10.1145/1449764.1449804,
author = {Smith, Daniel and Cartwright, Robert},
title = {Java type inference is broken: can we fix it?},
year = {2008},
@@ -511,61 +466,3 @@ keywords = {Compilation, Java, generic classes, language design, language semant
publisher={ACM New York, NY, USA}
}
@InProceedings{PH23,
author = {Martin Pl{\"u}micke and Daniel Holle},
title = {Principal generics in {J}ava--{T}{X}},
crossref = {kps2023},
pages = {122--143},
year = {2023},
Opteditor = {Thomas Noll and Ira Fesefeldt},
address = {Aachen},
Optnumber = {AIB-2023-03},
month = {September},
series = {Aachener Informatik-Berichte (AIB)},
url = {https://publications.rwth-aachen.de/record/972197/files/972197.pdf#%5B%7B%22num%22%3A281%2C%22gen%22%3A0%7D%2C%7B%22name%22%3A%22XYZ%22%7D%2C89.292%2C740.862%2Cnull%5D},
Optdoi = {10.18154/RWTH-2023-10034},
Optnote = {(to appear)}
}
@Proceedings{kps2023,
booktitle = {22. Kolloquium Programmiersprachen und Grundlagen der Programmierung},
year = {2023},
editor = {Noll, Thomas and Fesefeldt, Ira Justus},
number = {AIB-2023-03},
series = {Technical report / Department of Computer Science. - Informatik},
month = {September},
organization = {RWTH Aachenen},
doi = {10.18154/RWTH-2023-10034}
}
@InProceedings{plue24_1,
author = {Martin Pl{\"u}micke},
title = {Avoiding the Capture Conversion in {J}ava--{T}{X}},
crossref = {HKPTW24},
pages = {109--115},
year = {2023}
}
@proceedings{HKPTW24,
author = {Daniel Holle and Jens Knoop and Martin Pl\"umicke and Peter Thiemann and Baltasar Tranc\'{o}n y Widemann},
booktitle = {Proceedings of the 38th and 39th Annual Meeting of the GI Working Group Programming Languages and
Computing Concepts},
institution = {DHBW Stuttgart},
year = {2024},
series = {INSIGHTS -- Schriftenreihe der Fakult\"at Technik},
number = {01/2024},
ISSN = {2193-9098},
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}
}

BIN
orcid.pdf Normal file
View File

Binary file not shown.

19
prolog.tex
View File

@@ -11,21 +11,14 @@
escapeinside={(*@}{@*)},
captionpos=t,float,abovecaptionskip=-\medskipamount
}
\lstdefinestyle{fgj}{backgroundcolor=\color{lime!20}}
\lstdefinestyle{tfgj}{backgroundcolor=\color{lightgray!20}}
\lstdefinestyle{letfj}{backgroundcolor=\color{lime!20}}
\lstdefinestyle{tamedfj}{backgroundcolor=\color{yellow!20}}
\lstdefinestyle{java}{backgroundcolor=\color{lightgray!20}}
\lstdefinestyle{constraints}{
basicstyle=\normalfont,
backgroundcolor=\color{red!20}
}
\newtheorem{recap}[note]{Recap}
\newcommand{\rulenameAfter}[1]{\begin{array}[b]{l}\rulename{#1}\\[-1em] \ \end{array}}
\newcommand{\tifj}{\texttt{TamedFJ}}
\newcommand{\wcSep}{\vdash}
@@ -78,9 +71,6 @@
\newcommand\subeq{\mathbin{\texttt{<:}}}
\newcommand\extends{\ensuremath{\triangleleft}}
\newcommand{\QMextends}[1]{\textrm{\normalshape\ttfamily ?\,extends}\linebreak[0]\,#1}
\newcommand{\QMsuper}[1]{\textrm{\normalshape\ttfamily ?\linebreak[0]\,su\-per}\linebreak[0]\,#1}
\newcommand\rulename[1]{\textup{\textsc{(#1)}}}
\newcommand{\generalizeRule}{General}
@@ -107,8 +97,7 @@
\newcommand{\constraints}{\ensuremath{\mathit{\overline{c}}}}
\newcommand{\itype}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\il}[1]{\ensuremath{\overline{\itype{#1}}}}
\newcommand{\gtype}[1]{\type{#1}}
\newcommand{\type}[1]{\ensuremath{\mathtt{#1}}}
\newcommand{\type}[1]{\mathtt{#1}}
\newcommand{\anyType}[1]{\mathit{#1}}
\newcommand{\gType}[1]{\texttt{#1}}
\newcommand{\mtypeEnvironment}{\ensuremath{\Pi}}
@@ -116,7 +105,7 @@
\newcommand{\localVarAssumption}{\ensuremath{\mathtt{\eta}}}
\newcommand{\expandLB}{\textit{expandLB}}
\newcommand{\letfj}{\textbf{LetFJ}}
\newcommand{\letfj}{\emph{LetFJ}}
\newcommand{\tph}{\text{tph}}
\newcommand{\expr}[1]{\texttt{#1}}
@@ -132,8 +121,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]{\tv{#1}}
%\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
\newcommand{\ntv}[1]{\tv{#1}}
\newcommand{\wcstore}{\ensuremath{\Delta}}
%\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}_?}}

76
relatedwork.tex
View File

@@ -1,76 +0,0 @@
\section{Related Work}
Igarashi et al \cite{FJ} define Featherweight Java
and its generic sibling, Featherweight Generic Java. Their language is
a functional calculus reduced to the bare essentials, they develop the full metatheory, they
support generics, and study the type erasing transformation used by
the Java compiler. Stadelmeier et. al. extends this approach by global type
inference \cite{TIforFGJ}.
\subsection{Wildcards in formal Java models}
Wildcards are first described in a research paper in \cite{addingWildcardsToJava}. In
\cite{TEP05} the Featherweight Java-Calculus \textsf{Wild~ FJ} is introduced. It
contains a formal description of wildcards. The Java Language Specification
\cite{GoJoStBrBuSm23} refers to \textsf{Wild~FJ} for the introduction of
wildcards. In \cite{aModelForJavaWithWildcards} a formal model based of explicite existential types
is introduced and proven as sound. Additionally, for a subset of Java a
translation to the formal model is given, such that this subset is proven as
sound. In \cite{WildcardsNeedWitnessProtection} another core calculus is
introduced, which is proven as
sound, too. In this paper it is shown that the unsoundness of Java which is
discovered in \cite{AT16} is avoidable, even in the absence of nullness-aware type
system. In \cite{TamingWildcards} finally a framework is presented which combines
use-site variance (wildcards as in Java) and definition-site variance (as in Scala). For
instance, it can be used to add use-site variance to Scala and extend the Java
type system to infer the definition-site variance.
Our calculus is mixture ...
\subsection{Type inference}
Some object-oriented languages like Scala, C\#, and Java perform
\emph{local} type inference \cite{PT98,OZZ01}. Local type
inference means that missing type annotations are recovered using only
information from adjacent nodes in the syntax tree without long distance
constraints. For instance, the type of a variable initialized with a
non-functional expression or the return type of a method can be
inferred. However, method argument types, in particular for recursive
methods, cannot be inferred by local type inference.
Milner's algorithm $\mathcal{W}$ \cite{DBLP:journals/jcss/Milner78} is
the gold standard for global type inference for languages with
parametric polymorphism, which is used by ML-style languages. The fundamental idea
of the algorithm is to enforce type equality by many-sorted type
unification \cite{Rob65,MM82}. This approach is effective and results
in so-called principal types because many-sorted unification is
unitary, which means that there is at most one most general result.
Pl\"umicke \cite{Plue07_3} presents a first attempt to adopt Milner's
approach to Java. However, the presence of subtyping means that type
unification is no longer unitary, but still finitary. Thus, there is
no longer a single most general type, but any type is an instance of a
finite set of maximal types (for more details see Section
\ref{sec:unification}). Further work by the same author
\cite{plue15_2,plue17_2},
refines this approach by moving to a constraint-based algorithm and by
considering lambda expressions and Scale-like function types.
Pluemicke has a different approach to introduce wildcards in \cite{plue09_1}. He
allows wildcards as any subsitution for type variables and disclaim the
capture conversion. Instead he extended
the subtyping ordering such that for $\theta \sub \theta' \sub \theta''$ holds
indeed the transitiv closure of $\QMextends{\theta} \sub \theta'$ and $\theta' \sub
\QMsuper{\theta''}$ but not the reflexive closure. He gave a type unification
algorithm for this type system, which he proved as sound and complete.
The problem of his type system is in the lossing reflexivity as shown in
example \ref{intro-example1}. First approaches to solve this problem he gave in
\cite{plue24_1}, where he fixes that no pairwise different nodes in the
abstract syntax gets the same type variable and that no pairwise different type
variables are equalized. In \cite{PH23} he showed how his type inference
algorithm suffices theese properties.
In Pl\"umicke's work there is indeed a formal definition of the subtying
ordering and a correctness proof of the type unification algorithms but no
soundness proof of the type system, itself. Therefore we choose for our type
inference algorithms with wildcars the approach of ???????

8
soundness.tex
View File

@@ -1,5 +1,7 @@
\section{Soundness}
\newcommand{\CC}{\text{CC}}
\begin{lemma}
A sound TypelessFJ program is also sound under LetFJ type rules.
\begin{description}
@@ -152,7 +154,7 @@ By structural induction over the expression $\texttt{e}$.
% $\sigma(\ol{\tv{r}}) = \overline{\wcNtype{\Delta}{N}}$,
% $\ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
% TODO: S ok? We could proof $\Delta, \Delta' \overline{\Delta} \vdash \ol{S} \ \ok$
% by proving every substitution in Unify is ok aslong as every type in the inputs is ok
% by proofing every substitution in Unify is ok aslong as every type in the inputs is ok
% S ok when all variables are in the environment and every L <: U and U <: Class-bound
% This can be given by the constraints generated. We can proof if T ok and S <: T and T <: S' then S ok and S' ok
@@ -386,8 +388,6 @@ $\Delta \vdash \sigma(C') \implies \Delta \vdash \sigma(C)$
\item[Settle] Assumption, S-Trans
\item[Super] S-Extends ($\vdash \wctype{\Delta}{C}{\ol{T}} <: \wctype{\Delta}{D}{[\ol{T}/\ol{X}]\ol{N}}$), S-Trans
\item[\generalizeRule{}] by Assumption, because $C \subset C'$
\item[Same] by S-Exists
\item[SameW] %TODO
\item[Adapt] Assumption, S-Extends, S-Trans
\item[Adopt] Assumption, because $C \subset C'$
%\item[Capture, Reduce] are always applied together. We have to destinct between two cases:
@@ -424,7 +424,7 @@ Therefore we can say that $\Delta, \Delta', \overline{\Delta} \vdash \sigma'(\ex
% List<X> <. Y.List<Y>, free variables are either in
If $\text{fv}(\exptype{C}{\ol{S}}) = \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.
Otherwise
$\Delta' \vdash \text{CC}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$
$\Delta' \vdash \CC{}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$
holds with any $\Delta'$ so that $(\text{fv}(\exptype{C}{\ol{S}}) \cup \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) ) \subseteq \text{dom}(\Delta') $.
\item[Match] Assumption, S-Trans
\item[Trim] Assumption and S-Exists

1548
splncs04.bst
View File

File diff suppressed because it is too large Load Diff

298
tRules.tex
View File

@@ -1,43 +1,32 @@
\section{Syntax and Typing}\label{sec:tifj}
\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}
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}.
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: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}).
\noindent
\textit{Notes:}
\begin{itemize}
\item The calculus does not include method overriding for simplicity reasons.
Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
The input language is designed to showcase type inference involving existential types.
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.
Type inference for that is described in \cite{TIforFGJ} and can be added to this algorithm accordingly.
%\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 proving 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}
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}.
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 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)
@@ -49,37 +38,200 @@ Our soundness proof works either way.
% on overriding methods, because their type is already determined.
% Allowing overriding therefore has no implication on our type inference algorithm.
% 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.
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.
\newcommand{\highlight}[1]{\begingroup\fboxsep=0pt\colorbox{yellow}{$\displaystyle #1$}\endgroup}
\begin{figure}
\par\noindent\rule{\textwidth}{0.4pt}
\center
$
\begin{array}{lrcl}
%\hline
\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{Method declarations} & \texttt{M} & ::= & \texttt{m}(\overline{\expr{x}}) = t \\
\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 \\
\text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
%\hline
\hline
\end{array}
$
\par\noindent\rule{\textwidth}{0.4pt}
\caption{Input Syntax with optional type annotations}\label{fig:syntax}
\caption{\TamedFJ{} 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{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}
\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{center}
$\begin{array}{l}
@@ -137,7 +289,7 @@ $\begin{array}{l}
\Delta', \Delta \vdash [\ol{T}/\ol{\type{X}}]\ol{L} <: \ol{T} \quad \quad
\Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\
\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta, \Delta') \quad
\text{dom}(\Delta') \cap \text{fv}(\wcNtype{\ol{\wildcard{X}{U}{L}}}{N}) = \emptyset
\text{dom}(\Delta') \cap \text{fv}(\wctype{\ol{\wildcard{X}{U}{L}}}{C}{\ol{S}}) = \emptyset
\\
\hline
\vspace*{-0.3cm}\\
@@ -308,15 +460,18 @@ $\begin{array}{l}
\end{array}$
\\[1em]
$\begin{array}{l}
%TODO: why is dom(\Delta) subset of fv(N) a restriction. This excludes X,Y^X.Pair<X,Y>?
%TODO: we do not allow X.Pair<X,X> in the t-let (could we allow it? what about L and U being WTVs?)
\typerule{T-Let}\\
\begin{array}{@{}c}
\Delta | \Gamma \vdash \expr{t}_1 : \type{T}_1 \quad \quad
\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}
%\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}
\Delta \vdash \type{T}_1 <: \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{X}}
\\
\Delta, \Delta' | \Gamma, \expr{x} : \wcNtype{}{N} \vdash \expr{t}_2 : \type{T}_2 \quad \quad
\Delta, \Delta' | \Gamma, \expr{x} : \wctype{}{C}{\ol{X}} \vdash \expr{t}_2 : \type{T}_2 \quad \quad
\Delta, \Delta' \vdash \type{T}_2 <: \type{T} \quad \quad
\text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
\Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok
% \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
\Delta \vdash \type{T}, \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{X}} \ \ok
\\
\hline
\vspace*{-0.3cm}\\
@@ -346,10 +501,9 @@ $\begin{array}{l}
$\begin{array}{l}
\typerule{T-Method}\\
\begin{array}{@{}c}
\texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\ldots} \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' = \overline{\type{Y} : \bot .. \type{P}} \\
\triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \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
%\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
@@ -357,33 +511,37 @@ $\begin{array}{l}
\\
\hline
\vspace*{-0.3cm}\\
\mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) \set{ \texttt{return}\ \texttt{e}; } \ \ok \ \text{in C}
\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}
%\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} : (\exptype{C}{\ol{X}}, \ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{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}
\mathtt{\Pi}' | \triangle \vdash \ol{M} \ \ok \text{ in C with} \ \generics{\ol{Y \triangleleft P}}
\\
\hline
\vspace*{-0.3cm}\\
\mathtt{\Pi} \vdash \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \}
\texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \} : \mathtt{\Pi}''
\end{array}
\end{array}$
%\\[1em]
\hfill
\\[1em]
$\begin{array}{l}
\typerule{T-Program}\\
\begin{array}{@{}c}
\mathtt{\Pi} = \overline{\texttt{m} : \generics{\ol{X \triangleleft \type{N}}}\ol{T} \to \type{T}}
\emptyset \vdash \texttt{L}_1 : \mathtt{\Pi}_1 \quad \quad
\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
\vspace*{-0.3cm}\\
\mathtt{\Pi} \vdash \overline{D}
\vdash \ol{L} : \mathtt{\Pi}_n
\end{array}
\end{array}$
\end{center}

16
todo-11.4.24
View File

@@ -1,16 +0,0 @@
- Eingangsbeispiel
- Motivation (gibt es ein nicht funktionierendes Beispiel für lokale Typinferenz was mit unserem algorithmus funktioniert)
- Zeile 52 steht LetFJ, muss eingeführt werden
- Operatoren motivieren. Denotable expressable types
Java macht CC implizit. Wir machen es mit let statements. Dadurch LetFJ einführen
- Java macht es anders. es gibt keine let statements
- In java kann ich die lets nur in bestimmter Weise einbauen. Die ANF Transformation macht aus TamedFJ das letFJ
- constraints nicht zu früh erwähnen
- informal erwähnen. um capture conversion zu behandeln braucht es neue constraints
- ganz vorne auflisten. Capture Conversion ist eine Neuheit
Figure 4 und 5 in ein Bild
- man könnte die syntax unterlegen und sagen die unterlegten elemente fallen weg
- in beiden Syntaxen die Methodendeklarationen sollen gleich sein. beides return benutzen
- anschließend bei der convertierung zu TamedFJ nur die Änderungen beschreiben (Änderungen nur in Expressions)

1914
unify.tex
View File

File diff suppressed because it is too large Load Diff