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

Finish someList example

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-05-04 13:56:55 +02:00
parent 4a3e39ad9e
commit 72dff3fa36
1 changed files with 16 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
unify.tex
View File

@ -74,13 +74,15 @@ $\begin{array}{l}
%$\exptype{List}{\type{String}} \lessdot {\ntv{r}}, \exptype{List}{\type{Integer}} \lessdot {\ntv{r}}$
The constraint $\type{String} \lessdot {\ntv{x}}$ is solved by applying
\rulename{Super} and substituting $\type{String}$ for $\ntv{x}$.
The same for $\type{Integer} \lessdot \ntv{y}$ accordingly,
\rulename{Super} and afterwards substituting $\type{String}$ for $\ntv{x}$,
same for $\type{Integer} \lessdot \ntv{y}$,
resulting in the two constraints \linebreak[2]
$\exptype{List}{\type{Integer}} \lessdot {\ntv{r}},
\exptype{List}{\type{String}} \lessdot {\ntv{r}}$.
$\exptype{List}{\type{Integer}} \lessdot {\ntv{r}}$ \linebreak[2] and \linebreak[2]
$\exptype{List}{\type{String}} \lessdot {\ntv{r}}$.
Now comes the part where \unify{} creates existential types by applying the \rulename{Same} transformation.
An existential type is created with fresh type placeholders as upper and lower bound.
After a substitution all $\tv{r}$ are replaced with this new existential type.
\unify{} can now determine type replacements for the freshly created bounds $\tv{u}$ and $\tv{l}$.
\begin{displaymath}
\prftree[r]{\rulename{Reduce}}{
\prftree[r]{\rulename{Subst}}{
@ -96,7 +98,15 @@ $\exptype{List}{\type{Integer}} \lessdot {\ntv{r}},
\type{Integer} \lessdot \ntv{u}, \ntv{l} \lessdot \type{Integer}}
\end{displaymath}
In this example a correct solution is $\sigma(\tv{u}) = \type{Object}$ and $\sigma(\tv{l}) = \bot$.
Remember that the substitution for the type placeholder $\tv{r}$ is $\wctype{\wildcard{X}{\ntv{u}}{\ntv{l}}}{List}{\rwildcard{X}}$
leading to \texttt{List<?>} as a return type for the \texttt{someList} method after applying $\sigma$.
\begin{lstlisting}
List<? extends Object> someList(){
return new List("String") :? new List(42);
}
\end{lstlisting}
\subsection{Description}
The \unify{} algorithm tries to find a solution for a set of constraints like