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

Restructure and Cleanup Unify

Browse Source
This commit is contained in:
JanUlrich 2024-05-27 16:07:24 +02:00
parent 0f1e7d0199
commit 42d8afce35
2 changed files with 196 additions and 264 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
introduction.tex
View File

@ -489,8 +489,8 @@ exists to satisfy
$\exptype{List}{\type{A}} <: \exptype{List}{\type{X}}, $\exptype{List}{\type{A}} <: \exptype{List}{\type{X}},
\exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$. \exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$.
\textbf{Solution:} % \textbf{Solution:}
Capture Conversion during Unify. % Capture Conversion during Unify.
\item \item
\unify{} morphs a constraint set into a correct type solution \unify{} morphs a constraint set into a correct type solution
@ -566,10 +566,10 @@ $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
There is no solution for the subtype constraint: There is no solution for the subtype constraint:
$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$ $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$
\item \textbf{Free Variables cannot leaver their scope}: \item \label{challenge3} \textbf{Free Variables cannot leaver their scope}:
\begin{example} \begin{example}
Take the following Java program for example. Take the Java program in listing \ref{lst:mapExample} for example.
It maps every element of a list It maps every element of a list
$\expr{l} : \exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$ $\expr{l} : \exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
to a polymorphic \texttt{id} method. to a polymorphic \texttt{id} method.
@ -580,31 +580,25 @@ lambda expressions used in this example,
we can imagine that the constraints have to look something like this: we can imagine that the constraints have to look something like this:
\begin{minipage}{0.45\textwidth} \begin{minipage}{0.45\textwidth}
\begin{lstlisting}{java} \begin{lstlisting}[caption=List Map Example,label=lst:mapExample]
<X> List<X> id(List<X> l){ ... } <X> List<X> id(List<X> l){ ... }
List<List<?>> ls; List<List<?>> ls;
l2 = l.map(x -> id(x)); l2 = l.map(x -> id(x));
\end{lstlisting}\end{minipage} \end{lstlisting}\end{minipage}
\hfill \hfill
\begin{minipage}{0.45\textwidth} \begin{minipage}{0.45\textwidth}
\begin{constraintset} \begin{lstlisting}[style=constraints, caption=Constraints, label=lst:mapExampleCons]
$ (*@$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}$@*)
\begin{array}{l} (*@$\exptype{List}{\wtv{x}} \lessdot \tv{z},$@*)
\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}, \\ (*@$\exptype{List}{\tv{z}} \lessdot \tv{l2}$@*)
\exptype{List}{\wtv{x}} \lessdot \tv{z}, \\ \end{lstlisting}
\exptype{List}{\tv{z}} \lessdot \tv{l2}
\end{array}
$
\end{constraintset}
\end{minipage} \end{minipage}
The constraints The constraints
$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}, $\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}},
\exptype{List}{\wtv{x}} \lessdot \tv{z}$ \exptype{List}{\wtv{x}} \lessdot \tv{z}$
stem from the body of the lambda expression stem from the body of the lambda expression
\texttt{shuffle(x)}. \texttt{id(x)}.
\textit{For clarification:} This method call would be represented as the following expression in \letfj{}: \textit{For clarification:} This method call would be represented as the following expression in \letfj{}:
\texttt{let x1 :$\wctype{\rwildcard{A}}{List}{\rwildcard{A}}$ = x in id(x) :$\tv{z}$} \texttt{let x1 :$\wctype{\rwildcard{A}}{List}{\rwildcard{A}}$ = x in id(x) :$\tv{z}$}

432
unify.tex
View File

