645 lines
23 KiB
TeX
645 lines
23 KiB
TeX
% This is samplepaper.tex, a sample chapter demonstrating the
|
||
% LLNCS macro package for Springer Computer Science proceedings;
|
||
% Version 2.21 of 2022/01/12
|
||
%
|
||
\documentclass[submission]{eptcs}
|
||
\providecommand{\event}{Symposium in honor of Peter Thiemann's 60th birthday} % Name of the event you are submitting to
|
||
\usepackage{underscore}
|
||
\usepackage[T1]{fontenc}
|
||
% T1 fonts will be used to generate the final print and online PDFs,
|
||
% so please use T1 fonts in your manuscript whenever possible.
|
||
% Other font encondings may result in incorrect characters.
|
||
%
|
||
\usepackage{graphicx}
|
||
% Used for displaying a sample figure. If possible, figure files should
|
||
% be included in EPS format.
|
||
%
|
||
% If you use the hyperref package, please uncomment the following two lines
|
||
% to display URLs in blue roman font according to Springer's eBook style:
|
||
%\usepackage{color}
|
||
%\renewcommand\UrlFont{\color{blue}\rmfamily}
|
||
%\urlstyle{rm}
|
||
%
|
||
\include{prolog}
|
||
\usepackage{mathpartir}
|
||
\usepackage{amsmath}
|
||
\usepackage{amssymb}
|
||
\usepackage{amsthm}
|
||
\usepackage{enumitem}
|
||
\usepackage{xcolor}
|
||
%\usepackage{amsthm}
|
||
|
||
|
||
\newtheorem{theorem}{Theorem}
|
||
\newtheorem{lemma}[theorem]{Lemma}
|
||
|
||
\title{Global Type Inference for Java using Answer Set Programming}
|
||
\author{Andreas Stadelmeier
|
||
\institute{DHBW\\ Stuttgart}
|
||
\email{a.stadelmeier@hb.dhbw-stuttgart.de}
|
||
}
|
||
\newcommand{\authorrunning}{Andreas Stadelmeier}
|
||
\newcommand{\titlerunning}{Type Unification with ASP}
|
||
\hypersetup{
|
||
bookmarksnumbered,
|
||
pdftitle = {\titlerunning},
|
||
pdfauthor = {\authorrunning},
|
||
pdfsubject = {Global Type Inference for Java}, % Consider adding a more appropriate subject or description
|
||
pdfkeywords = {typeinference, java, sat solving, answer set programming} % Uncomment and enter keywords specific to your paper
|
||
}
|
||
|
||
\begin{document}
|
||
%
|
||
% First names are abbreviated in the running head.
|
||
% If there are more than two authors, 'et al.' is used.
|
||
%
|
||
%
|
||
\maketitle % typeset the header of the contribution
|
||
%
|
||
\begin{abstract}
|
||
Global type inference for Java is able to compute correct types for an input program
|
||
which has no type annotations at all, but turns out to be NP-hard.
|
||
Former implementations of the algorithm therefore struggled with bad runtime performance.
|
||
In this paper we translate the type inference algorithm for Featherweight Generic Java to an
|
||
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.
|
||
% 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.
|
||
%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}
|
||
|
||
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!
|
||
|
||
\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{lstlisting}
|
||
class C1 {
|
||
C1 self(){
|
||
return this;
|
||
}
|
||
}
|
||
class C2 {
|
||
C2 self(){
|
||
return this;
|
||
}
|
||
}
|
||
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}}$@*)
|
||
}
|
||
}
|
||
\end{lstlisting}
|
||
% \end{minipage}%
|
||
% \hfill
|
||
% \begin{minipage}{0.49\textwidth}
|
||
% \begin{lstlisting}[style=constraints]
|
||
% (*@$\tv{var} \lessdot \type{C1} | $@*),
|
||
% (*@$\sigma(\tv{xp}) = \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*)
|
||
% \end{lstlisting}
|
||
% \end{minipage}
|
||
%\end{figure}
|
||
|
||
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.
|
||
|
||
If we chain multiple overloaded method calls together we end up with multiple Or-Constraints.
|
||
The type unification algorithm \unify{} only sees the supplied constraints and has to potentially try all combinations of them.
|
||
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{lstlisting}
|
||
untypedMethod(var){
|
||
return var.self().self().self().self();
|
||
}
|
||
\end{lstlisting}
|
||
|
||
Now there are four chained method calls leading to four Or-Constraints:
|
||
\begin{align*}
|
||
\set{\tv{var} \lessdot \type{C1}, \tv{r1} \doteq \type{C1} }\ ||\ \set{\tv{var} \lessdot \type{C2}, \tv{r1} \doteq \type{C2}} \\
|
||
\set{\tv{r1} \lessdot \type{C1}, \tv{r2} \doteq \type{C1} }\ ||\ \set{\tv{r1} \lessdot \type{C2}, \tv{r2} \doteq \type{C2}} \\
|
||
\set{\tv{r2} \lessdot \type{C1}, \tv{r3} \doteq \type{C1} }\ ||\ \set{\tv{r2} \lessdot \type{C2}, \tv{r3} \doteq \type{C2}} \\
|
||
\set{\tv{r3} \lessdot \type{C1}, \tv{ret} \doteq \type{C1} }\ ||\ \set{\tv{r3} \lessdot \type{C2}, \tv{ret} \doteq \type{C2}} \\
|
||
\end{align*}
|
||
|
||
The placeholder $\tv{r1}$ stands for the return type of the first call to \texttt{self} and
|
||
$\tv{r2}$ for the return type of the second call and so on.
|
||
It is obvious that this constraint set only has two solutions.
|
||
The variable \texttt{var} and the return type of the method aswell as all intermediate placeholders $\tv{r1}-\tv{r3}$
|
||
get either the type \texttt{C1} or \texttt{C2}.
|
||
A first prototype implementation of the \unify{} algorithm simply created the cartesian product of all Or-Constraints,
|
||
16 possibilities in this example, and iteratively tried all of them.
|
||
This leads to a exponential runtime increase with every added overloaded method call.
|
||
Eventhough the current algorithm is equipped with various optimizations as presented in \cite{plue181} and \cite{plue231},
|
||
there is still a runtime increas sensible when dealing with many Or-Constraints.
|
||
|
||
Our global type inference algorithm should construct type solutions in real time.
|
||
Then it can effectively used as a Java compiler which can deal with large inputs of untyped Java code.
|
||
Another use case scenario is as an editor plugin which helps a Java programmer by enabling him to write untyped Java code
|
||
and letting our tool insert the missing type statements.
|
||
For both applications a short execution time is vital.
|
||
|
||
Answer Set programming promises to solve complex search problems in a highly optimized way.
|
||
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{Subtyping}
|
||
\begin{mathpar}
|
||
\inferrule[S-Refl]{}{
|
||
\type{T} <: \type{T}
|
||
}
|
||
\and
|
||
\inferrule[S-Trans]{\type{T}_1 <: \type{T}_2 \\ \type{T}_2 <: \type{T}_3}{
|
||
\type{T}_1 <: \type{T}_3
|
||
}
|
||
\and
|
||
\inferrule[S-Var]{}{\type{A} <: \Delta(\type{A})}
|
||
\and
|
||
\inferrule[S-Class]{\texttt{class}\ \exptype{C}{\ol{X}} \triangleleft \type{N}}{
|
||
\exptype{C}{\ol{T}} <: [\ol{T}/\ol{X}]\type{N}
|
||
}
|
||
\end{mathpar}
|
||
|
||
\begin{mathpar}
|
||
\inferrule[N-Refl]{}{
|
||
\type{C} << \type{C}
|
||
}
|
||
\and
|
||
\inferrule[N-Trans]{\type{C}_1 << \type{C}_2 \\ \type{C}_2 << \type{C}_3}{
|
||
\type{C}_1 << \type{C}_3
|
||
}
|
||
\and
|
||
\inferrule[N-Class]{\texttt{class}\ \exptype{C}{\ldots} \triangleleft \exptype{D}{\ldots}}{
|
||
\type{C} << \type{D}
|
||
}
|
||
\end{mathpar}
|
||
|
||
%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
|
||
|
||
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.
|
||
\label{sec:implicationRules}
|
||
\begin{mathpar}
|
||
\inferrule[Subst-L]{
|
||
\tv{a} \doteq \type{T}_1 \\
|
||
\tv{a} \lessdot \type{T}_2
|
||
}{
|
||
\type{T}_1 \lessdot \type{T}_2
|
||
}
|
||
\and
|
||
\inferrule[Subst-R]{
|
||
\tv{a} \doteq \type{T}_1 \\
|
||
\type{T}_2 \lessdot \tv{a}
|
||
}{
|
||
\type{T}_2 \lessdot \type{T}_1
|
||
}
|
||
\and
|
||
\inferrule[Subst-Equal]{
|
||
\tv{a} \doteq \type{T}_1 \\
|
||
\tv{a} \doteq \type{T}_2
|
||
}{
|
||
\type{T}_1 \doteq \type{T}_2
|
||
}
|
||
\and
|
||
\inferrule[Swap]{
|
||
\type{T}_1 \doteq \type{T}_2
|
||
}{
|
||
\type{T}_2 \doteq \type{T}_1
|
||
}
|
||
\and
|
||
\inferrule[Unfold]{
|
||
\tv{b} \doteq \exptype{C}{\type{T}_1 \ldots \type{T}_n}
|
||
}{
|
||
\type{T}_i \doteq \type{T}_i
|
||
}
|
||
\and
|
||
\inferrule[Subst-Param]{
|
||
\tv{a} \doteq \type{S} \\
|
||
\type{T} \doteq \exptype{C}{\type{T}_1 \ldots, \tv{a}, \ldots \type{T}_n} \\
|
||
}{
|
||
\type{T} \doteq \exptype{C}{\type{T}_1, \ldots \type{S}, \ldots \type{T}_n}
|
||
}
|
||
\and
|
||
\inferrule[Subst-Param']{
|
||
\tv{a} \doteq \type{S} \\
|
||
\tv{b} \lessdot \exptype{C}{\type{T}_1 \ldots, \tv{a}, \ldots \type{T}_n} \\
|
||
}{
|
||
\tv{b} \lessdot \exptype{C}{\type{T}_1, \ldots \type{S}, \ldots \type{T}_n}
|
||
}
|
||
\and
|
||
\inferrule[S-Object]{}{\tv{a} \lessdot \type{Object}}
|
||
\and
|
||
\inferrule[Match]{
|
||
\tv{a} \lessdot \type{N}_1 \\
|
||
\tv{a} \lessdot \type{N}_2 \\
|
||
\type{N}_1 << \type{N}_2
|
||
}{
|
||
\type{T}_1 \lessdot \type{T}_2
|
||
}
|
||
\and
|
||
\inferrule[Adopt]{
|
||
\tv{a} \lessdot \tv{b} \\
|
||
\tv{b} \lessdot \type{T}
|
||
}{
|
||
\tv{a} \lessdot \type{T}
|
||
}
|
||
\and
|
||
% \inferrule[Subst-Param]{
|
||
% \tv{a} \doteq \type{N} \\
|
||
% \tv{a} = \type{T}_i \\
|
||
% \exptype{C}{\type{T}_1 \ldots \type{T}_n} \lessdot \type{T} \\
|
||
% }{
|
||
% \type{T}_i \doteq \type{N} \\
|
||
% }
|
||
\and
|
||
\inferrule[Adapt]{
|
||
\type{N}_1 \lessdot \exptype{C}{\type{T}_1 \ldots \type{T}_n} \\
|
||
\type{N}_1 <: \exptype{C}{\type{S}_1 \ldots \type{S}_n} \\
|
||
}{
|
||
\exptype{C}{\type{S}_1 \ldots \type{S}_n} \doteq \exptype{C}{\type{T}_1 \ldots \type{T}_n} \\
|
||
}
|
||
\and
|
||
\inferrule[Reduce]{
|
||
\exptype{C}{\type{S}_1 \ldots \type{S}_n} \doteq \exptype{C}{\type{T}_1 \ldots \type{T}_n} \\
|
||
}{
|
||
\type{S}_i \doteq \type{T}_i \\
|
||
}
|
||
\end{mathpar}
|
||
|
||
\begin{mathpar}
|
||
\text{Apply only once per constraint:}\quad
|
||
\inferrule[Super]{
|
||
\type{N} \lessdot \tv{a}\\
|
||
\type{N} <: \type{N}'
|
||
}{
|
||
\tv{a} \doteq \type{N}'
|
||
}
|
||
\end{mathpar}
|
||
|
||
\begin{center}
|
||
Apply one or the other:
|
||
\end{center}
|
||
\begin{mathpar}
|
||
\inferrule[Split-L]{
|
||
\tv{a} \lessdot \tv{b}\\
|
||
\tv{a} \lessdot \type{N}\\
|
||
}{
|
||
\tv{b} \lessdot \type{N}
|
||
}
|
||
\quad \quad
|
||
\vline
|
||
\quad \quad
|
||
\inferrule[Split-R]{
|
||
\tv{a} \lessdot \tv{b}\\
|
||
\tv{a} \lessdot \type{N}\\
|
||
}{
|
||
\type{N} \lessdot \tv{b}
|
||
}
|
||
\end{mathpar}
|
||
|
||
Result:
|
||
\begin{mathpar}
|
||
\inferrule[Solution]{
|
||
\tv{a} \doteq \type{G}
|
||
}{
|
||
\sigma(\tv{a}) = \type{G}
|
||
}
|
||
\and
|
||
\inferrule[Solution-Gen]{
|
||
\tv{a} \lessdot \type{C}_1, \ldots, \tv{a} \lessdot \type{C}_n \\
|
||
\forall i: \type{C}_m << \type{C}_i \\
|
||
}{
|
||
\tv{a} \doteq \type{C}_m
|
||
}
|
||
% \and
|
||
% \inferrule[Solution-Gen]{
|
||
% \tv{a} \lessdot \type{C}\\
|
||
% \sigma(\tv{a}) = \emptyset
|
||
% }{
|
||
% \tv{a} \doteq \type{A} \\ \sigma'(\tv{a}) = \type{A}
|
||
% }
|
||
% \and
|
||
% \inferrule[Solution-Gen]{
|
||
% \tv{a} \lessdot \type{G} \\
|
||
% \tv{a} \lessdot \type{G}_1, \ldots, \tv{a} \lessdot \type{G}_n \\
|
||
% \forall i: \type{G} << \type{G}_i \\
|
||
% \sigma'(\tv{a}) = \type{A}
|
||
% }{
|
||
% \Delta(\type{A}) = \type{G}
|
||
% }
|
||
\end{mathpar}
|
||
|
||
Fail:
|
||
|
||
\begin{mathpar}
|
||
% \inferrule[Fail]{
|
||
% \type{T} \lessdot \type{N}\\
|
||
% \type{T} \nless : \type{N}
|
||
% }{
|
||
% \emptyset
|
||
% }
|
||
% \and
|
||
\inferrule[Fail]{
|
||
\exptype{C}{\ldots} \doteq \exptype{D}{\ldots}\\
|
||
\type{C} \neq \type{D}
|
||
}{
|
||
\emptyset
|
||
}
|
||
\and
|
||
\inferrule[Fail-Generic]{
|
||
\type{X} \doteq \type{T}\\
|
||
\type{X} \neq \type{T}
|
||
}{
|
||
\emptyset
|
||
}
|
||
\and
|
||
\inferrule[Fail-Sigma]{
|
||
\tv{a} \doteq \type{N} \\
|
||
\tv{a} \in \type{N}
|
||
}{
|
||
\emptyset
|
||
}
|
||
\and
|
||
\inferrule[Fail]{
|
||
\tv{a} \lessdot \type{N}_1 \\
|
||
\tv{a} \lessdot \type{N}_2 \\
|
||
\text{not}\ \type{N}_1 << \type{N}_2 \\
|
||
\text{not}\ \type{N}_2 << \type{N}_1
|
||
}{
|
||
\emptyset
|
||
}
|
||
\end{mathpar}
|
||
|
||
% Subst
|
||
% a =. N, a <. T, N <: T
|
||
% --------------
|
||
% N <. T
|
||
|
||
% a <. List<b>, b <. List<a>
|
||
|
||
% how to proof completeness and termination?
|
||
% TODO: how to proof termination?
|
||
|
||
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}
|
||
\newcommand{\aspify}{\nabla}
|
||
\begin{align*}
|
||
\aspify(\tv{a}) =& \texttt{tph("a")}\\
|
||
\exptype{C}{} =& \texttt{type("C", null)}\\
|
||
\exptype{C}{\type{T}_1, \type{T}_2, \ldots} =& \texttt{type("C", params(}\aspify(\type{T}_1), \aspify(\type{T}_1), \ldots\texttt{))}\\
|
||
\aspify(\type{T} \doteq \type{T}') =& \texttt{equalcons}(\aspify(\type{T}), \aspify(\type{T}')) \\
|
||
\aspify(\type{T} \lessdot \type{T}') =& \texttt{subcons}(\aspify(\type{T}), \aspify(\type{T}')) \\
|
||
\aspify{} \left(\inferrule{
|
||
c_1, c_2
|
||
}{
|
||
c
|
||
}\right) =& \aspify(c)\ \texttt{:-} \aspify(c_1), \aspify(c_2)
|
||
\end{align*}
|
||
|
||
The S-Class rule contains a substitution and has to be encoded with 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
|
||
\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$.
|
||
|
||
\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
|
||
|
||
\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}
|
||
|
||
|
||
\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.
|
||
|
||
\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
|
||
|
||
\bibliographystyle{eptcs}
|
||
\bibliography{martin}
|
||
|
||
\end{document}
|