Cleanup and add Introduction
This commit is contained in:
JanUlrich
parent
514097ce56
commit
ac3e5651e3
480
aspUnify.tex
480
aspUnify.tex
@ -64,50 +64,43 @@ In this paper we translate the type inference algorithm for Featherweight Generi
|
||||
Answer Set Program.
|
||||
Answer Set Programming (ASP) promises to solve complex computational search problems
|
||||
as long as they are finite domain.
|
||||
This paper shows that it is possible to implement global type inference for FGJ as an ASP program.
|
||||
This paper shows that it is possible to implement global type inference for Featherweight Generic Java (FGJ) as an ASP program.
|
||||
Afterwards we compared the ASP implementation with our own implementation in Java
|
||||
exposing promising results.
|
||||
% We also show soundness, completeness and termination for our ASP implementation.
|
||||
Another advantage is that the specification of the algorithm can be translated one on one to ASP code
|
||||
leading to less errors in the respective implementation.
|
||||
Unfortunately ASP can only be used for type inference for a subset of the Java type system that excludes wildcard types.
|
||||
%TODO: Is this correct?
|
||||
\end{abstract}
|
||||
%
|
||||
%
|
||||
%
|
||||
\section{Type Inference}
|
||||
Every major typed programming language uses some form of type inference.
|
||||
Rust, Java, C++, Haskell, etc... %(see: https://en.wikipedia.org/wiki/Type_inference)
|
||||
Type inference adds alot of value to a programming language.
|
||||
\begin{itemize}
|
||||
\item Code is more readable.
|
||||
\item Type inference usually does a better job at finding types than a programmer.
|
||||
\item Type inference can use types that are not denotable by the programmer.
|
||||
\item Better reusability.
|
||||
\item Allows for faster development and the programmer to focus on the actual task instead of struggling with the type system.
|
||||
\end{itemize}
|
||||
\section{Global Type Inference}
|
||||
% Every major typed programming language uses some form of type inference.
|
||||
% Rust, Java, C++, Haskell, etc... %(see: https://en.wikipedia.org/wiki/Type_inference)
|
||||
% Type inference adds alot of value to a programming language.
|
||||
% \begin{itemize}
|
||||
% \item Code is more readable.
|
||||
% \item Type inference usually does a better job at finding types than a programmer.
|
||||
% \item Type inference can use types that are not denotable by the programmer.
|
||||
% \item Better reusability.
|
||||
% \item Allows for faster development and the programmer to focus on the actual task instead of struggling with the type system.
|
||||
% \end{itemize}
|
||||
|
||||
Java has adopted more and more type inference features over time.
|
||||
%TODO: list type inference additions
|
||||
Currently Java only has local type inference.
|
||||
We want to bring type inference for Java to the next level.
|
||||
% Java has adopted more and more type inference features over time.
|
||||
% %TODO: list type inference additions
|
||||
% Currently Java only has local type inference.
|
||||
% We want to bring type inference for Java to the next level.
|
||||
|
||||
Our type inference algorithms for Java are described in a formal manner in
|
||||
\cite{MartinUnify}, \cite{TIforGFJ}.
|
||||
The first prototype implementation put the focus on a correct implementation rather than
|
||||
fast execution times.
|
||||
These programs tend to be in exponential time upper bounded by the amount of ambiguous method calls and subtype relations.
|
||||
%TODO: Example with multiple calls to m.toString(). All possibilities are checked in a naive implementation!
|
||||
Java is a strictly typed programming language.
|
||||
The current versions come with a local type inference feature that allows the programmer to omit
|
||||
type annotations in some places like argument types of lambda expressions for example.
|
||||
But methods still have to be fully typed including argument and return types.
|
||||
We work at a global type inference algorithm for Java which is able to compute correct types
|
||||
for a Java program with no type annotations at all.
|
||||
|
||||
\section{Motivation}
|
||||
The nature of the global type inference algorithm causes the search space of the unification algorithm to
|
||||
increase exponentially.
|
||||
Java allows overloaded methods causing our type inference algorithm to create so called Or-Constraints.
|
||||
This can also happen if multiple classes implement a method with the same name and the same amount of parameters.
|
||||
Given the following input program we do not know, which method \texttt{self} is meant for the method call
|
||||
\texttt{var.self()}, because there is no type annotation for \texttt{var}.
|
||||
|
||||
|
||||
%\begin{figure}[h]
|
||||
%\begin{minipage}{0.49\textwidth}
|
||||
\begin{figure}[h]
|
||||
\begin{lstlisting}
|
||||
class C1 {
|
||||
C1 self(){
|
||||
@ -121,10 +114,45 @@ class C2 {
|
||||
}
|
||||
class Example {
|
||||
untypedMethod(var){
|
||||
return var.self(); (*@$\implies \set{\tv{var} \lessdot \type{C1}, \tv{ret} \doteq \type{C1} }\ ||\ \set{\tv{var} \lessdot \type{C2}, \tv{ret} \doteq \type{C2}}$@*)
|
||||
return var.self(); // (*@$\implies \set{\tv{var} \lessdot \type{C1}, \tv{ret} \doteq \type{C1} }\ ||\ \set{\tv{var} \lessdot \type{C2}, \tv{ret} \doteq \type{C2}}$@*)
|
||||
}
|
||||
}
|
||||
\end{lstlisting}
|
||||
\caption{Java program missing type annotations}\label{fig:introExample}
|
||||
\end{figure}
|
||||
|
||||
A possible input for our algorithm is shonw in figure \ref{fig:introExample}.
|
||||
Here the method \texttt{untypedMethod} is missing its argument type for \texttt{var} and its return type.
|
||||
Global type inference works in two steps.
|
||||
First we generate a set of subtype constraints, which are later unified resulting in a type solution consisting of type unifiers $\sigma$.
|
||||
Every missing type is replaced by a type placeholder.
|
||||
In this example the type placeholder $\tv{var}$ is a placeholder for the type of the \texttt{var} variable.
|
||||
The $\tv{ret}$ placeholder represents the return type of the \texttt{untypedMethod} method.
|
||||
Also shown as a comment behind the respective method call.
|
||||
There are two types of type constraints.
|
||||
A subtype constraint like $\tv{var} \lessdot \type{C1}$ meaning that the unification algorithm has to find
|
||||
a type replacement for $\tv{var}$ which is a subtype of $\type{C1}$.
|
||||
Due to the Java type system being reflexive one possible solution would be $\sigma(\tv{var}) = \type{C1}$.
|
||||
A constraint $\tv{var} \doteq \type{C1}$ directly results in $\sigma(\tv{ret}) = \type{C1}$.
|
||||
|
||||
Our type inference algorithms for Java are described in a formal manner in
|
||||
\cite{MartinUnify}, \cite{TIforGFJ}.
|
||||
The first prototype implementation put the focus on a correct implementation rather than
|
||||
fast execution times.
|
||||
Depending on the input it currently takes upto several minutes or even days to compute all or even one possible type solution.
|
||||
To make them usable in practice we now focus on decreasing the runtime to a feasible level.
|
||||
|
||||
\section{Motivation}
|
||||
The nature of the global type inference algorithm causes the search space of the unification algorithm to
|
||||
increase exponentially with every ambiguous method call.
|
||||
Java allows overloaded methods causing our type inference algorithm to create so called Or-Constraints.
|
||||
This happens if multiple classes implement a method with the same name and the same amount of parameters.
|
||||
Given the input program in figure \ref{fig:introExample} we do not know, which method \texttt{self} is meant for the method call
|
||||
\texttt{var.self()}, because there is no type annotation for \texttt{var}.
|
||||
|
||||
|
||||
%\begin{figure}[h]
|
||||
%\begin{minipage}{0.49\textwidth}
|
||||
% \end{minipage}%
|
||||
% \hfill
|
||||
% \begin{minipage}{0.49\textwidth}
|
||||
@ -138,8 +166,6 @@ class Example {
|
||||
An Or-Constraint like $\set{\tv{var} \lessdot \type{C1}, \tv{ret} \doteq \type{C1} }\ ||\ \set{\tv{var} \lessdot \type{C2}, \tv{ret} \doteq \type{C2}}$
|
||||
means that either the the constraint set $\set{\tv{var} \lessdot \type{C1}, \tv{ret} \doteq \type{C1} }$
|
||||
or $\set{\tv{var} \lessdot \type{C2}, \tv{ret} \doteq \type{C2}}$ has to be satisfied.
|
||||
In this example the type placeholder $\tv{var}$ is a placeholder for the type of the \texttt{var} variable.
|
||||
The $\tv{ret}$ placeholder represents the return type of the \texttt{untypedMethod} method.
|
||||
If we set the type of \texttt{var} to \texttt{C1}, then the return type of the method will be \texttt{C1} aswell.
|
||||
If we set it to \texttt{C2} then also the return type will be \texttt{C2}.
|
||||
There are two possibilities therefore the Or-Constraint.
|
||||
@ -149,11 +175,14 @@ The type unification algorithm \unify{} only sees the supplied constraints and h
|
||||
This is proven in \cite{TIforGFJ} and is the reason why type inference for Featherweight Generic Java is NP-hard.
|
||||
Let's have a look at the following alternation of our example:
|
||||
|
||||
\begin{figure}[h]
|
||||
\begin{lstlisting}
|
||||
untypedMethod(var){
|
||||
return var.self().self().self().self();
|
||||
}
|
||||
\end{lstlisting}
|
||||
\caption{Stacked ambiguous method calls}\label{fig:benchmark}
|
||||
\end{figure}
|
||||
|
||||
Now there are four chained method calls leading to four Or-Constraints:
|
||||
\begin{align*}
|
||||
@ -184,8 +213,29 @@ Answer Set programming promises to solve complex search problems in a highly opt
|
||||
The idea in this paper is to implement the algorithm presented in \cite{TIforGFJ}
|
||||
as an ASP program and see how well it handles our type unification problem.
|
||||
|
||||
\section{ASP Implementation}
|
||||
|
||||
\section{Subtyping}
|
||||
Our ASP implementation replaces the unification step of the type inference algorithm.
|
||||
So the input is a set of constraints $c$ and the output is a set of unifiers $\sigma$.
|
||||
An ASP program consists of implication rules and facts.
|
||||
Here the facts are the input constraints and the rules are the ones depicted in chapter \ref{sec:implicationRules}.
|
||||
After running the resulting program through an interpreter the output
|
||||
holds the desired $\sigma(\tv{a}) = \type{T}$ literals.
|
||||
|
||||
\begin{figure}[h]
|
||||
\center
|
||||
\begin{tabular}{lcll}
|
||||
$c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
|
||||
$\type{T} $ & $::=$ & $\tv{a} \mid \type{N}$ & Type placeholder or Type \\
|
||||
$\ntype{N}$ & $::=$ & $\exptype{C}{\ol{T}}$ & Class Type containing type placeholders\\
|
||||
$\gtype{G}$ & $::=$ & $\exptype{C}{\ol{G}}$ & Class Type not containing type placeholders \\
|
||||
\end{tabular}
|
||||
\caption{Syntax of types and constraints}
|
||||
\label{fig:syntax-constraints}
|
||||
\end{figure}
|
||||
|
||||
%\subsection{Subtyping}
|
||||
\begin{figure}[h]
|
||||
\begin{mathpar}
|
||||
\inferrule[S-Refl]{}{
|
||||
\type{T} <: \type{T}
|
||||
@ -201,7 +251,6 @@ as an ASP program and see how well it handles our type unification problem.
|
||||
\exptype{C}{\ol{T}} <: [\ol{T}/\ol{X}]\type{N}
|
||||
}
|
||||
\end{mathpar}
|
||||
|
||||
\begin{mathpar}
|
||||
\inferrule[N-Refl]{}{
|
||||
\type{C} << \type{C}
|
||||
@ -215,19 +264,21 @@ as an ASP program and see how well it handles our type unification problem.
|
||||
\type{C} << \type{D}
|
||||
}
|
||||
\end{mathpar}
|
||||
\caption{Subtyping}\label{fig:subtyping}
|
||||
\end{figure}
|
||||
|
||||
|
||||
%Subtyping has no bounds for generic type parameters.
|
||||
% but this is propably not needed
|
||||
|
||||
\section{Unify}
|
||||
Input: Every type placeholder must have an upper bound.
|
||||
Output: Every $\tv{a} \lessdot \type{T}$ constraint gets a
|
||||
\subsection{Unification Algorithm}\label{sec:implicationRules}
|
||||
|
||||
The $\tv{a} \lessdot \type{Object}$ rule has to be ensured by the incoming constraints.
|
||||
The need to have an upper bound to every type placeholder.
|
||||
|
||||
We have to formulate the unification algorithm with implication rules.
|
||||
Those can be directly translated to ASP.
|
||||
All the implication rules depicted in this chapter can be translated to ASP statements
|
||||
described in chapter \ref{sec:translation}.
|
||||
|
||||
\label{sec:implicationRules}
|
||||
\begin{mathpar}
|
||||
\inferrule[Subst-L]{
|
||||
@ -432,16 +483,18 @@ Fail:
|
||||
|
||||
The algorithm terminates if every type placeholder in the input constraint set has an assigned type.
|
||||
|
||||
\section{ASP Encoding}
|
||||
The implication rules defined in chapter \ref{sec:implicationRules} can be translated to an ASP program.
|
||||
|
||||
\begin{tabular}{l | r}
|
||||
$\tv{a}$ & \texttt{tph("a")}\\
|
||||
$\exptype{C}{}$ & \texttt{type("C", null)}\\
|
||||
$\exptype{C}{\ol{X}}$ & \texttt{type("C", params(\ldots))}\\
|
||||
|
||||
\end{tabular}
|
||||
\section{ASP Encoding}\label{sec:translation}
|
||||
\newcommand{\aspify}{\nabla}
|
||||
The implication rules defined in chapter \ref{sec:implicationRules} can be translated to an ASP program
|
||||
(see figure \ref{fig:aspTransformationRules}).
|
||||
|
||||
% \begin{tabular}{l | r}
|
||||
% $\tv{a}$ & \texttt{tph("a")}\\
|
||||
% $\exptype{C}{}$ & \texttt{type("C", null)}\\
|
||||
% $\exptype{C}{\ol{X}}$ & \texttt{type("C", params(\ldots))}\\
|
||||
% \end{tabular}
|
||||
|
||||
\begin{figure}[h]
|
||||
\begin{align*}
|
||||
\aspify(\tv{a}) =& \texttt{tph("a")}\\
|
||||
\exptype{C}{} =& \texttt{type("C", null)}\\
|
||||
@ -454,186 +507,207 @@ The implication rules defined in chapter \ref{sec:implicationRules} can be trans
|
||||
c
|
||||
}\right) =& \aspify(c)\ \texttt{:-} \aspify(c_1), \aspify(c_2)
|
||||
\end{align*}
|
||||
\caption{Transformation to ASP code}\label{fig:aspTransformationRules}
|
||||
\end{figure}
|
||||
|
||||
The S-Class rule contains a substitution and has to be encoded with variables.
|
||||
%The $\aspify{}$ function converts our formal specification of the algorithm to ASP code.
|
||||
|
||||
This also has to be done for the subtype rules in figure \ref{fig:subtyping}.
|
||||
There the S-Class rule needs special handling because it contains a substitution.
|
||||
It has to be encoded using variables.
|
||||
Given a extends relation $\texttt{class}\ \exptype{C}{\type{X}} \triangleleft \exptype{D}{\type{X}}$
|
||||
we generate the ASP code:\\
|
||||
{\small{\texttt{subtype(type("C", params(X)), type("D", params(X))) :- subtype(type("C", params(X))).}}}
|
||||
|
||||
Capital letters like \texttt{X} are variables in ASP and the former statement causes any
|
||||
literal like \texttt{subtype(type("C", params(tph("a"))))} leads to the literal
|
||||
literal like \texttt{subtype(type("C", params(tph("a"))))} to imply the literal
|
||||
\texttt{subtype(type("C", params(tph("a"))), type("D", params(tph("a"))))}.
|
||||
|
||||
|
||||
\section{Proofs}
|
||||
\begin{lemma}{Substitution:}
|
||||
For every $\tv{a} \doteq \type{T}$ and every constraint $c$,
|
||||
there also exists a constraint $[\type{T}/\tv{a}]c$.
|
||||
% \section{Proofs}
|
||||
% \begin{lemma}{Substitution:}
|
||||
% For every $\tv{a} \doteq \type{T}$ and every constraint $c$,
|
||||
% there also exists a constraint $[\type{T}/\tv{a}]c$.
|
||||
|
||||
\noindent
|
||||
\normalfont
|
||||
This lemma proofs that equal constraints lead to a substitution in every other constraint.
|
||||
For exmaple $\tv{b} \doteq \type{String}$ and $\tv{b} \lessdot \exptype{Comparable}{\tv{b}}$
|
||||
lead to a constraint $\type{String} \lessdot \exptype{Comparable}{\type{String}}$
|
||||
\end{lemma}
|
||||
\textit{Proof:}
|
||||
% \noindent
|
||||
% \normalfont
|
||||
% This lemma proofs that equal constraints lead to a substitution in every other constraint.
|
||||
% For exmaple $\tv{b} \doteq \type{String}$ and $\tv{b} \lessdot \exptype{Comparable}{\tv{b}}$
|
||||
% lead to a constraint $\type{String} \lessdot \exptype{Comparable}{\type{String}}$
|
||||
% \end{lemma}
|
||||
% \textit{Proof:}
|
||||
% %TODO
|
||||
|
||||
% \section{Termination}
|
||||
|
||||
% The amount of different constraints is limited by the maximum amount of encapsulated generics.
|
||||
% The only part that is able to add an additional nesting is the Subst-Param rule.
|
||||
% Here a type placeholder inside a type parameter list is replaced by another type which possibly adds
|
||||
% another layer of nesting but it also removes one type placeholder.
|
||||
|
||||
% There must be one substitution that does not add another type placeholder.
|
||||
% Otherwise there has to be a loop and this woul lead to an incorrect constraint set due to the Fail-Sigma rule.
|
||||
|
||||
% The Subst-Param rule can only be applied a finite number of times.
|
||||
% Due to the substitution lemma and the Sigma-Fail rule the Subst-Param rule can only be applied once per type placeholder.
|
||||
|
||||
% The Subst-Param rule can only be applied once per type placeholder.
|
||||
% If $\type{T} \doteq \exptype{C}{\tv{a}}$ is substituted to $\type{T} \doteq \exptype{C}{\type{N}}$
|
||||
% then there is no $\tv{a} \in \type{N}$.
|
||||
|
||||
% \section{Completeness}
|
||||
% To proof completeness we have to show that every type can be replaced by a placeholder in a correct constraint set.
|
||||
|
||||
% Completeness -> we never exclude a solution
|
||||
% Following constraints stay: $\tv{a} \lessdot \type{T}$ if $\tv{a}$ is never on a right side of another constraint.
|
||||
% Every other type placeholder will be reduced to $\tv{a} \doteq \type{T}$, if there is a solution.
|
||||
% Proof:
|
||||
% %Induction over every possible constraint variation:
|
||||
% a =. T -> induction start
|
||||
% a <. T -> if no other constraint then it can stay otherwise there is either a =. T or a <. T
|
||||
% in latter case: a <. T, a <. T'
|
||||
|
||||
% Proof that every type can be replaced by a Type Placeholder.
|
||||
% % Whats with a =. T, can T be replaced by a Type Placeholder?
|
||||
% % What is our finish condition? a <. T constraints stay, a =. b constraints stay.
|
||||
% % Algorithm does not fail -> \emptyset if a solution exists
|
||||
% % Otherwise there exists a substitution. If the algorithm succeeds we have to pick one of the possible solutions
|
||||
% % by: a <. T -> a =.T
|
||||
% % a =. b, b =. T -> use the solution generation from other paper
|
||||
% % TODO: try to include solution generation in the algorithm and proof that this solution is valid and will always occur as long as there is a solution
|
||||
|
||||
% Soundness -> we never make a wrong implication
|
||||
% %$\tv{a} \doteq \type{T}$ means that $\[type{T}/\tv{a}]C$ is correct
|
||||
% If it succeeds then we can substitute all $\tv{a} \doteq \type{T}$
|
||||
% constraints in the original constraint set and
|
||||
% there exists a typing for the remaining type placeholders
|
||||
% so that the constraint set is satisfied.
|
||||
|
||||
% \begin{theorem}{Soundness}\label{lemma:soundness}
|
||||
% if $\type{T} \lessdot \type{T'}$ and $\sigma(\tv{a}) = \type{N}$
|
||||
% then $[\type{N}/\tv{a}]\type{T} <: [\type{N}/\tv{a}]\type{T'}$.
|
||||
% \end{theorem}
|
||||
|
||||
% \SetEnumitemKey{ncases}{itemindent=!,before=\let\makelabel\ncasesmakelabel}
|
||||
% \newcommand*\ncasesmakelabel[1]{Case #1}
|
||||
|
||||
% \newenvironment{subproof}
|
||||
% {\def\proofname{Subproof}%
|
||||
% \def\qedsymbol{$\triangleleft$}%
|
||||
% \proof}
|
||||
% {\endproof}
|
||||
% Due to Match there must be $\type{N}_1 \lessdot \type{N}_2 \ldots \lessdot \type{N}_n$
|
||||
% \begin{proof}
|
||||
% \begin{enumerate}[ncases]
|
||||
% \item $\tv{a} \lessdot \exptype{C}{\ol{T}}$.
|
||||
% Solution-Sub
|
||||
% Let $\sigma(\tv{a}) = \type{N}$. Then $\type{N} <: \exptype{C}{[\type{N}/\tv{a}]}$
|
||||
% \item $\tv{a} \doteq \type{N}$.
|
||||
% Solution
|
||||
% \item $\tv{a} \lessdot \tv{b}$.
|
||||
% There must be a $\tv{a} \lessdot \type{N}$
|
||||
% \begin{subproof}
|
||||
% $\sigma(\tv{a}) = \type{Object}$,
|
||||
% $\sigma(\tv{b}) = \type{Object}$.
|
||||
% \end{subproof}
|
||||
% \item $\type{N} \lessdot \tv{a}$.
|
||||
% \begin{subproof}
|
||||
% $2$
|
||||
% \end{subproof}
|
||||
% \end{enumerate}
|
||||
% And more text.
|
||||
% \end{proof}
|
||||
|
||||
% \begin{lemma}{Substitution}
|
||||
% \begin{description}
|
||||
% \item[If] $\tv{a} \doteq \type{N}$ with $\tv{a} \neq \type{N}$
|
||||
% \item[Then] for every $\type{T} \doteq \type{T}$ there exists a $[\type{N}/\tv{a}]\type{T} \doteq [\type{N}/\tv{a}]\type{T}$
|
||||
% \item[Then] for every $\type{T} \lessdot \type{T}$ there exists a $[\type{N}/\tv{a}]\type{T} \lessdot [\type{N}/\tv{a}]\type{T}$
|
||||
% \end{description}
|
||||
% \end{lemma}
|
||||
% \textit{Proof:}
|
||||
% TODO
|
||||
|
||||
\section{Termination}
|
||||
% \begin{lemma} \label{lemma:subtypeOnly}
|
||||
% If $\sigma(\tv{a}) = \emptyset$ then $\tv{a}$ appears only on the left side of $\tv{a} \lessdot \type{T}$ constraints.
|
||||
% \end{lemma}
|
||||
% Proof:
|
||||
% Every type placeholder gets a solution, because there must be atleast one $\tv{a} \lessdot \type{N}$ constraint.
|
||||
% Then either the Solution-Sub generates a $\sigma$ or the Solution rule can be used TODO: Proof.
|
||||
|
||||
The amount of different constraints is limited by the maximum amount of encapsulated generics.
|
||||
The only part that is able to add an additional nesting is the Subst-Param rule.
|
||||
Here a type placeholder inside a type parameter list is replaced by another type which possibly adds
|
||||
another layer of nesting but it also removes one type placeholder.
|
||||
% The Solution-Sub rule is always correct.
|
||||
|
||||
There must be one substitution that does not add another type placeholder.
|
||||
Otherwise there has to be a loop and this woul lead to an incorrect constraint set due to the Fail-Sigma rule.
|
||||
% Proof:
|
||||
|
||||
The Subst-Param rule can only be applied a finite number of times.
|
||||
Due to the substitution lemma and the Sigma-Fail rule the Subst-Param rule can only be applied once per type placeholder.
|
||||
% \begin{theorem}{Termination}
|
||||
% %jede nichtendliche Menge von Constraints bleibt endlich. Die Regeln können nicht unendlich oft angewendet werden
|
||||
% %Trivial. The only possibility would be if we allow a =. C<a> constraints!
|
||||
% \end{theorem}
|
||||
|
||||
The Subst-Param rule can only be applied once per type placeholder.
|
||||
If $\type{T} \doteq \exptype{C}{\tv{a}}$ is substituted to $\type{T} \doteq \exptype{C}{\type{N}}$
|
||||
then there is no $\tv{a} \in \type{N}$.
|
||||
% TODO: For completeness we have to proof that not $\tv{a} \doteq \type{N}$ only is the case if $\tv{a}$ only appears on the left side of $\tv{a} \lessdot \type{T}$ constraints.
|
||||
% Problem: a <. List<a>
|
||||
% a <. List<b>
|
||||
% then a =. b
|
||||
% Solution: Keep the a <. N constraints and apply the Step 6 from the GTFGJ paper.
|
||||
% Then we have to proof that only a <. N constraints remain with sigma(a) = empty. Or Fail
|
||||
|
||||
\section{Completeness}
|
||||
To proof completeness we have to show that every type can be replaced by a placeholder in a correct constraint set.
|
||||
|
||||
Completeness -> we never exclude a solution
|
||||
Following constraints stay: $\tv{a} \lessdot \type{T}$ if $\tv{a}$ is never on a right side of another constraint.
|
||||
Every other type placeholder will be reduced to $\tv{a} \doteq \type{T}$, if there is a solution.
|
||||
Proof:
|
||||
%Induction over every possible constraint variation:
|
||||
a =. T -> induction start
|
||||
a <. T -> if no other constraint then it can stay otherwise there is either a =. T or a <. T
|
||||
in latter case: a <. T, a <. T'
|
||||
|
||||
Proof that every type can be replaced by a Type Placeholder.
|
||||
% Whats with a =. T, can T be replaced by a Type Placeholder?
|
||||
% What is our finish condition? a <. T constraints stay, a =. b constraints stay.
|
||||
% Algorithm does not fail -> \emptyset if a solution exists
|
||||
% Otherwise there exists a substitution. If the algorithm succeeds we have to pick one of the possible solutions
|
||||
% by: a <. T -> a =.T
|
||||
% a =. b, b =. T -> use the solution generation from other paper
|
||||
% TODO: try to include solution generation in the algorithm and proof that this solution is valid and will always occur as long as there is a solution
|
||||
|
||||
Soundness -> we never make a wrong implication
|
||||
%$\tv{a} \doteq \type{T}$ means that $\[type{T}/\tv{a}]C$ is correct
|
||||
If it succeeds then we can substitute all $\tv{a} \doteq \type{T}$
|
||||
constraints in the original constraint set and
|
||||
there exists a typing for the remaining type placeholders
|
||||
so that the constraint set is satisfied.
|
||||
|
||||
\begin{theorem}{Soundness}\label{lemma:soundness}
|
||||
if $\type{T} \lessdot \type{T'}$ and $\sigma(\tv{a}) = \type{N}$
|
||||
then $[\type{N}/\tv{a}]\type{T} <: [\type{N}/\tv{a}]\type{T'}$.
|
||||
\end{theorem}
|
||||
|
||||
\SetEnumitemKey{ncases}{itemindent=!,before=\let\makelabel\ncasesmakelabel}
|
||||
\newcommand*\ncasesmakelabel[1]{Case #1}
|
||||
|
||||
\newenvironment{subproof}
|
||||
{\def\proofname{Subproof}%
|
||||
\def\qedsymbol{$\triangleleft$}%
|
||||
\proof}
|
||||
{\endproof}
|
||||
Due to Match there must be $\type{N}_1 \lessdot \type{N}_2 \ldots \lessdot \type{N}_n$
|
||||
\begin{proof}
|
||||
\begin{enumerate}[ncases]
|
||||
\item $\tv{a} \lessdot \exptype{C}{\ol{T}}$.
|
||||
Solution-Sub
|
||||
Let $\sigma(\tv{a}) = \type{N}$. Then $\type{N} <: \exptype{C}{[\type{N}/\tv{a}]}$
|
||||
\item $\tv{a} \doteq \type{N}$.
|
||||
Solution
|
||||
\item $\tv{a} \lessdot \tv{b}$.
|
||||
There must be a $\tv{a} \lessdot \type{N}$
|
||||
\begin{subproof}
|
||||
$\sigma(\tv{a}) = \type{Object}$,
|
||||
$\sigma(\tv{b}) = \type{Object}$.
|
||||
\end{subproof}
|
||||
\item $\type{N} \lessdot \tv{a}$.
|
||||
\begin{subproof}
|
||||
$2$
|
||||
\end{subproof}
|
||||
\end{enumerate}
|
||||
And more text.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}{Substitution}
|
||||
\begin{description}
|
||||
\item[If] $\tv{a} \doteq \type{N}$ with $\tv{a} \neq \type{N}$
|
||||
\item[Then] for every $\type{T} \doteq \type{T}$ there exists a $[\type{N}/\tv{a}]\type{T} \doteq [\type{N}/\tv{a}]\type{T}$
|
||||
\item[Then] for every $\type{T} \lessdot \type{T}$ there exists a $[\type{N}/\tv{a}]\type{T} \lessdot [\type{N}/\tv{a}]\type{T}$
|
||||
\end{description}
|
||||
\end{lemma}
|
||||
\textit{Proof:}
|
||||
TODO
|
||||
|
||||
\begin{lemma} \label{lemma:subtypeOnly}
|
||||
If $\sigma(\tv{a}) = \emptyset$ then $\tv{a}$ appears only on the left side of $\tv{a} \lessdot \type{T}$ constraints.
|
||||
\end{lemma}
|
||||
Proof:
|
||||
Every type placeholder gets a solution, because there must be atleast one $\tv{a} \lessdot \type{N}$ constraint.
|
||||
Then either the Solution-Sub generates a $\sigma$ or the Solution rule can be used TODO: Proof.
|
||||
|
||||
The Solution-Sub rule is always correct.
|
||||
|
||||
Proof:
|
||||
|
||||
\begin{theorem}{Termination}
|
||||
%jede nichtendliche Menge von Constraints bleibt endlich. Die Regeln können nicht unendlich oft angewendet werden
|
||||
%Trivial. The only possibility would be if we allow a =. C<a> constraints!
|
||||
\end{theorem}
|
||||
|
||||
TODO: For completeness we have to proof that not $\tv{a} \doteq \type{N}$ only is the case if $\tv{a}$ only appears on the left side of $\tv{a} \lessdot \type{T}$ constraints.
|
||||
Problem: a <. List<a>
|
||||
a <. List<b>
|
||||
then a =. b
|
||||
Solution: Keep the a <. N constraints and apply the Step 6 from the GTFGJ paper.
|
||||
Then we have to proof that only a <. N constraints remain with sigma(a) = empty. Or Fail
|
||||
|
||||
\begin{theorem}{Completeness}
|
||||
$\forall \tv{a} \in C_{input}: \sigma(\tv{a}) = \type{N}$, if there is a solution for $C_{input}$
|
||||
and every type placeholder has an upper bound $\tv{a} \lessdot \type{N}$.
|
||||
\end{theorem}
|
||||
%Problem: We do not support multiple inheritance
|
||||
\begin{proof}
|
||||
\begin{enumerate}[ncases]
|
||||
\item $\tv{a} \lessdot \type{N}$.
|
||||
Solution-Sub
|
||||
\item $\tv{a} \doteq \type{N}$.
|
||||
Solution
|
||||
\item $\tv{a} \lessdot \tv{b}$.
|
||||
There must be a $\tv{a} \lessdot \type{N}$
|
||||
\begin{subproof}
|
||||
$\sigma(\tv{a}) = \type{Object}$,
|
||||
$\sigma(\tv{b}) = \type{Object}$.
|
||||
\end{subproof}
|
||||
\item $\type{N} \lessdot \tv{a}$.
|
||||
\begin{subproof}
|
||||
$2$
|
||||
\end{subproof}
|
||||
\end{enumerate}
|
||||
And more text.
|
||||
\end{proof}
|
||||
% \begin{theorem}{Completeness}
|
||||
% $\forall \tv{a} \in C_{input}: \sigma(\tv{a}) = \type{N}$, if there is a solution for $C_{input}$
|
||||
% and every type placeholder has an upper bound $\tv{a} \lessdot \type{N}$.
|
||||
% \end{theorem}
|
||||
% %Problem: We do not support multiple inheritance
|
||||
% \begin{proof}
|
||||
% \begin{enumerate}[ncases]
|
||||
% \item $\tv{a} \lessdot \type{N}$.
|
||||
% Solution-Sub
|
||||
% \item $\tv{a} \doteq \type{N}$.
|
||||
% Solution
|
||||
% \item $\tv{a} \lessdot \tv{b}$.
|
||||
% There must be a $\tv{a} \lessdot \type{N}$
|
||||
% \begin{subproof}
|
||||
% $\sigma(\tv{a}) = \type{Object}$,
|
||||
% $\sigma(\tv{b}) = \type{Object}$.
|
||||
% \end{subproof}
|
||||
% \item $\type{N} \lessdot \tv{a}$.
|
||||
% \begin{subproof}
|
||||
% $2$
|
||||
% \end{subproof}
|
||||
% \end{enumerate}
|
||||
% And more text.
|
||||
% \end{proof}
|
||||
|
||||
|
||||
\section{Discussion}
|
||||
%\section{Discussion}
|
||||
% We cannot use Datalog, because it cannot solve NP-Hard problems.
|
||||
% See: E. Dantsin, T. Eiter, G. Gottlob, and A. Voronkov. Complexity and Expressive Power of Logic Programming.
|
||||
% ACM Computing Surveys, 33(3):374–425, 2001. Available at
|
||||
% http://www.kr.tuwien.ac.at/staff/eiter/et-archive/
|
||||
% Source: https://www.cs.ox.ac.uk/files/1018/gglecture7.pdf
|
||||
|
||||
It is only possible to implement a type inference algorithm for Java as long as we omit wildcard types.
|
||||
The reason is that subtype checking in Java is turing complete \cite{javaTuringComplete}.
|
||||
It is not possible to implement a type inference algorithm for Java in ASP, because the grounding process will not terminate
|
||||
\cite{kaufmann2016grounding}.
|
||||
|
||||
\section{Outcome and Conclusion}
|
||||
ASP handles Or-Constraints surprisingly well.
|
||||
We tested our ASP implementation of the unification algorithm with the constraints originating from the program in
|
||||
figure \ref{fig:benchmark}.
|
||||
We compared it with the current implementation of the Unification algorithm in Java
|
||||
\footnote{\url{https://gitea.hb.dhbw-stuttgart.de/JavaTX/JavaCompilerCore}}.
|
||||
We increased the complexity by adding more stacked method calls up to ten stacked calls and the interpreter clingo \footnote{\url{https://potassco.org/clingo/}}
|
||||
was still able to handle it easily and finish computation in under 50 milliseconds.
|
||||
By contrast our Java implementation already takes multiple seconds processing time for the same input.
|
||||
|
||||
\section{Future Work}
|
||||
We are using this example for a fair comparision between the two implementations because it does not include generic type parameters causing the unification algorithm
|
||||
not to consider wildcard types.
|
||||
The Java implementation also supports Java wildcard types whereas the ASP implementation does not.
|
||||
%It is only possible to implement a type inference algorithm for Java as long as we omit wildcard types.
|
||||
It is unfortunately not possible to implement the unification algorithm including wildcard support with Answer Set Programming.
|
||||
The reason is that subtype checking in Java is turing complete \cite{javaTuringComplete}.
|
||||
The grounding process of the ASP interpreter clingo would not terminate if the problem is turing complete
|
||||
\cite{kaufmann2016grounding}.
|
||||
The Java implementation is still able to spawn atleast one solution in most cases and only never terminates for specific inputs,
|
||||
whereas the ASP program never terminates as soon as wildcards are involved.
|
||||
|
||||
|
||||
%\section{Future Work}
|
||||
% Benchmarks
|
||||
% Integrating the ASP Unify implementation into existing Java-TX Compiler
|
||||
% Checking how many programs are abel to be build without wildcards
|
||||
|
||||
Loading…
Reference in New Issue
Block a user