@ -25,7 +25,7 @@ Each calculation step of the algorithm is expressed as a transformation rule con
The input is shown above the line, the output below, and additional premises are displayed on the right side. The input is shown above the line, the output below, and additional premises are displayed on the right side.
If the wildcard environment $\wildcardEnv$ and the constraint set $C$ match the pattern declared as the input If the wildcard environment $\wildcardEnv$ and the constraint set $C$ match the pattern declared as the input
the transformation will reduce them into the specified output. the transformation will reduce them into the specified output.
The \rulename{Subst} rule for example takes a constraint set that has atleast one constraint of the form The \rulename{Subst} rule (figure \ref{fig:subst-rules}) for example takes a constraint set that has atleast one constraint of the form
$\ntv{a} \doteq \type{T}$ and replaces every occurence of $\ntv{a}$ by $\type{T}$ $\ntv{a} \doteq \type{T}$ and replaces every occurence of $\ntv{a}$ by $\type{T}$
in the wildcard environment $\wildcardEnv{}$ aswell as the remaining constraint set $C$. in the wildcard environment $\wildcardEnv{}$ aswell as the remaining constraint set $C$.
@ -93,8 +93,8 @@ The \rulename{Upper} and \rulename{Lower} conversions (figure \ref{fig:wildcard-
\rulename{Lower} has to check if the wildcard is part of the input wildcards $\Delta_{in}$. \rulename{Lower} has to check if the wildcard is part of the input wildcards $\Delta_{in}$.
If that is the case the wildcard can be part of the type solution and stays in the constraint set. If that is the case the wildcard can be part of the type solution and stays in the constraint set.
\textit{Note:} The subtype constraints in these rules are annotated with numbers $\lessdot_1$. \textit{Note:} The subtype constraints in these rules are annotated with numbers $\lessdot_1$.
All rule inputs containing subtype constraints $(\lessdot)$ are always meant for both, All rule inputs containing subtype constraints $(\lessdot)$ are always meant for both kinds,
subtype constraints and capture constraints ($\lessdotCC$). subtype ($\lessdot$) and capture constraints ($\lessdotCC$).
If multiple constraints are stated in the input format they will be annotated with numbers which map them to the constraints used in the output of the rule. If multiple constraints are stated in the input format they will be annotated with numbers which map them to the constraints used in the output of the rule.
Constraints with the same number stay the same kind. Constraints with the same number stay the same kind.
So if the input to \rulename{Upper} is $\rwildcard{A} \lessdotCC \type{G}$ the output will be something like $\type{U} \lessdotCC \type{G}$. So if the input to \rulename{Upper} is $\rwildcard{A} \lessdotCC \type{G}$ the output will be something like $\type{U} \lessdotCC \type{G}$.
@ -114,6 +114,16 @@ Note that the new generated constraint $\wtv{b} \lessdot \type{String}$ is a nor
%The type placeholders which are annotated as wildcard placeholders also stay wildcard placeholders. %The type placeholders which are annotated as wildcard placeholders also stay wildcard placeholders.
%The only rule that replaces wildcard type placeholders with regular placeholders is the \rulename{Normalize} rule. %The only rule that replaces wildcard type placeholders with regular placeholders is the \rulename{Normalize} rule.
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{Erase} rule will remove redundant $\type{T} \doteq \type{T}$ constraints
\rulename{Equals} ensures equality of two types by ensuring they are mutual subtypes.
We define two types as equal if they are mutual subtypes of each other.
\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}
\begin{figure} \begin{figure}
\begin{center} \begin{center}
\leavevmode \leavevmode
@ -433,6 +443,39 @@ $\tv{a} \lessdot \wctype{\wildcard{A}{\type{Integer}}{\type{Integer}}}{List}{\rw
\caption{Constraint reduce rules}\label{fig:reduce-rules} \caption{Constraint reduce rules}\label{fig:reduce-rules}
\end{figure} \end{figure}
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}$.
For example the constraint
$\exptype{List}{\tv{a}} \lessdot \wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$
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}}$.
The \unify{} algorithm applies a capture conversion by applying the \rulename{Capture} transformation when needed.
Capture conversion removes a types bounding environment $\Delta$ and adds the included wildcard definitions to the global environment $\wildcardEnv{}$.
Only the \rulename{Capture} transformation adds wildcards to the wildcard environment $\wildcardEnv{}$
and every added wildcard gets a fresh unique name.
This ensures the wildcard environment $\wildcardEnv{}$ never
gets the same wildcard twice.
\subsection{Branching Step}
\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.
\subsection{Adding Wildcards to the mix} \subsection{Adding Wildcards to the mix}
%\unify{} is able to create wildcard solutions even when the input set of constraints do not contain any wildcard variables. %\unify{} is able to create wildcard solutions even when the input set of constraints do not contain any wildcard variables.
%Input constraints originating from a completely untyped input program do not contain any existential types. %Input constraints originating from a completely untyped input program do not contain any existential types.
@ -550,61 +593,17 @@ The \texttt{concat} method takes two lists of the same generic type.
%TODO: Explain capture conversion %TODO: Explain capture conversion
\subsection{Description} %\subsection{Description}
The \unify{} algorithm tries to find a solution for a set of constraints like % The \unify{} algorithm tries to find a solution for a set of constraints like
$\set{\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}}$. % $\set{\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}}$.
Those two constraints imply that we have to find a type replacement for type variable $\tv{a}$, % 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}$. % which is a supertype of $\exptype{List}{String}$ aswell as $\exptype{List}{Integer}$.
The input constraints are transformed until they reach a solved form which is then converted to a type solution. % The \unify{} algorithm applies conversions according to the subtyping rules (depicted in figure \ref{fig:subtyping}).
A constraint set is in solved form if it only consists of constraints of the form % At every step we try to find a reduction, which brings us closer to solved form without excluding any possible solution.
$\tv{a} \doteq \type{T}$ and $\tv{a} \lessdot \type{T}$. % \textit{Examples:}
\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.
\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.
\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}$.
For example the constraint
$\exptype{List}{\tv{a}} \lessdot \wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$
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}
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 proving 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 %This definition makes sense
% The symmetric subtyping allows this type to be substit % The symmetric subtyping allows this type to be substit
% We define types to be equal if they are symmetric subtypes. % We define types to be equal if they are symmetric subtypes.
@ -612,13 +611,6 @@ We define two types as equal if they are mutual subtypes of each other.
% If $\Delta \vdash \type{S} = \type{S'}$ and $\Delta \vdash \type{T} <: \type{T'}$, % 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'}$. % then $\Delta \vdash [\type{S}/\type{S'}]\type{T} <: \type{T'}$.
\textbf{Wildcard Environment:}
Additional to a constraint set \unify{} holds a wildcard environment $\wildcardEnv{}$ keeping free variables.
The algorithm starts with an empty wildcard environment $\wildcardEnv{}$.
Only the \rulename{Capture} rule adds wildcards to that environment
and every added wildcard gets a fresh unique name.
This ensures the wildcard environment $\wildcardEnv{}$ never
gets the same wildcard twice.
% \subsection{Capture Conversion} % \subsection{Capture Conversion}
% % TODO: Describe Capture conversion % % TODO: Describe Capture conversion
@ -628,53 +620,6 @@ gets the same wildcard twice.
% Free variables are not allowed to leave their scope. % 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. % This is ensured by type variables which are not allowed to be assigned type holding free variables.
\textbf{Wildcard Placeholders:}
The vital part are the \rulename{Subst} and \rulename{Normalize} rules.
They assert that a normal type placeholder is never replaced by a type containing free variables.
\rulename{Normalize} replaces Wildcard placeholders with normal placeholders right before they get substituted by \rulename{Subst}.
The idea is to keep the possibility of replacing a wildcard placeholder with a free variable as long as possible.
As soon as they appear in a $\ntv{a} \doteq \type{T}$ constraint they have to be replaced with normal placeholders.
A type solution for a normal type placeholder will never contain free variables.
This is needed to guarantee well-formed type solutions and also keep free variables inside their scope.
\begin{example}{Free variables must not leave the scope of the surrounding \texttt{let} statement}
\noindent
\begin{minipage}{0.40\textwidth}
\begin{lstlisting}
m(l) = let v = l in v.get()
\end{lstlisting}
\end{minipage}%
\hfill
\begin{minipage}{0.59\textwidth}
\begin{constraintset}
$\tv{l} \lessdot \tv{v}, \tv{v} \lessdotCC \exptype{List}{\wtv{x}},
\wtv{x} \lessdot \tv{r}$
\end{constraintset}
\end{minipage}
Lets assume the variables \texttt{l} and \texttt{v}
get the type $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$ assigned to them.
After application of the \rulename{Capture} and \rulename{SubstWC} rules the constraint set looks like this:
$\begin{array}[c]{l}
\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}, \wtv{x} \lessdot \ntv{r}
\\
\hline
\vspace*{-0.4cm}\\
\wildcard{X}{\type{Object}}{\type{String}} \vdash \wtv{x} \doteq \rwildcard{X}, \rwildcard{X} \lessdot \ntv{r}
\end{array}
$
Replacing $\tv{r}$ with $\rwildcard{X}$ would solve the constraint set but lead to the method type
\texttt{X m(List<? super String> l)} which makes no sense.
The normal type placeholder $\ntv{r}$ has to be replaced by a type without free type variables
($\ntv{r} \doteq \type{Object}$) leading to
\texttt{Object m(List<? super String> l)}.
\end{example}
\subsection{Algorithm} \subsection{Algorithm}
%\newcommand{\tw}[1]{\tv{#1}_?} %\newcommand{\tw}[1]{\tv{#1}_?}
@ -779,10 +724,6 @@ and a name $\mathtt{X}$.
The \rulename{Tame} rule eliminates wildcards. %TODO The \rulename{Tame} rule eliminates wildcards. %TODO
This is done by setting the upper and lower bound to the same value. This is done by setting the upper and lower bound to the same value.
\unify{} applies a capture conversion everywhere it is possible (see \rulename{Capture} rule).
Capture conversion removes a types bounding environment $\Delta$ and adds the included wildcard definitions to the global environment $\wildcardEnv{}$.
%Type variables used in its type parameters are now bound to a global scope and not locally anymore.
The \rulename{match} rule generates fresh wildcards $\overline{\wildcard{A}{\tv{u}}{\tv{l}}}$. The \rulename{match} rule generates fresh wildcards $\overline{\wildcard{A}{\tv{u}}{\tv{l}}}$.
Their upper and lower bounds are fresh type variables. Their upper and lower bounds are fresh type variables.
@ -879,19 +820,6 @@ which are used for the upper and lower bounds.
% if there are a <. List<x?> constraints remaining in the end, then this can be a sign of a irregular input constraint set. % if there are a <. List<x?> constraints remaining in the end, then this can be a sign of a irregular input constraint set.
\unify{} must not replace normal type placeholders with free variables
except variables initially passed by $\Delta_{in}$.
The \rulename{Subst} rule checks if a type $\type{T}$ contains any
free variables or wildcard placeholders before replacing a normal type placeholder with it.
This ensures that free variables are never substituted for normal type placeholders.
\rulename{Subst-WC} does not need to do that and can freely replace wildcard placehodlers with types despite their free variables.
We do not keep replacements for wildcard placeholders and they also will not show up in the final type solution.
If the \rulename{Subst} rule is not applicable then either the \rulename{Normalize}
or \rulename{Contract} transformation has to be used to remove wildcard placeholders and
wildcards.
\begin{figure} \begin{figure}
\begin{center} \begin{center}
\leavevmode \leavevmode
@ -944,12 +872,57 @@ C \cup [\type{U}/\type{A}]\set{\ntv{a} \doteq \type{T}, \type{L} \doteq \type{U}
\caption{Substitution rules}\label{fig:subst-rules} \caption{Substitution rules}\label{fig:subst-rules}
\end{figure} \end{figure}
\unify{} must not replace normal type placeholders with free variables
except variables initially passed by $\Delta_{in}$.
The \rulename{Subst} rule checks if a type $\type{T}$ contains any
free variables or wildcard placeholders before replacing a normal type placeholder with it.
%This ensures that free variables are never substituted for normal type placeholders.
This ensures that a normal type placeholder is never replaced by a type containing free variables.
A type solution for a normal type placeholder will never contain free variables.
This is needed to guarantee well-formed type solutions and also keep free variables inside their scope
(see challenge \ref{challenge3}).
\rulename{Subst-WC} does not need to do that and can freely replace wildcard placehodlers with types despite their free variables.
We do not keep replacements for wildcard placeholders and they will not show up in the final type solution.
If the \rulename{Subst} rule is not applicable then either the \rulename{Normalize}
or \rulename{Contract} transformation has to be used to remove wildcard placeholders and
wildcards.
% \begin{example}{Free variables must not leave the scope of the surrounding \texttt{let} statement}
% \noindent
% \begin{minipage}{0.40\textwidth}
% \begin{lstlisting}
% m(l) = let v = l in v.get()
% \end{lstlisting}
% \end{minipage}%
% \hfill
% \begin{minipage}{0.59\textwidth}
% \begin{constraintset}
% $\tv{l} \lessdot \tv{v}, \tv{v} \lessdotCC \exptype{List}{\wtv{x}},
% \wtv{x} \lessdot \tv{r}$
% \end{constraintset}
% \end{minipage}
% Lets assume the variables \texttt{l} and \texttt{v}
% get the type $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$ assigned to them.
% After application of the \rulename{Capture} and \rulename{SubstWC} rules the constraint set looks like this:
% all possible variations have to be converted % $\begin{array}[c]{l}
There are n different rules to deal with $\type{N} \lessdot \type{N}$ constraints. % \wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}, \wtv{x} \lessdot \ntv{r}
Prepare, Capture, Reduce, Trim, Clear, Exclude, Adapt % \\
% \hline
% \vspace*{-0.4cm}\\
% \wildcard{X}{\type{Object}}{\type{String}} \vdash \wtv{x} \doteq \rwildcard{X}, \rwildcard{X} \lessdot \ntv{r}
% \end{array}
% $
% Replacing $\tv{r}$ with $\rwildcard{X}$ would solve the constraint set but lead to the method type
% \texttt{X m(List<? super String> l)} which makes no sense.
% The normal type placeholder $\ntv{r}$ has to be replaced by a type without free type variables
% ($\ntv{r} \doteq \type{Object}$) leading to
% \texttt{Object m(List<? super String> l)}.
% \end{example}
% % TODO: % % TODO:
% a <c C<X> % a <c C<X>
@ -1163,42 +1136,6 @@ $\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \cap \Delta_{in}
\ol{X} \notin \wildcardEnv \cup \Delta,\, \Delta' = \Delta \cap \text{fv}([\ol{T}/\ol{X}]\ol{N}) \ol{X} \notin \wildcardEnv \cup \Delta,\, \Delta' = \Delta \cap \text{fv}([\ol{T}/\ol{X}]\ol{N})
\end{array} \end{array}
$ $
% \\\\
% \hline \\
% \rulename{SameW}
% & $
% \begin{array}[c]{l}
% \wildcardEnv \vdash
% C \cup \type{G} \lessdot \wtv{a}\\
% \hline
% \wildcardEnv \vdash
% C \cup \set{
% \wtv{a} \doteq \type{G}
% }
% \end{array}
% $
% \\\\
% \cdashline{1-2} \\
% \rulename{\generalizeRule{}W} %TODO: Change description for step 2!
% & $
% \begin{array}[c]{l}
% \wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \wtv{a}\\
% \hline
% \wildcardEnv \vdash C \cup \set{\wctype{\Delta}{C}{\ol{T}} \lessdot \wtv{a},
% \wtv{a} \doteq \wctype{\overline{\wildcard{X}{\wtv{u}}{\wtv{l}}}}{C}{\overline{\rwildcard{X}}},
% %\overline{\tv{l} \lessdot \tv{u}}, % not needed, due to subst and reduce rule which are used afterwards
% \overline{\wtv{u} \lessdot \type{S}}
% }
% \end{array} \quad \begin{array}[c]{l}
% \texttt{class} \ \exptype{C}{\ol{X \triangleleft \type{S}}} \triangleleft \exptype{D}{\ol{N}} \\
% \text{fresh}\ \overline{\wildcard{X}{\wtv{u}}{\wtv{l}}}
% \end{array}
% $
% %The idea behind the GeneralW rule is, that a constraint X.Pair<X,X> <. a? can be resolved:
% % X.Pair<X,X> <. Y,Z.Pair<Y,Z>
% % X =. y, X =. z, y <. yu?, z <. zu?, yl? <. y, zl? <. z
% % X <. yu?, X <. zu?, yl? <. X, zl? <. X
% % ???
\end{tabular} \end{tabular}
} }
\end{center} \end{center}
@ -1278,6 +1215,11 @@ $\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \cap \Delta_{in}
\label{fig:step2-rules2} \label{fig:step2-rules2}
\end{figure} \end{figure}
Figure \ref{fig:step2-rules2} are special transformations aimed at free variables defined in the input environment $\Delta_{in}$.
Usually \rulename{Upper} takes care of $\rwildcard{X} \lessdot \tv{a}$ constraints,
but if $\rwildcard{X}$ is an element of $\Delta_{in}$ we can also treat it as a regular type.
This leaves us with the two possibilities \rulename{Subst-X} and \rulename{Gen-X} which is the same as \rulename{Upper}.
\begin{figure} \begin{figure}
\begin{center} \begin{center}
\leavevmode \leavevmode
@ -1415,59 +1357,55 @@ $\begin{array}{c}
\end{tikzpicture} \end{tikzpicture}
\end{NiceTabular} \end{NiceTabular}
\subsection{Capture Conversion during Unification} % \subsection{Capture Conversion during Unification}
% The \unify{} algorithm applies a capture conversion when needed. % % The \unify{} algorithm applies a capture conversion when needed.
% A constraint of the form $\wcNtype{\Delta'}{N} \lessdot \type{T}$, % % A constraint of the form $\wcNtype{\Delta'}{N} \lessdot \type{T}$,
% where $\text{fv}(\type{T}) \neq \emptyset$ is not solvable without capture conversion. % % where $\text{fv}(\type{T}) \neq \emptyset$ is not solvable without capture conversion.
% \unify{} converts those constraints to $\type{N} \lessdot \type{T}$. % % \unify{} converts those constraints to $\type{N} \lessdot \type{T}$.
% This is only possible for subtype constraints which originated from a method call. % % This is only possible for subtype constraints which originated from a method call.
Capture conversion only works with constraints containing free variables. % The challenge for a type inference algorithm is to apply capture conversion during type inference.
It also introduces fresh free variables into the constraint set. % Given a program
Both have to be regulated. % \begin{verbatim}
% class TypeInferenceExample{
% m(l){
% return swap(make(l));
% }
% }
% \end{verbatim}
The challenge for a type inference algorithm is to apply capture conversion during type inference. % During the time of the type inference algorithm the type of the parameter \texttt{l} is not known.
Given a program % Due to the call to the method \texttt{make} it is clear that it has to be a subtype of
\begin{verbatim} % \texttt{List}.
class TypeInferenceExample{ % These subtype relations are expressed with constraints.
m(l){ % $\tv{l} \lessdot \exptype{List}{\tv{a}}$ in this case.
return swap(make(l)); % $\tv{l}$ and $\tv{a}$ are type placeholders.
} % $\tv{l}$ is a type placeholder for the method parameter \texttt{l}.
}
\end{verbatim}
During the time of the type inference algorithm the type of the parameter \texttt{l} is not known. % One correct solution for this constraint is the substitution $\tv{l} \doteq \exptype{List}{\type{Object}}$,
Due to the call to the method \texttt{make} it is clear that it has to be a subtype of % which leads to the program:
\texttt{List}. % \begin{verbatim}
These subtype relations are expressed with constraints. % class TypeInferenceExample{
$\tv{l} \lessdot \exptype{List}{\tv{a}}$ in this case. % Pair<Object, Object> m(List<Object> l){
$\tv{l}$ and $\tv{a}$ are type placeholders. % return swap(make(l));
$\tv{l}$ is a type placeholder for the method parameter \texttt{l}. % }
% }
% \end{verbatim}
One correct solution for this constraint is the substitution $\tv{l} \doteq \exptype{List}{\type{Object}}$, % But $\tv{l} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ is also a possible solution.
which leads to the program: % Eventhough the constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\tv{a}}$
\begin{verbatim} % is not solvable.
class TypeInferenceExample{ % But when we apply capture conversion to create $\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\tv{a}}$
Pair<Object, Object> m(List<Object> l){ % we can substitute $\tv{a} \doteq \rwildcard{Y}$.
return swap(make(l));
}
}
\end{verbatim}
But $\tv{l} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ is also a possible solution. % The \unify{} algorithm has to apply capture conversions during the unification of type constraints.
Eventhough the constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\tv{a}}$
is not solvable.
But when we apply capture conversion to create $\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\tv{a}}$
we can substitute $\tv{a} \doteq \rwildcard{Y}$.
The \unify{} algorithm has to apply capture conversions during the unification of type constraints. % But this renders additional problems:
% \begin{itemize}
But this renders additional problems: % \item Capture conversion is not allowed for every constraint.
\begin{itemize} % \item Capture Converted variables are not allowed to leave their scope
\item Capture conversion is not allowed for every constraint. % \item \unify{} generates type substitution which cannot be translated to Java types.
\item Capture Converted variables are not allowed to leave their scope % \end{itemize}
\item \unify{} generates type substitution which cannot be translated to Java types.
\end{itemize}
\subsection{Completeness}\label{sec:completeness} \subsection{Completeness}\label{sec:completeness}
@ -1528,43 +1466,43 @@ The new constraint generated by the adopt rule may be eliminated by the match ru
The adopt rule still needs to be applied only once per constraint. The adopt rule still needs to be applied only once per constraint.
\textbf{Eliminating Wildcards} % \textbf{Eliminating Wildcards}
Wildcards that have the same upper and lower bounds can be removed. % Wildcards that have the same upper and lower bounds can be removed.
This is done by the \rulename{Crunch} rule. % This is done by the \rulename{Crunch} rule.
\textit{Example:} The type $\wctype{\wildcard{X}{\type{String}}{\type{String}}}{List}{\rwildcard{X}}$ % \textit{Example:} The type $\wctype{\wildcard{X}{\type{String}}{\type{String}}}{List}{\rwildcard{X}}$
becomes $\exptype{List}{\type{String}}$. % becomes $\exptype{List}{\type{String}}$.
\begin{tabular}[t]{l@{~}l} % \begin{tabular}[t]{l@{~}l}
\\\\ % \\\\
\rulename{Crunch} % \rulename{Crunch}
& $\begin{array}[c]{@{}ll} % & $\begin{array}[c]{@{}ll}
\begin{array}[c]{l} % \begin{array}[c]{l}
\wildcardEnv \vdash C \cup \, \set{ \tv{a} \doteq \wctype{\Delta', \set{\overline{\wildcard{X}{\type{U}}{\type{L}}}}}{C}{\ol{S}} } \\ % \wildcardEnv \vdash C \cup \, \set{ \tv{a} \doteq \wctype{\Delta', \set{\overline{\wildcard{X}{\type{U}}{\type{L}}}}}{C}{\ol{S}} } \\
\hline % \hline
\vspace*{-0.4cm}\\ % \vspace*{-0.4cm}\\
\wildcardEnv \vdash % \wildcardEnv \vdash
C \cup \set{ \tv{a} \doteq \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}} % C \cup \set{ \tv{a} \doteq \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}}
\end{array} % \end{array}
&\begin{array}[c]{l} % &\begin{array}[c]{l}
\ol{U} = \ol{L} % \ol{U} = \ol{L}
\end{array} % \end{array}
\end{array}$ % \end{array}$
\\\\ % \\\\
\rulename{Crunch} % \rulename{Crunch}
& $\begin{array}[c]{@{}ll} % & $\begin{array}[c]{@{}ll}
\begin{array}[c]{l} % \begin{array}[c]{l}
\wildcardEnv \vdash C \cup \, \set{ \tv{a} \lessdot \wctype{\Delta', \set{\overline{\wildcard{X}{\type{U}}{\type{L}}}}}{C}{\ol{S}} } \\ % \wildcardEnv \vdash C \cup \, \set{ \tv{a} \lessdot \wctype{\Delta', \set{\overline{\wildcard{X}{\type{U}}{\type{L}}}}}{C}{\ol{S}} } \\
\hline % \hline
\vspace*{-0.4cm}\\ % \vspace*{-0.4cm}\\
\wildcardEnv \vdash % \wildcardEnv \vdash
C \cup \set{ \tv{a} \lessdot \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}} % C \cup \set{ \tv{a} \lessdot \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}}
\end{array} % \end{array}
&\begin{array}[c]{l} % &\begin{array}[c]{l}
\ol{U} = \ol{L} % \ol{U} = \ol{L}
\end{array} % \end{array}
\end{array}$ % \end{array}$
\end{tabular} % \end{tabular}
% After applying the GenDelta and GenSigma rules unifiers $\sigma$ do not contain % After applying the GenDelta and GenSigma rules unifiers $\sigma$ do not contain