This commit is contained in:
Andreas Stadelmeier 2024-04-21 13:09:13 +02:00
parent 9035c5faf1
commit c42477bf8a

View File

@ -18,7 +18,7 @@ List<String> ls = emptyList();
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>}.
a \texttt{List<Object>} instead of the required \texttt{List<List<String>>}.
\begin{verbatim}
emptyList().add(new List<String>())
.get(0)
@ -40,8 +40,13 @@ this.<List<String>>emptyList().add(new List<String>())
.get(0);
\end{verbatim}
%motivate constraints:
For this example we will create constraints $\exptype{List}{\tv{a}} \lessdot \tv{b}...$ TODO
%motivate constraints:
To solve this example we will create constraints
$
\exptype{List}{\tv{a}} \lessdot \tv{b},
\tv{b} \lessdot \exptype{List}{\tv{c}},
\tv{c} \lessdot \exptype{List}{\tv{d}}
$ 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