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

Add Capture Constraint are not reflexive explanation

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-05-15 23:58:52 +02:00
parent 9e0d9ddd18
commit 1fd7c56391
7 changed files with 94 additions and 92 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
conclusion.tex
View File

@ -120,7 +120,7 @@ The problems introduced in the openening \ref{challenges} can be solved via our
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 proof soundness and completeness for \unify{}.
Going further we try to prove soundness and completeness for \unify{}.
% The tricks are:

53
constraints.tex
View File

@ -1,3 +1,56 @@
\section{Capture Constraints}
%TODO: General Capture Constraint explanation
Capture Constraints are not reflexive.
This is necessary to solve challenge \ref{challenge:1}.
A capture constraint is bound to a specific let statement.
For example the statement \lstinline{let x = v in x.get()}
generates a constraint like $\tv{x} \lessdotCC \exptype{List}{\wtv{a}}$.
This means that the type variable $\tv{x}$ on the left side of the capture constraint is actually a placeholder
for a type that is subject to capture conversion.
It is possible that two syntactically equal capture constraints evolve
during constraint generation or the \unify{} process.
Take the two constraints in listing \ref{lst:sameConstraints}
which originate from the \texttt{concat} method invocation in listing \ref{lst:faultyConcat} for example.
To illustrate their connection to a let statement each capture constraint is annoted with its respective variable.
After a capture conversion step the constraints become
$\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}},
\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}
$
making obvious that this constraint set is unsolvable.
\textit{Note:}
In the special case \lstinline{let x = v in concat(x,x)} the constraint 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}).
In this paper we do not annotate capture constraint with their source let statement.
Instead we consider every capture constraint as distinct to other constraints even when syntactically the same,
because we know that each capture constraint 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.
\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]
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{y} \exptype{List}{\wtv{a}}$
\end{lstlisting}
\end{minipage}
\end{figure}
\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.

74
introduction.tex
View File

