stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Intro Wildcards

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-05-07 16:14:48 +02:00
parent 38589f804c
commit 6c8b78914f
1 changed files with 41 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

51
introduction.tex
View File

@ -293,19 +293,50 @@ List<?> genList() {
\subsection{Java Wildcards}
Java has invariant subtyping for polymorphic types
and incooperates use-site variance via so called wildcard types.
Java has invariant subtyping for polymorphic types.
%but it incooperates use-site variance via so called wildcard types.
A \texttt{List<String>} is not a subtype of \texttt{List<Object>}
even though it seems intuitive with \texttt{String} being a subtype of \texttt{Object}.
To make the type system more expressive Java incooperates use-site variance by allowing wildcards (\texttt{?}) in type annotations.
For example a type \texttt{List<?>} (short for \texttt{List<? extends Object>}, with \texttt{?} being a placeholder for any type) %with the wildcard \texttt{?} representing a placeholder for any type
is a supertype of \texttt{List<String>} and \texttt{List<Object>}.
%The \texttt{?} is a wildcard type which can be replaced by any type as needed.
%Class instances in Java are mutable and passed by reference.
Subtyping must be invariant otherwise the integrity of data classes like lists could be
corrupted like shown in listing \ref{lst:invarianceExample},
where an \texttt{Integer} is added to a list of \texttt{String}.
In listing \ref{lst:invarianceExample} the assignment \texttt{lo = ls} is not semantically correct
and rejected by Java's type system.
Listing \ref{lst:wildcardIntro} shows the use of wildcards in the type
\texttt{List<? extends Object>} which is a supertype of \texttt{List<String>}
rendering the assignment \texttt{lo = ls} correct.
Subtyping must be invariant in Java otherwise the integrity of data classes like \texttt{List} could be cannot be guaranteed.
See listing \ref{lst:invarianceExample} for example,
where an \texttt{Integer} would be added to a list of \texttt{String}
if not for the Java type system which rejects the assignment \texttt{lo = ls}.
Listing \ref{lst:wildcardIntro} shows the use of wildcards rendering the assignment \texttt{lo = ls} correct.
The program still does not compile, because now the addition of an Integer to \texttt{lo} is rightfully deemed incorrect by Java.
This behaviour is emulated by our language \TamedFJ{}.
A Featherweight Java \cite{FJ} derivative with added wildcard support
and a global type inference feature.
\TamedFJ{} is basically the language described by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection} with optional type annotations.
The \texttt{add} call in listing \ref{lst:wildcardIntro} needs to be encased by a \texttt{let} statement in our calculus.
This makes the capture converion explicit.
\begin{lstlisting}
let v : (*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$@*) = lo in v.<A>add(new Integer(1));
\end{lstlisting}
\begin{displaymath}
\begin{array}{l}
\begin{array}{@{}c}
\textit{mtype}(\texttt{concat}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \\
\texttt{l1} : \wctype{\rwildcard{A}}{List}{\rwildcard{A}}, \texttt{l2} : \wctype{\rwildcard{B}}{List}{\rwildcard{B}} \\
\exptype{List}{\rwildcard{A}} \nless: [{\color{red}?}/\type{X}]\exptype{List}{\type{X}} \quad \quad
\exptype{List}{\rwildcard{B}} \nless: [{\color{red}?}/\type{X}]\exptype{List}{\type{X}}
\\
\hline
\vspace*{-0.3cm}\\
\texttt{concat}(\expr{l1}, \expr{l2}) : {\color{red}\textbf{Error}}
\end{array}
\end{array}
\end{displaymath}
\begin{figure}
\begin{minipage}{0.4\textwidth}