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

Explain let

Browse Source
This commit is contained in:
JanUlrich 2024-05-07 23:49:07 +02:00
parent 6c8b78914f
commit 2dae79053c
1 changed files with 22 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
introduction.tex
View File

@ -303,8 +303,8 @@ 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 in Java otherwise the integrity of data classes like \texttt{List} could be cannot be guaranteed.
See listing \ref{lst:invarianceExample} for example,
Subtyping must be invariant in Java otherwise the integrity of data classes like \texttt{List} 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.
@ -314,13 +314,29 @@ 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.
Let's have a look at a representation of the \texttt{add} call from the last line in listing \ref{lst:wildcardIntro} in our calculus:
%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}
The method call needs to be encased in a \texttt{let} statement.
The variable \expr{v} is assigned the \textbf{Existential Type} $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$.
Wildcards can be formalized as existential types \cite{WildFJ}:
\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,
and a type they are bound to.
In this case the name is $\rwildcard{A}$ and it's bound to the the type \texttt{List}.
Inside the \texttt{let} statement the variable \expr{v} has the type
$\exptype{List}{\rwildcard{A}}$.
This is an explicit version of \textbf{Capture Conversion},
which makes use of the fact that a concrete type must be behind every wildcard type.
There is no instantiation of a \texttt{List<?>},
but there exists some unknown type $\exptype{List}{\rwildcard{A}}$, with $\rwildcard{A}$ inbetween the bounds $\bot$ (bottom type, subtype of all types) and
\texttt{Object}.
After assigning \texttt{lo} to \expr{v} it will not change it's type during the execution of the body of \texttt{let}
and \expr{v} is treated as the type $\exptype{List}{\rwildcard{A}}$
\begin{displaymath}
\begin{array}{l}