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

Rephrase Wildcard Intro

Browse Source
This commit is contained in:
JanUlrich 2024-05-07 11:30:45 +02:00
parent b432c5b091
commit b5f7345e51
1 changed files with 15 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
introduction.tex
View File

@ -295,13 +295,19 @@ List<?> genList() {
Java has invariant subtyping for polymorphic types Java has invariant subtyping for polymorphic types
and incooperates use-site variance via so called wildcard types. and incooperates use-site variance via so called wildcard types.
A \texttt{List<String>} is not a subtype of \texttt{List<Object>} for example 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}. even though it seems intuitive with \texttt{String} being a subtype of \texttt{Object}.
Class instances in Java are mutable and passed by reference. %Class instances in Java are mutable and passed by reference.
Subtyping must be invariant otherwise the integrity of data classes like lists could be Subtyping must be invariant otherwise the integrity of data classes like lists could be
corrupted like shown in listing \ref{lst:invarianceExample}, corrupted like shown in listing \ref{lst:invarianceExample},
where an \texttt{Integer} is added to a list of \texttt{String}. 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.
\begin{figure}
\begin{minipage}{0.4\textwidth} \begin{minipage}{0.4\textwidth}
\begin{lstlisting}[caption=Java Invariance Example,label=lst:invarianceExample]{java} \begin{lstlisting}[caption=Java Invariance Example,label=lst:invarianceExample]{java}
List<String> ls = ...; List<String> ls = ...;
@ -312,24 +318,20 @@ lo.add(new Integer(1));
\end{minipage} \end{minipage}
\hfill \hfill
\begin{minipage}{0.5\textwidth} \begin{minipage}{0.5\textwidth}
\begin{lstlisting}[caption=Use-Site Variance Example]{java} \begin{lstlisting}[caption=Use-Site Variance Example,label=lst:wildcardIntro]{java}
List<String> ls = ...; List<String> ls = ...;
List<? extends Object> lo = ...; List<? extends Object> lo = ...;
lo = ls; // correct lo = ls; // correct
lo.add(new Integer(1)); // error! lo.add(new Integer(1)); // error!
\end{lstlisting} \end{lstlisting}
\end{minipage} \end{minipage}
\end{figure}
Wildcards can be formalized as existential types \cite{WildFJ}.
A \texttt{List<? extends Object>} is translated to $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$
and \texttt{List<? super String>} is expressed as $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
%Passing wildcard types to a polymorphic method call comes with additional challenges. %Passing wildcard types to a polymorphic method call comes with additional challenges.
% TODO: Here the concat example! % TODO: Here the concat example!
- Wildcards are not reflexive %- Wildcards are not reflexive
- Wildcards are opaque types. Behind a Java Wildcard is a real type. %- Wildcards are opaque types. Behind a Java Wildcard is a real type.
Wildcard types are virtual types. Wildcard types are virtual types.
There is no instantiation of a \texttt{List<?>}. There is no instantiation of a \texttt{List<?>}.
@ -381,6 +383,9 @@ concat(l1, l2);
%A method call in Java makes use of the fact that a real type is behind a wildcard type %A method call in Java makes use of the fact that a real type is behind a wildcard type
Wildcards can be formalized as existential types \cite{WildFJ}.
A \texttt{List<? extends Object>} is translated to $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$
and \texttt{List<? super String>} is expressed as $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound at the same time, The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound at the same time,
and a type they are bound to. and a type they are bound to.