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

Comments

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-04-03 00:50:59 +02:00
parent c6571879b7
commit 5371824a55
1 changed files with 19 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
unify.tex
View File

@ -1178,6 +1178,7 @@ C \cup \set{ \tv{a} \lessdot \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}}
% Otherwise the found solution is incorrect. % Otherwise the found solution is incorrect.
% This only happens if the input constraints contain type variables with no upper bound constraint like $\tv{a} \lessdot \type{N}$. % This only happens if the input constraints contain type variables with no upper bound constraint like $\tv{a} \lessdot \type{N}$.
% FOLLOWING IS WRONG AND JUST COMMENTS:
The motivating use case example for existential types in \cite{aModelForJavaWithWildcards} is not The motivating use case example for existential types in \cite{aModelForJavaWithWildcards} is not
type correct in \TamedFJ{} unfortunately. %Unify can calculate it though! type correct in \TamedFJ{} unfortunately. %Unify can calculate it though!
At least if we use the A-normal form transformation defined in chapter \cite{sec:anfTransformation}. At least if we use the A-normal form transformation defined in chapter \cite{sec:anfTransformation}.
@ -1186,12 +1187,29 @@ At least if we use the A-normal form transformation defined in chapter \cite{sec
<X> Pair<X,X> make(List<X> l) <X> Pair<X,X> make(List<X> l)
X.List<X> l = ... X.List<X> l = ...
cmp(make(l)) m(l) {
return cmp(make(l));
}
\end{lstlisting} \end{lstlisting}
\begin{lstlisting}[style=tamedfj] \begin{lstlisting}[style=tamedfj]
let v = { let x = l in make(x) } in cmp(v) let v = { let x = l in make(x) } in cmp(v)
\end{lstlisting} \end{lstlisting}
x <. l, x <c List<a?>, Pair<a?,a?> <. v, v <c Pair<b?,b?>
It will not infer a wildcard type. But a wildcard type can still be used to call m(l :: X.List<X>)
is it complete? Our no free variable restriction is too restrictive for let statement.
Not for method params. Only Java types are allowed. (no free variables)
would it be complete if we allow free variables everywhere?
Are there still supertypes that are not covered?
Box<Pair<String,String>> <. a
Box<Pair<Integer,Integer>> <. a
a =. X.Box<Pair<X,X>>
% TODO: find an example which is not inferred by our TI!
$\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ is a correct type for \texttt{v}. $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ is a correct type for \texttt{v}.
But the T-Let rule does only allow a type in the form of $\wctype{\rwildcard{X},\rwildcard{Y}}{Pair}{\rwildcard{X},\rwildcard{Y}}$. But the T-Let rule does only allow a type in the form of $\wctype{\rwildcard{X},\rwildcard{Y}}{Pair}{\rwildcard{X},\rwildcard{Y}}$.
%why is X,Y^X_X.Pair<X,Y> not a valid type? %why is X,Y^X_X.Pair<X,Y> not a valid type?
@ -1211,6 +1229,3 @@ x <c List<a>, Pair<a,a> <c Pair<b,b>
% which types are not allowed? the Same rule is the problem: here T <. a -> a =. T(without free variables) % which types are not allowed? the Same rule is the problem: here T <. a -> a =. T(without free variables)
% Example that does not work with our TI:
Pair<Pair<X,X>> <.
a <. X.Pair<Pair<X,X>>