Cleanup. Define mutual subtyping as equality
This commit is contained in:
Andreas Stadelmeier
parent
e40693a7de
commit
9556f1521e
@ -26,6 +26,12 @@ $
|
||||
The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
|
||||
Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
|
||||
|
||||
|
||||
The parameter types given to a generic method also affect their return type.
|
||||
During constraint generation the algorithm does not know the parameter types yet.
|
||||
We generate $\lessdotCC$ constraints and let \unify{} do the capture conversion.
|
||||
$\lessdotCC$ constraints are kept until they reach the form $\type{G} \lessdotCC \type{G}$ and a capture conversion is possible.
|
||||
|
||||
At points where a well-formed type is needed we use a normal type placeholder.
|
||||
Inside a method call expression sub expressions (receiver, parameter) wildcard placeholders are used.
|
||||
Here captured variables can flow freely.
|
||||
|
||||
@ -513,6 +513,17 @@ $
|
||||
\end{figure}
|
||||
% TODO: make Unify to resolve C<X> <. a as a =. X.C<X>
|
||||
|
||||
% A method has infinte possibilities of being called and there is no most general type.
|
||||
% P<X,Y> m(C<X> c, C<Y> c2)
|
||||
% depending on
|
||||
% A.P<A,A> <. A,B.P<A,B>
|
||||
|
||||
% % During the method call it is not sure what kind of return type is needed from the method.
|
||||
% % The method P<A,B> make(A a, B b)
|
||||
% % The type A,B.P<A,B> cannot be a subtype of P<X,X>
|
||||
% % But if A^X_X and B^X_X
|
||||
% % Could a constraint C<X> <. a? be expanded to a? = X^u?_l?.C<X>
|
||||
|
||||
|
||||
\end{itemize}
|
||||
|
||||
|
||||
@ -432,7 +432,8 @@ holds with any $\Delta'$ so that $(\text{fv}(\exptype{C}{\ol{S}}) \cup \text{fv}
|
||||
\item[Circle] S-Refl
|
||||
\item[Swap] by definition
|
||||
\item[Erase] S-Refl
|
||||
\item[Equals] %by definition
|
||||
\item[Equals] by definition \ref{def:equal}
|
||||
%by definition
|
||||
%TODO
|
||||
% Unify does never contain wildcard environments with unused wildcards. Therefore after N <: N' and N' <: N, both types have the same wildcard environment
|
||||
|
||||
|
||||
217
unify.tex
217
unify.tex
@ -1,80 +1,11 @@
|
||||
% TODO: unify changes
|
||||
% a? <. T can be deleted in the last step
|
||||
% delete wildcard tphs a? when needed
|
||||
% aswell ass free variables:
|
||||
% a <. T with fv(T) not empty and not in \Delta' must be removed by U = L
|
||||
% also in T <. T constraints no free variables are allowed on both sides
|
||||
% also in T <. T constraints no free variables are allowed on both sides (why? this is wrong i think)
|
||||
% the algorithm only removes wildcards, never adds them
|
||||
|
||||
% lessdotCC constraint cannot be removed. we do not know what to capture
|
||||
% example <X> add(List<X> l, X v)
|
||||
% here we need to generate constraints p1 <c List<x>, p2 <c x
|
||||
% because x can become List<a?>:
|
||||
|
||||
% class Box<X>{}
|
||||
|
||||
% class Test{
|
||||
|
||||
% static <X> Box<X> add(Box<X> b, X x){return null;}
|
||||
% static <X> Box<X> empty(){return null;}
|
||||
% static <X> Box<Box<X>> empty2(){return null;}
|
||||
% public static void main(String args[]){
|
||||
% Box<?> b = null;
|
||||
% Box<? extends Box<?>> b2 = add(empty2(), b);
|
||||
% }
|
||||
% }
|
||||
|
||||
\section{Unify}\label{sec:unify}
|
||||
|
||||
%TODO: Remove lessdotC constraints. those have to be handeld during constraint generation
|
||||
% is capture conversion for methods in the same class unsovable? Can it be reduced to polymorphic recursion?
|
||||
% the other problem is, that there are infinite subtypes.
|
||||
% For example for a type X^Infinite<X>.Infinite<X>
|
||||
% here a correct subtype would be an instantiation of the class Omega extends Infinite<Omega>
|
||||
|
||||
The parameter types given to a generic method also affect their return type.
|
||||
During constraint generation the algorithm does not know the parameter types yet.
|
||||
We generate $\lessdotCC$ constraints and let \unify{} do the capture conversion.
|
||||
$\lessdotCC$ constraints are kept until they reach the form $\type{G} \lessdotCC \type{G}$ and a capture conversion is possible.
|
||||
|
||||
% A method has infinte possibilities of being called and there is no most general type.
|
||||
% P<X,Y> m(C<X> c, C<Y> c2)
|
||||
% depending on
|
||||
% A.P<A,A> <. A,B.P<A,B>
|
||||
|
||||
% % During the method call it is not sure what kind of return type is needed from the method.
|
||||
% % The method P<A,B> make(A a, B b)
|
||||
% % The type A,B.P<A,B> cannot be a subtype of P<X,X>
|
||||
% % But if A^X_X and B^X_X
|
||||
% % Could a constraint C<X> <. a? be expanded to a? = X^u?_l?.C<X>
|
||||
|
||||
% Why is there no most general type?
|
||||
% - the return type depends on the parameter types
|
||||
The most general type denotable in Java of a class $\exptype{C}{\ol{X}}$
|
||||
is $\wctype{\ol{X}}{C}{\ol{X}}$
|
||||
|
||||
%Is there a direct subtype of a type N including generics? e.g. a <c C<C<x>>
|
||||
% AND if yes! why is there not a most generic expression of a method head without the need of Capture Conversion?
|
||||
% Pair<X,Y> m(List<X> l, List<Y> l2) => X,Y.Pair<X,Y> m()
|
||||
% X.List<X> <. List<x>
|
||||
% because we want the most specfic return type and the least specific parameter types!
|
||||
|
||||
|
||||
A method is only equiped with generic parameters if they only appear in a <. T constraints
|
||||
Polymorphic recursion makes it impossible to infer a generic type who is called in a more specific way.
|
||||
Is it? Not ours for sure!
|
||||
|
||||
The problem is, that we don't know which type is the parameter of the method call.
|
||||
And a method with a parameter \texttt{List<? extends A>} can have an infinite number of subtypes. %Does it?
|
||||
% Y.List<Y> <c Z^List<x>.List<Z>
|
||||
% Y <. List<x>
|
||||
|
||||
% X,Y^List<X>.List<Y> <c Z^List<x>.List<Z>
|
||||
|
||||
% The idea is to hold out until the left side of a $\lessdotCC$ constraint is known to be a named type
|
||||
% and then check if the typing is still correct.
|
||||
|
||||
|
||||
The wildcard placeholders are used for intermediat types.
|
||||
It is not possible to create all super types of a type.
|
||||
The General rule only creates the ones expressable by Java syntax, which still are infinitly many in some cases \cite{TamingWildcards}.
|
||||
@ -93,46 +24,71 @@ $\set{\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \
|
||||
Those two constraints imply that we have to find a type replacement for type variable $\tv{a}$,
|
||||
which is a supertype of $\exptype{List}{String}$ aswell as $\exptype{List}{Integer}$.
|
||||
|
||||
The algorithm works in a recursive fashion.
|
||||
The input constraints are transformed until they reach a irreducible state,
|
||||
which the last step of the algorithm eventually transforms into a solution.
|
||||
A constraint set is convertable to a correct type solution if it only contains constraints of the form
|
||||
$\tv{a} \doteq \type{T}$ (where $\tv{a} \notin \text{tph}(\type{T})$) and $\tv{a} \lessdot \type{T}$.
|
||||
We call this \textit{Solved Form}.
|
||||
The input constraints are transformed until they reach a solved form which is then converted to a type solution.
|
||||
A constraint set is in solved form if it only consists of constraints of the form
|
||||
$\tv{a} \doteq \type{T}$ and $\tv{a} \lessdot \type{T}$.
|
||||
\unify{} is described as a nondeterministic algorithm.
|
||||
Some constraints allow for multiple transformations from which
|
||||
the algorithm has to pick the right one.
|
||||
There are also cases where there is more than on correct transformation and
|
||||
therefore more than one correct solution to the given input constraints.
|
||||
For that case still only one correct solution is returned by this specification of the algorithm.
|
||||
Our implementation of the algorithm considers this and tries every possible transformation option
|
||||
and gathers all possible type solutions.
|
||||
We skip the definition of this practice, because it is already described in \cite{TIforFGJ}
|
||||
and only needed for a proof of completeness.
|
||||
|
||||
The \unify{} algorithm applies conversions according to the subtyping rules (depicted in figure \ref{fig:subtyping}).
|
||||
At every step we try to find a reduction, which brings us closer to solved form without excluding any possible solution.
|
||||
|
||||
A $\bot \lessdot \type{T}$ constraint is always satisfied and can be ignored. It will be removed by the \rulename{Bot} rule.
|
||||
\textit{Examples:}
|
||||
\begin{itemize}
|
||||
\item A $\bot \lessdot \type{T}$ constraint is always satisfied and can be ignored. It will be removed by the \rulename{Bot} rule.
|
||||
For the type placeholder $\tv{a}$ in the constraint $\tv{a} \lessdot \bot$ only the $\bot$ type is a possible substitution,
|
||||
which is set by the \rulename{Pit} rule.
|
||||
|
||||
The \rulename{Reduce} rule represents the S-Exists type rule.
|
||||
\item The \rulename{Reduce} rule represents the S-Exists type rule.
|
||||
This rule uses wildcard placeholders ($\ol{\wtv{a}}$) to find a possible substitution for the wildcards on the right side.
|
||||
The constraint $\type{N} \lessdot \wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N'}$ is satisfied if
|
||||
there is a substitution $[\ol{T}/\ol{X}]\type{N} = \type{N'}$ with $\ol{T}$ inside the bounds $\ol{U}$ and $\ol{L}$.
|
||||
|
||||
\textbf{Example:}
|
||||
For example the constraint
|
||||
$\exptype{List}{\tv{a}} \lessdot \wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$
|
||||
The \rulename{Reduce} rule converts this to
|
||||
is converted to
|
||||
$\set{\tv{a} \doteq \wtv{x}, \wtv{x} \lessdot \type{Object}, \bot \lessdot \wtv{x} }$.
|
||||
After applying \rulename{Swap} and \rulename{Subst-WC} on $\tv{a} \doteq \wtv{x}$ we get
|
||||
$\set{\tv{a} \lessdot \type{Object}, \bot \lessdot \tv{a}}$ and can now apply the \rulename{Bot} rule.
|
||||
This leaves us with $\set{\tv{a} \lessdot \type{Object}}$.
|
||||
\item The \rulename{Erase} rule will remove redundant $\type{T} \doteq \type{T}$ constraints
|
||||
\item \rulename{Equals} ensures equality of two types by ensuring they are mutual subtypes.
|
||||
Constraints like $\wctype{\wildcard{X}{\tv{a}}{\tv{b}}}{List}{\rwildcard{X}} \doteq \wctype{\wildcard{Y}{\type{Object}}{\tv{String}}}{List}{\rwildcard{Y}}$
|
||||
are transformed to
|
||||
$\wctype{\wildcard{X}{\tv{a}}{\tv{b}}}{List}{\rwildcard{X}} \lessdot \wctype{\wildcard{Y}{\type{Object}}{\tv{String}}}{List}{\rwildcard{Y}}$
|
||||
and $\wctype{\wildcard{Y}{\type{Object}}{\tv{String}}}{List}{\rwildcard{Y}} \lessdot \wctype{\wildcard{X}{\tv{a}}{\tv{b}}}{List}{\rwildcard{X}}$.
|
||||
% The types $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and $\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}$
|
||||
% are equal.
|
||||
\end{itemize}
|
||||
|
||||
The \rulename{Erase} rule will remove redundant $\type{T} \doteq \type{T}$ constraints.
|
||||
But what about constraints like $\wctype{\wildcard{X}{\tv{a}}{\tv{b}}}{List}{\rwildcard{X}} \doteq \wctype{\wildcard{Y}{\type{Object}}{\tv{String}}}{List}{\rwildcard{Y}}$
|
||||
The \rulename{Equals} rule converts this to
|
||||
|
||||
% The equals rule is complicated, because
|
||||
% X.List<X> =. Y.List<Y> -> is the same
|
||||
% X^String.List<X> =. X.List<X> -> is not!
|
||||
|
||||
% T =. T => T <. T
|
||||
We define two types as equal if they are mutual subtypes of each other.
|
||||
%This relation is symmetric, reflexive and transitive by the definition of subtyping.
|
||||
%This definition is sufficient for proofing soundness.
|
||||
\begin{definition}{Type Equality:}\label{def:equal}
|
||||
$\Delta \vdash \type{S} = \type{T}$ if $\Delta \vdash \type{T} <: \type{S}$ and $\Delta \vdash \type{T} <: \type{S}$
|
||||
\end{definition}
|
||||
%This definition makes sense
|
||||
% The symmetric subtyping allows this type to be substit
|
||||
% We define types to be equal if they are symmetric subtypes.
|
||||
% This allows the substitution of these types with eachother.
|
||||
% If $\Delta \vdash \type{S} = \type{S'}$ and $\Delta \vdash \type{T} <: \type{T'}$,
|
||||
% then $\Delta \vdash [\type{S}/\type{S'}]\type{T} <: \type{T'}$.
|
||||
|
||||
|
||||
% Special cases: lessdotCC, Normalize/Tame rule,
|
||||
The $\lessdotCC$ constraints and the wildcard placeholders $\wtv{a}$ are kept as long as possible.
|
||||
%TODO: Example where lessdotCC constraints get spared until they can be captured
|
||||
The equality relation on Capture constraints is not reflexive.
|
||||
$(\type{T} \lessdotCC \type{S}) \neq (\type{T} \lessdotCC \type{S})$ eventhough it's the same constraint.
|
||||
|
||||
Capture conversion is done during the \unify{} algorithm.
|
||||
\unify{} has to make two promises to ensure soundness of our type inference algorithm.
|
||||
Capture conversion can only be applied at capture constraints.
|
||||
Free variables are not allowed to leave their scope.
|
||||
This is ensured by type variables which are not allowed to be assigned type holding free variables.
|
||||
|
||||
\subsection{Algorithm}
|
||||
|
||||
@ -155,15 +111,7 @@ The input constraints must be of the following format:
|
||||
\noindent
|
||||
Additional requirements:
|
||||
\begin{itemize}
|
||||
\item Every wildcard $\rwildcard{X} \in \Delta'$ has to have an unique name which is not defined anywhere in the constraint set $C$.
|
||||
\item The input only consists of $\lessdot$ constraints
|
||||
% \item No free variables in type parameters.
|
||||
% A constraint like $\tv{a} \lessdot \exptype{List}{\rwildcard{X}}$ is prohibited.
|
||||
% $\tv{a} \lessdot \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ is valid.
|
||||
\item the input is a list of constraints. It cannot be a set.
|
||||
A constraint set containing the constraint $\tv{a} \lessdot \type{T}$ twice
|
||||
is a different to one that contains it only once.
|
||||
%\item every wildcard is bound to its enclosing type.
|
||||
|
||||
\item All types have to be well-formed: $\wcNtype{\Delta}{N} \in C \implies \Delta_{in} \vdash \wcNtype{\Delta}{N} \ \ok$
|
||||
\item Naming scheme of every wildcard environment has to be the same.
|
||||
%TODO: We need this so that wildcard substitutions get the correct name. also the Equals rule needs this condition
|
||||
@ -369,37 +317,38 @@ $
|
||||
\quad \type{T} \ \text{is no wildcard placeholder}
|
||||
$
|
||||
\\\\
|
||||
% \rulename{Equals} %TODO
|
||||
% & $
|
||||
% \begin{array}[c]{l}
|
||||
% \wildcardEnv \vdash C \cup \, \set{ \type{N} \doteq \type{N'} } \\
|
||||
% \hline
|
||||
% \vspace*{-0.4cm}\\
|
||||
% \wildcardEnv \vdash C \cup \,
|
||||
% \set{
|
||||
% \type{N} \lessdot \type{N'}, \type{N'} \lessdot \type{N}
|
||||
% }
|
||||
% \end{array} % \quad \text{fv}(\type{N}) = \text{fv}(\type{N'}) = \emptyset
|
||||
% $
|
||||
% \\\\
|
||||
\rulename{Equals} %TODO
|
||||
& $
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \vdash C \cup \, \set{ \wctype{\Delta}{C}{\ol{T}} \doteq \wctype{\Delta}{C}{\ol{T'}} } \\
|
||||
\hline
|
||||
\vspace*{-0.4cm}\\
|
||||
\wildcardEnv \vdash C \cup \,
|
||||
\set{
|
||||
\pi(\ol{T}) \doteq \pi(\ol{T'} )
|
||||
%\ol{T} \doteq \ol{T'}
|
||||
}
|
||||
\end{array}
|
||||
\quad \begin{array}{l}
|
||||
\text{given a permutation}\ \pi\ \text{with:}\\
|
||||
\pi(\Delta) = \pi(\Delta')
|
||||
\end{array}
|
||||
$
|
||||
\\\\
|
||||
\rulename{Equals} %TODO
|
||||
& $
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \vdash C \cup \, \set{ \wcNtype{\Delta}{N} \doteq \wcNtype{\Delta'}{N'} } \\
|
||||
\hline
|
||||
\vspace*{-0.4cm}\\
|
||||
\wildcardEnv \vdash C \cup \,
|
||||
\set{
|
||||
\wcNtype{\Delta}{N} \lessdot \wcNtype{\Delta'}{N'}, \wcNtype{\Delta'}{N'} \lessdot \wcNtype{\Delta}{N}
|
||||
}
|
||||
\end{array} %\quad |\Delta| = |\Delta'|
|
||||
% \quad \text{fv}(\type{N}) = \text{fv}(\type{N'}) = \emptyset
|
||||
$
|
||||
\\\\
|
||||
% \rulename{Equals} %TODO
|
||||
% & $
|
||||
% \begin{array}[c]{l}
|
||||
% \wildcardEnv \vdash C \cup \, \set{ \wctype{\Delta}{C}{\ol{T}} \doteq \wctype{\Delta}{C}{\ol{T'}} } \\
|
||||
% \hline
|
||||
% \vspace*{-0.4cm}\\
|
||||
% \wildcardEnv \vdash C \cup \,
|
||||
% \set{
|
||||
% \pi(\ol{T}) \doteq \pi(\ol{T'} )
|
||||
% %\ol{T} \doteq \ol{T'}
|
||||
% }
|
||||
% \end{array}
|
||||
% \quad \begin{array}{l}
|
||||
% \text{given a permutation}\ \pi\ \text{with:}\\
|
||||
% \pi(\Delta) = \pi(\Delta')
|
||||
% \end{array}
|
||||
% $
|
||||
% \\\\
|
||||
\rulename{Erase}
|
||||
& $
|
||||
\begin{array}[c]{l}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user