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

Rephrase Triple example

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-04-10 17:40:49 +02:00
parent b78594cf39
commit 24cfd8cb75
1 changed files with 41 additions and 43 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

84
introduction.tex
View File

@ -561,6 +561,47 @@ As soon as enough type information is given \unify{} can conduct a capture conve
The constraints where this is possible are marked as capture constraints.
\section{Discussion Pair Example}
\begin{verbatim}
<X> Pair<X,X> make(List<X> l){ ... }
<X> boolean compare(Pair<X,X> p) { ... }
List<?> l;
Pair<?,?> p;
compare(make(l)); // Valid
compare(p); // Error
\end{verbatim}
Our type inference algorithm is not able to solve this example.
When we convert this to \TamedFJ{} and generate constraints we end up with:
\begin{lstlisting}[style=tamedfj]
let m = let x = l in make(x) in compare(m)
\end{lstlisting}
\begin{constraintset}$
\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \ntv{x},
\ntv{x} \lessdotCC \exptype{List}{\wtv{a}}
\exptype{Pair}{\wtv{a}, \wtv{a}} \lessdot \ntv{m}, %% TODO: Mark this constraint
\ntv{m} \lessdotCC \exptype{Pair}{\wtv{b}, \wtv{b}}
$\end{constraintset}
$\ntv{x}$ will get the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and
from the constraint
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
\unify{} deducts $\wtv{a} \doteq \rwildcard{X}$ leading to
$\exptype{Pair}{\rwildcard{X}, \rwildcard{X}} \lessdot \ntv{m}$.
Finding a supertype to $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ is the crucial part.
The correct substition for $\ntv{m}$ would be $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$.
But this leads to additional branching inside the \unify{} algorithm and increases runtime.
%We refrain from using that type, because it is not denotable with Java syntax.
%Types used for normal type placeholders should be expressable Java types. % They are not!
The prefered way of dealing with this example in our opinion would be the addition of a multi-let statement to the syntax.
\begin{lstlisting}[style=letfj]
let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l, m = make(x) in compare(make(x))
\end{lstlisting}
We can make it work with a special rule in the \unify{}.
But this will only help in this specific example and not generally solve the issue.
A type $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ has atleast two immediate supertypes:
@ -599,49 +640,6 @@ $
\end{constraintset}
\begin{verbatim}
<X> Pair<X,X> make(List<X> l){ ... }
<X> boolean compare(Pair<X,X> p) { ... }
List<?> l;
Pair<?,?> p;
compare(make(l)); // Valid
compare(p); // Error
\end{verbatim}
Our type inference algorithm is not able to solve this example.
When we convert this to \TamedFJ{} and generate constraints we end up with:
\begin{lstlisting}[style=tamedfj]
let m = let x = l in make(x) in compare(m)
\end{lstlisting}
\begin{constraintset}$
\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \ntv{x},
\ntv{x} \lessdotCC \exptype{List}{\wtv{a}}
\exptype{Pair}{\wtv{a}, \wtv{a}} \lessdot \ntv{m}, %% TODO: Mark this constraint
\ntv{m} \lessdotCC \exptype{Pair}{\wtv{b}, \wtv{b}}
$\end{constraintset}
$\ntv{x}$ will get the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and
from the constraint
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
\unify{} deducts $\wtv{a} \doteq \rwildcard{X}$ leading to
$\exptype{Pair}{\rwildcard{X}, \rwildcard{X}} \lessdot \ntv{m}$.
Finding a supertype to $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ is the crucial part.
The correct substition for $\ntv{m}$ would be $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$.
We refrain from using that type, because it is not denotable with Java syntax.
Types used for normal type placeholders should be expressable Java types.
The prefered way of dealing with this example in our opinion would be the addition of a multi-let statement to the syntax.
\begin{lstlisting}[style=letfj]
let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l in let m = make(x) in compare(m)
\end{lstlisting}
\end{itemize}
%TODO: Move this part. or move the third challenge some underneath.