Cleanup motivation
This commit is contained in:
JanUlrich
parent
df22ed5cce
commit
9035c5faf1
132
introduction.tex
132
introduction.tex
@ -15,15 +15,7 @@ because the expected return type is known. \texttt{List<String>} in this case.
|
||||
List<String> ls = emptyList();
|
||||
\end{lstlisting}
|
||||
|
||||
Local type inference \cite{javaTIisBroken} is able to find a type substitution $\sigma$ satisfying
|
||||
$\overline{\type{A} <: \sigma(\type{F}) }, \sigma(\type{R}) <: \type{E}$.
|
||||
It is important that $\overline{\type{A}}$ and $\type{E}$ are given types and do not contain
|
||||
type placeholders already used in $\overline{\type{F}}$.
|
||||
|
||||
The type parameters are not allowed on the left side of $A <: F$
|
||||
We can generate method calls where this is the case. The second call to \texttt{get}.
|
||||
|
||||
Local type inference is based on matching and not unification.
|
||||
Local type inference is based on matching and not unification \cite{javaTIisBroken}.
|
||||
When calling the \texttt{emptyList} method without context its return value will be set to a \texttt{List<Object>}.
|
||||
The following Java code snippet is incorrect, because \texttt{emptyList()} returns
|
||||
a \texttt{List<Object>} instead of the required \texttt{List<String>}.
|
||||
@ -36,87 +28,83 @@ emptyList().add(new List<String>())
|
||||
%List<A> <: List<B>, B <: List<C>
|
||||
% B = A and therefore A on the left and right side of constraints.
|
||||
% this makes matching impossible
|
||||
|
||||
The return type of the first \texttt{get} method is based on the return type of
|
||||
\texttt{emptyList},
|
||||
but the second call to \texttt{get} is only possible if \texttt{emptyList} returns
|
||||
a list of lists.
|
||||
The local type inference algorithm based on matching cannot produce this solution.
|
||||
Here a type inference algorithm based on unification is needed.
|
||||
\begin{verbatim}
|
||||
this.<List<String>>emptyList().add(new List<String>())
|
||||
.get(0)
|
||||
.get(0);
|
||||
\end{verbatim}
|
||||
|
||||
Local type inference cannot deal with type inference during the algorithm.
|
||||
If the left side contains unknown type parameters.
|
||||
%motivate constraints:
|
||||
For this example we will create constraints $\exptype{List}{\tv{a}} \lessdot \tv{b}...$ TODO
|
||||
Local type inference \cite{javaTIisBroken} is able to find a type substitution $\sigma$ satisfying
|
||||
$\overline{\type{A} <: \sigma(\type{F}) }, \sigma(\type{R}) <: \type{E}$.
|
||||
It is important that $\overline{\type{A}}$ and $\type{E}$ are given types and do not contain
|
||||
type placeholders already used in $\overline{\type{F}}$.
|
||||
|
||||
The type parameters are not allowed on the left side of $A <: F$
|
||||
We can generate method calls where this is the case. The second call to \texttt{get}.
|
||||
|
||||
% Local type inference cannot deal with type inference during the algorithm.
|
||||
% If the left side contains unknown type parameters.
|
||||
|
||||
|
||||
\begin{verbatim}
|
||||
import java.util.ArrayList;
|
||||
import java.util.stream.*;
|
||||
% \begin{verbatim}
|
||||
% import java.util.ArrayList;
|
||||
% import java.util.stream.*;
|
||||
|
||||
class Test {
|
||||
void test(){
|
||||
var s = new ArrayList<String>().stream().map(i -> 1);
|
||||
receive(s);
|
||||
}
|
||||
% class Test {
|
||||
% void test(){
|
||||
% var s = new ArrayList<String>().stream().map(i -> 1);
|
||||
% receive(s);
|
||||
% }
|
||||
|
||||
void receive(Stream<Object> l){}
|
||||
}
|
||||
\end{verbatim}
|
||||
% void receive(Stream<Object> l){}
|
||||
% }
|
||||
% \end{verbatim}
|
||||
|
||||
TypeError:
|
||||
\begin{verbatim}
|
||||
void test(){
|
||||
var l = new ArrayList<String>();
|
||||
l.add("hi");
|
||||
var s = l.stream().map(i -> 1).collect(Collectors.toList());
|
||||
var s2 = l.stream().map(i -> "String").collect(Collectors.toList());
|
||||
receive(s, s2);
|
||||
}
|
||||
<A> void receive(List<A> l, List<A> l2){}
|
||||
\end{verbatim}
|
||||
Correct:
|
||||
\begin{verbatim}
|
||||
void test(){
|
||||
var l = new ArrayList<String>();
|
||||
l.add("hi");
|
||||
List<Object> s = l.stream().map(i -> 1).collect(Collectors.toList());
|
||||
List<Object> s2 = l.stream().map(i -> "String").collect(Collectors.toList());
|
||||
receive(s, s2);
|
||||
}
|
||||
<A> void receive(List<A> l, List<A> l2){}
|
||||
\end{verbatim}
|
||||
|
||||
Error:
|
||||
\begin{verbatim}
|
||||
rrr(this.emptyBox().set(this.<Integer>emptyBox()).set(this.<String>emptyBox()));
|
||||
\end{verbatim}
|
||||
Correct:
|
||||
\begin{verbatim}
|
||||
rrr(this.<Box<?>>emptyBox().set(this.<Integer>emptyBox()).set(this.<String>emptyBox()));
|
||||
\end{verbatim}
|
||||
|
||||
incorrect:
|
||||
\begin{verbatim}
|
||||
emptyList().add(emptyList()).head().head()
|
||||
\end{verbatim}
|
||||
|
||||
In this example the return type of \texttt{emptyList} needs to consider that it should contain a list of a list.
|
||||
This is a limitation of local type inference as presented here \cite{javaTIisBroken}.
|
||||
% TypeError:
|
||||
% \begin{verbatim}
|
||||
% void test(){
|
||||
% var l = new ArrayList<String>();
|
||||
% l.add("hi");
|
||||
% var s = l.stream().map(i -> 1).collect(Collectors.toList());
|
||||
% var s2 = l.stream().map(i -> "String").collect(Collectors.toList());
|
||||
% receive(s, s2);
|
||||
% }
|
||||
% <A> void receive(List<A> l, List<A> l2){}
|
||||
% \end{verbatim}
|
||||
% Correct:
|
||||
% \begin{verbatim}
|
||||
% void test(){
|
||||
% var l = new ArrayList<String>();
|
||||
% l.add("hi");
|
||||
% List<Object> s = l.stream().map(i -> 1).collect(Collectors.toList());
|
||||
% List<Object> s2 = l.stream().map(i -> "String").collect(Collectors.toList());
|
||||
% receive(s, s2);
|
||||
% }
|
||||
% <A> void receive(List<A> l, List<A> l2){}
|
||||
% \end{verbatim}
|
||||
|
||||
% Error:
|
||||
% \begin{verbatim}
|
||||
% rrr(this.emptyBox().set(this.<Integer>emptyBox()).set(this.<String>emptyBox()));
|
||||
% \end{verbatim}
|
||||
% Correct:
|
||||
% \begin{verbatim}
|
||||
% rrr(this.<Box<?>>emptyBox().set(this.<Integer>emptyBox()).set(this.<String>emptyBox()));
|
||||
% \end{verbatim}
|
||||
|
||||
% \begin{recap}{Java Local Type Inference}
|
||||
% Local type inference is able to solve constraints of the form
|
||||
% T <. b, b <. T where T are given types
|
||||
% \end{recap}
|
||||
% Local Type inference cannot infer F-Bounded types (TODO: we can, right?)
|
||||
The big difference to local type inference is the ability to have constraints where both sides contain type placeholders.
|
||||
As described in \cite{javaTIisBroken} local type inference is able to determine an unifier $\sigma$
|
||||
which satisfies $\set{\overline{A <: \sigma(F)}, \sigma(R) <: E }$.
|
||||
Note that $A$ and $E$ are already given types.
|
||||
$A$ are method arguments and $E$ is the expected return type.
|
||||
|
||||
% Are there examples where the expected return type is not given?
|
||||
% with global type inference this is easy to produce
|
||||
% an example where this is the case for local type inference?
|
||||
% - the val example
|
||||
|
||||
\section{Type Inference for Java}
|
||||
%The goal is to find a correct typing for a given Java program.
|
||||
|
||||
Loading…
Reference in New Issue
Block a user