From 6702d9b0cb86356f42b25057aedbdbe4ee672e3c Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Wed, 17 Apr 2024 12:59:31 +0200 Subject: [PATCH] Java local Type inference intro --- introduction.tex | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/introduction.tex b/introduction.tex index 8a16888..0d5c4ab 100644 --- a/introduction.tex +++ b/introduction.tex @@ -5,6 +5,26 @@ % - Constraints und Unifikation erklären, bevor Unifikation erwähnt wird \section{Motivation} +Java already uses type inference when it comes to method invocations, local variables or lambda expressions. +The crucial part for all of this use cases is the surrounding context. +The invocation of \texttt{emptyList} missing type parameters can be added by Java's local type inference +because the expected return type is known. \texttt{List} in this case. +\begin{lstlisting}[caption=Extract of a valid Java program] + List emptyList() { ... } + +List 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}$. + +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}. + +\begin{verbatim} +emptyList().get(0).get(0); +\end{verbatim} + \begin{verbatim} import java.util.ArrayList; import java.util.stream.*; @@ -59,6 +79,7 @@ emptyList().add(emptyList()).head().head() 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}. + % \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