@ -16,6 +16,12 @@ Type inference for Java has many use cases and could be used to help programmers
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.
We propose a global type inference algorithm for Java supporting Wildcards and proven sound.
Global type inference allows input programs without any type annotations.
A programmer could write Java code without stressing about types and type annotations which
are infered and inserted by our algorithm.
%This leads to better types (Poster referenz)
%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}.
@ -47,7 +53,7 @@ Also the transformation steps of the \unify{} algorithm are directly related to
\item[Java Type Inference]
Standard Java provides type inference in a restricted form % namely {Local Type Inference}.
which only works for local environments where the surrounding context has knwon types.
which only works for local environments where the surrounding context has known types.
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.
In listing \ref{lst:tiExample} the method call \texttt{emptyList} is missing
@ -113,7 +119,7 @@ We present a novel approach to deal with existential types and capture conversio
\item The algorithm is split in two parts. A constraint generation step and an unification step.
Input language and constraint generations can be extended without altering the unification part.
\item
We proof soundness and aim for a good compromise between completeness and time complexity.
We prove soundness and aim for a good compromise between completeness and time complexity.
\end{itemize}
% Our algorithm finds a correct type solution for the following example, where the Java local type inference fails:
% \begin{verbatim}
@ -253,7 +259,7 @@ but there exists some unknown type $\exptype{List}{\rwildcard{A}}$, with $\rwild
\texttt{Object}.
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}.
Polymorphic method calls need to be wraped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
Polymorphic method calls need to be wrapped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
In Java this is done implicitly in a process called capture conversion (as proposed in Wild FJ \cite{WildFJ}).
\begin{figure}
@ -360,6 +366,19 @@ A subtype constraint is satisfied if the left side is a subtype of the right sid
Subtype constraints and type placeholders act the same as the ones used in \emph{Type Inference for Featherweight Generic Java} \cite{TIforFGJ}.
The novel capture constraints and wildcard placeholders are needed for method invocations involving wildcards.
Our \unify{} process uses a similar concept as the standard unification by Martelli and Montanari \cite{MM82},
consisting of terms, relations and variables.
Instead of terms we have types of the form $\exptype{C}{\ol{T}}$ and
the variables are called type placeholders.
The input consist out of subtype relations.
The goal is to find a solution (an unifier) which is a substitution for type placeholders
which satisfies all input subtype constraints.
Types are reduced until they %either reach a discrepancy like $\type{String} \doteq \type{Integer}$
reach a form like $\tv{a} \doteq \type{T}$.
Afterwards \unify{} substitutes type placeholder $\tv{a}$ with $\type{T}$.
This is done until a substitution for all type placeholders and therefore a valid solution is reached.
The reduction and substitutions are done in the first step of the algorithm.
\begin{recap}\textbf{TI for FGJ without Wildcards:}
\TFGJ{} generates subtype constraints $(\type{T} \lessdot \type{T})$ consisting of named types and type placeholders.
For example the method invocation \texttt{concat(l, new Object())} generates the constraints
@ -433,53 +452,6 @@ $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
There is no solution for the subtype constraint:
$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$
% No capture conversion for methods in the same class:
% Given two methods without type annotations like
% \begin{verbatim}
% // m :: () -> r
% m() = new List<String>() :? new List<Integer>();
% // id :: (a) -> a
% id(a) = a
% \end{verbatim}
% and a method call \texttt{id(m())} would lead to the constraints:
% $\exptype{List}{\type{String}} \lessdot \ntv{r},
% \exptype{List}{\type{Integer}} \lessdot \ntv{r},
% \ntv{r} \lessdotCC \ntv{a}$
% In this example capture conversion is not applicable,
% because the \texttt{id} method is not polymorphic.
% The type solution provided by \unify{} for this constraint set is:
% $\sigma(\ntv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}},
% \sigma(\ntv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$
% \begin{verbatim}
% List<?> m() = new List<String>() :? new List<Integer>();
% List<?> id(List<?> a) = a
% \end{verbatim}
% The following example has the \texttt{id} method already typed and the method \texttt{m}
% extended by a recursive call \texttt{id(m())}:
% \begin{verbatim}
% <A> List<A> id(List<A> a) = a
% m() = new List<String>() :? new List<Integer>() :? id(m());
% \end{verbatim}
% Now the constraints make use of a $\lessdotCC$ constraint:
% $\exptype{List}{\type{String}} \lessdot \ntv{r},
% \exptype{List}{\type{Integer}} \lessdot \ntv{r},
% \ntv{r} \lessdotCC \exptype{List}{\wtv{a}}$
% After substituting $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\ntv{r}$ like in the example before
% we get the constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$.
% Due to the $\lessdotCC$ \unify{} is allowed to perform a capture conversion yielding
% $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
% \textit{Note:} The wildcard placeholder $\wtv{a}$ is allowed to hold free variables whereas a normal placeholder like $\ntv{r}$
% is never assigned a type containing free variables.
% Therefore \unify{} sets $\wtv{a} \doteq \rwildcard{X}$, completing the constraint set and resulting in the type solution:
% \begin{verbatim}
% List<?> m() = new List<String>() :? new List<Integer>() :? id(m());
% \end{verbatim}
\subsection{Challenges}\label{challenges}
%TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
@ -498,7 +470,7 @@ A problem arises when replacing type variables with wildcards.
Lets have a look at a few challenges:
\begin{itemize}
\item
\item \label{challenge:1}
One challenge is to design the algorithm in a way that it finds a correct solution for the program shown in listing \ref{lst:addExample}
and rejects the program in listing \ref{lst:concatError}.
The first one is a valid Java program,

5
prolog.tex
View File

@ -11,11 +11,16 @@
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}

2
soundness.tex
View File

@ -152,7 +152,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 proofing every substitution in Unify is ok aslong as every type in the inputs is ok
% by proving 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

2
tRules.tex
View File

@ -35,7 +35,7 @@ Our algorithm is designed for extensibility with the final goal of full support
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
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.

48
unify.tex
View File

@ -175,7 +175,7 @@ and $\wctype{\wildcard{Y}{\type{Object}}{\tv{String}}}{List}{\rwildcard{Y}} \les
We define two types as equal if they are mutual subtypes of each other.
%This relation is symmetric, reflexive and transitive by the definition of subtyping.
%This definition is sufficient for proofing soundness.
%This definition is sufficient for proving soundness.
\begin{definition}{Type Equality:}\label{def:equal}
$\Delta \vdash \type{S} = \type{T}$ if $\Delta \vdash \type{T} <: \type{S}$ and $\Delta \vdash \type{T} <: \type{S}$
\end{definition}
@ -279,34 +279,15 @@ The normal type placeholder $\ntv{r}$ has to be replaced by a type without free
%\newcommand{\tw}[1]{\tv{#1}_?}
\begin{description}
\item[Input:] An environment $\Delta'$
and a set of constraints $C = \set{ \type{T} \lessdot \type{T}, \type{T} \doteq \type{T} \ldots}$
and a list of constraints $C' = \set{ \type{T} \lessdotCC \type{T}}$.
The input constraints must be of the following format:
\begin{tabular}{lcll}
$c $ &$::=$ & $\type{T} \lessdot \type{T}, \type{T} \lessdotCC \type{T}$ & Constraint \\
$\type{T}, \type{U}, \type{L} $ & $::=$ & $\ntv{a} \mid \wtv{a} \mid \ntype{N}$ & Type variable or Wildcard Variable or Type \\
$\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\overline{\wildcard{X}{U}{L}}}{C}{\ol{T}} $ & Class Type \\
\end{tabular}\\[0.5em]
and a set of constraints $C = \set{ \type{T} \lessdot \type{T}, \type{T} \lessdotCC \type{T}, \type{T} \doteq \type{T} \ldots}$
\item[Output:]
Set of unifiers $Uni = \set{\sigma_1, \ldots, \sigma_n}$ and an environment $\Delta$
\end{description}
The \unify{} algorithm internally uses the following data types:
\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}
The algorithm is split into multiple parts:
Each calculation step of the algorithm is expressed as a transformation rule.
% TODO: Explain syntax of the transformation steps
The transformation steps are not applied all at once but in a specific order:
\begin{description}
\item[Step 1:]
Apply the rules depicted in the figures \ref{fig:normalizing-rules}, \ref{fig:reduce-rules} and \ref{fig:wildcard-rules} exhaustively,
@ -1371,23 +1352,13 @@ $
\caption{Type Reduction rules}\label{fig:reductionRules}
\end{figure}
\subsection{Explanation}
Our \unify{} process uses a similar concept to the standard unification by Martelli and Montanari \cite{MM82},
consisting of terms, relations and variables.
Instead of terms we have types of the form $\exptype{C}{\ol{T}}$ and
the variables are called type placeholders.
The input consist out of subtype relations.
The goal is to find a solution (an unifier) which is a substitution for type placeholders
which satisfies all input subtype constraints.
Types are reduced until they %either reach a discrepancy like $\type{String} \doteq \type{Integer}$
reach a form like $\tv{a} \doteq \type{T}$.
Afterwards \unify{} substitutes type placeholder $\tv{a}$ with $\type{T}$.
This is done until a substitution for all type placeholders and therefore a valid solution is reached.
The reduction and substitutions are done in the first step of the algorithm.
\subsection{Explanations}
%The type reduction is done by the rules in figure \ref{fig:reductionRules}
\begin{description}
\item[Prepare]
The \rulename{Prepare} transformation is always applied together with the \rulename{Reduce} transformation.
\unify{} cannot reduce constraints without checking a few prerequisites.
Take the constraint $\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdot \exptype{C}{\wtv{a}}$ for example.
If we apply a reduction here we get $\rwildcard{X} \doteq \wtv{a}$.
@ -1399,6 +1370,7 @@ Therefore the \rulename{Reduce} rule only reduces constraints where the left sid
But if the right side neither contains wildcard type placeholders nor free variables the constraint can be reduced anyways.
The \rulename{Prepare} rule then converts this constraint to a capture constraint.
Afterwards the \rulename{Capture} rule removes the wildcard declarations on the left side an the constraint can be reduced.
\end{description}
\textit{Example} of the type reduction rules in figure \ref{fig:reductionRules} with the input
$\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$