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

Restructure, Add Explanation für Wildcard Reduce Rules and Unify Intro

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-05-17 11:56:35 +02:00
parent ed8895f0b5
commit 724f9ab328
4 changed files with 267 additions and 232 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
constraints.tex
View File

@ -1,7 +1,9 @@
\section{Capture Constraints}
%TODO: General Capture Constraint explanation
Capture Constraints are not reflexive.
The equality relation on Capture constraints is not reflexive.
A capture constraint is never equal to another capture constraint even when structurally the same
($\type{T} \lessdotCC \type{S} \neq \type{T} \lessdotCC \type{S}$).
This is necessary to solve challenge \ref{challenge:1}.
A capture constraint is bound to a specific let statement.
For example the statement \lstinline{let x = v in x.get()}

25
introduction.tex
View File

@ -50,6 +50,8 @@ Whereas our type inference algorithm is based on a Featherweight Java calculus \
The central piece of this type inference algorithm, the \unify{} process, is described with implication rules (chapter \ref{sec:unify}).
We try to keep the branching at a minimal amount to improve runtime behavior.
Also the transformation steps of the \unify{} algorithm are directly related to the subtyping rules of our calculus.
There are no informal parts in our \unify{} algorithm.
It solely consist out of transformation rules which are bound to simple checks.
\item[Java Type Inference]
Standard Java provides type inference in a restricted form % namely {Local Type Inference}.
@ -100,13 +102,14 @@ Here our type inference algorithm based on unification is needed.
\subsection{Conclusion}
%\subsection{Conclusion}
% Additions: TODO
% - Global Type Inference Algorithm, no type annotations are needed
% - Soundness Proof
% - Easy to implement
% - Capture Conversion support
% - Existential Types support
Our contributions are
\begin{itemize}
\item
We introduce the language \tifj{} (chapter \ref{sec:tifj}).
@ -366,19 +369,6 @@ A subtype constraint is satisfied if the left side is a subtype of the right sid
Subtype constraints and type placeholders act the same as the ones used in \emph{Type Inference for Featherweight Generic Java} \cite{TIforFGJ}.
The novel capture constraints and wildcard placeholders are needed for method invocations involving wildcards.
Our \unify{} process uses a similar concept as the standard unification by Martelli and Montanari \cite{MM82},
consisting of terms, relations and variables.
Instead of terms we have types of the form $\exptype{C}{\ol{T}}$ and
the variables are called type placeholders.
The input consist out of subtype relations.
The goal is to find a solution (an unifier) which is a substitution for type placeholders
which satisfies all input subtype constraints.
Types are reduced until they %either reach a discrepancy like $\type{String} \doteq \type{Integer}$
reach a form like $\tv{a} \doteq \type{T}$.
Afterwards \unify{} substitutes type placeholder $\tv{a}$ with $\type{T}$.
This is done until a substitution for all type placeholders and therefore a valid solution is reached.
The reduction and substitutions are done in the first step of the algorithm.
\begin{recap}\textbf{TI for FGJ without Wildcards:}
\TFGJ{} generates subtype constraints $(\type{T} \lessdot \type{T})$ consisting of named types and type placeholders.
For example the method invocation \texttt{concat(l, new Object())} generates the constraints
@ -456,13 +446,6 @@ $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype
\subsection{Challenges}\label{challenges}
%TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
The introduction of wildcards adds additional challenges.
% we cannot replace every type variable with a wildcard
Type variables can also be used as type parameters, for example
$\exptype{List}{String} \lessdot \exptype{List}{\tv{a}}$.
A problem arises when replacing type variables with wildcards.
% Wildcards are not reflexive.
% ( on the equals property ), every wildcard has to be capture converted when leaving its scope

4
tRules.tex
View File

@ -374,7 +374,7 @@ $\begin{array}{l}
\\
\hline
\vspace*{-0.3cm}\\
\texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \} : \mathtt{\Pi}
\mathtt{\Pi} \vdash \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \}
\end{array}
\end{array}$
%\\[1em]
@ -386,7 +386,7 @@ $\begin{array}{l}
\\
\hline
\vspace*{-0.3cm}\\
\overline{D : \mathtt{\Pi}}
\mathtt{\Pi} \vdash \overline{D}
\end{array}
\end{array}$
\end{center}

466
unify.tex
View File

@ -6,19 +6,128 @@
% the algorithm only removes wildcards, never adds them
\section{Unify}\label{sec:unify}
Our \unify{} process uses a similar concept as the standard unification by Martelli and Montanari \cite{MM82},
consisting of terms, relations and variables.
Instead of terms we have types of the form $\exptype{C}{\ol{T}}$ and
the variables are called type placeholders.
The input consist out of subtype relations.
The goal is to find a solution (an unifier) which is a substitution for type placeholders
which satisfies all input subtype constraints.
Types are reduced until they %either reach a discrepancy like $\type{String} \doteq \type{Integer}$
reach a form like $\tv{a} \doteq \type{T}$.
Afterwards \unify{} substitutes type placeholder $\tv{a}$ with $\type{T}$.
This is done until a substitution for all type placeholders and therefore a valid solution is reached.
The reduction and substitutions are done in the first step of the algorithm.
The algorithms state consists out of a wildcard environment and a constraint set ($\wildcardEnv \vdash C$).
Initially they are set to $\Delta_{in}$ and the input constraints.
Each calculation step of the algorithm is expressed as a transformation rule consisting of three parts.
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
the transformation will reduce them into the specified output.
The \rulename{Subst} rule for example takes a constraint set that has atleas one constraint of the form
$\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$.
The \rulename{Upper} and \rulename{Lower} conversions (figure \ref{fig:wildcard-rules}) replace wildcards with their respective bounds when appearing in a subtype constraint.
\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.
\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,
subtype constraints and capture constraints ($\lessdotCC$) aswell.
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.
So if the input to \rulename{Upper} is $\rwildcard{A} \lessdotCC \type{G}$ the output will be something like $\type{U} \lessdotCC \type{G}$.
If the input is a normal subtype constraint the output has to be a normal subtype constraint too.
%TODO: Rephrase
%The reason being that capture constraints are treated like regular subtype constraints in these rules.
%All transformations for subtype constraints work for capture constraints aswell.
%For clarification Subtype constraints are marked with a number.
But the \rulename{Adopt} rule for example takes multiple subtype constraints and also adds a new one.
Here the numbered annotations are necessary.
\textit{Example:} Having the constraints
$\ntv{a} \lessdotCC \wtv{b}, \ntv{a} \lessdot \type{String}, \wtv{b} \lessdot \type{Object}$
would lead to
$\wtv{b} \lessdot \type{String}, \ntv{a} \lessdotCC \wtv{b}, \ntv{a} \lessdot \type{String}, \wtv{b} \lessdotCC \type{Object}$
after applying \rulename{Adopt}.
Note that the new generated constraint $\wtv{b} \lessdot \type{String}$ is a normal subtype constraint.
%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.
\begin{figure}
\begin{center}
\leavevmode
\fbox{
\begin{tabular}[t]{l@{~}l}
\rulename{Upper}
& $
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdot_1 \type{G} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdot_1 \type{G} }
\end{array}
$
\\\\
\rulename{Lower}
& $
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot_1 \type{A} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot_1 \type{L} }
\end{array}
$
\\\\
\rulename{Lower}
& $
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \ntv{a} \lessdot_1 \type{A} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \ntv{a} \lessdot_1 \type{L} }
\end{array} \quad \type{A} \notin \Delta_{in}
$
\\\\
\rulename{Bot}
& $
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \bot \lessdot \type{T} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash C
\end{array}
$
\quad
\rulename{Pit}
$
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \bot } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash C \cup \set{ \tv{a} \doteq \bot }
\end{array}
$
\\\\
\end{tabular}}
\end{center}
\caption{Wildcard reduce rules}\label{fig:wildcard-rules}
\end{figure}
\subsection{Adding Wildcards to the mix}
Input constraints originating from a completely untyped input program do not contain any existential types.
Those are added during \unify{}.
The only parts where existential types are created are the \rulename{Match} and \rulename{General} rules.
Existential types can only be a supertype of normal types and never a subtype.
Except when used as an argument to a method invocation (see discussion in chapter \ref{sec:completeness}).
\unify{} works with the principle that type terms are reduced until constraints
of the form $\tv{a} \doteq \type{T}$ remain and we have a type solution.
This is for example done by the \rulename{Reduce} transformation, which works according to the S-Exists subtyping rule.
Existential types are created during the unificaiton process by the \rulename{Same} rule.
This rule always comes with a substitution and a \rulename{Reduce} transformation.
\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.
%Those are added during \unify{}.
Wildcard types are added preemptively and if necessary can be removed later down the line.
The parts where existential types are created are the \rulename{Match} and \rulename{General} transformations.
Everytime a constraint of the form $\type{T} \lessdot \tv{a}$ occurs,
it could be possible that a wildcard type for $\tv{a}$ is needed.
For example the constraint $\exptype{List}{\type{String}} \lessdot \tv{a}$
results in $\tv{a} \doteq \wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}$.
The upper and lower bounds of the freshly generated wildcard $\rwildcard{X}$ are type placeholders.
If a second constraint like $\tv{a} \lessdot \exptype{List}{\type{String}}$
exists the wildcard $\rwildcard{X}$ has to be removed by setting both lower and upper bound to $\type{String}$.
\textit{Example:}
\begin{displaymath}
@ -186,31 +295,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'}$,
% then $\Delta \vdash [\type{S}/\type{S'}]\type{T} <: \type{T'}$.
\textbf{Capture Constraints:}
The equality relation on Capture constraints is not reflexive.
A capture constraint is never equal to another capture constraint even when structurally the same
($\type{T} \lessdotCC \type{S} \neq \type{T} \lessdotCC \type{S}$).
An implementation of the algorithm has to take this into account.
All constraints are stored in a set and there are no dublicates of subtype constraints in a constraint set.
Capture constraints however have to be stored as a list or have an unique number assigned
so that duplicates don't get automatically discarded.
Capture constraints are treated like regular subtype constraints.
All transformations for subtype constraints work for capture constraints aswell.
For clarification Subtype constraints are marked with a number.
Constraints with the same number stay the same type.
Newly created subtype constraints are always regular subtype constrains unless stated otherwise.
The \rulename{Adopt} rule for example takes multiple subtype constraints and adds a new one.
Having the constraints
$\ntv{a} \lessdotCC \wtv{b}, \ntv{a} \lessdot \type{String}, \wtv{b} \lessdot \type{Object}$
would lead to
$\wtv{b} \lessdot \type{String}, \ntv{a} \lessdotCC \wtv{b}, \ntv{a} \lessdot \type{String}, \wtv{b} \lessdotCC \type{Object}$
after applying \rulename{Adopt}.
The new generated constraint $\wtv{b} \lessdot \type{String}$ is a normal subtype constraint.
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.
\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{}$.
@ -285,9 +369,8 @@ and a set of constraints $C = \set{ \type{T} \lessdot \type{T}, \type{T} \lessdo
Set of unifiers $Uni = \set{\sigma_1, \ldots, \sigma_n}$ and an environment $\Delta$
\end{description}
Each calculation step of the algorithm is expressed as a transformation rule.
% TODO: Explain syntax of the transformation steps
The transformation steps are not applied all at once but in a specific order:
%The transformation steps are not applied all at once but in a specific order:
\unify{} executes the following steps until a type solution is found:
\begin{description}
\item[Step 1:]
Apply the rules depicted in the figures \ref{fig:normalizing-rules}, \ref{fig:reduce-rules} and \ref{fig:wildcard-rules} exhaustively,
@ -577,86 +660,6 @@ Prepare, Capture, Reduce, Trim, Clear, Exclude, Adapt
%The capture constraints are preserved when applying the \rulename{Upper} rule.
% This is legal: a T <c S constraint indicates a let-statement can be inserted. Therefore there must exist a type T' with T <. T' <c S
\begin{figure}
\begin{center}
\leavevmode
\fbox{
\begin{tabular}[t]{l@{~}l}
% \rulename{normalize}
% & $
% \begin{array}[c]{l}
% \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \rwildcard{A} \doteq \rwildcard{B} } \\
% \hline
% \vspace*{-0.4cm}\\
% \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \type{L} \doteq \type{U} , \type{U} \doteq \type{U'}, \type{L} \doteq \type{L'} }
% \end{array}
% $
% \\\\
\rulename{Upper}
& $
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdot_1 \type{G} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdot_1 \type{G} }
\end{array}
$
% \quad \quad
% \begin{array}[c]{l} %TODO: can the second part be removed by adding a X.C<X> <. C<a?> constraint at method invocation?
% \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdotCC \type{G} } \\
% \hline
% \vspace*{-0.4cm}\\
% \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdotCC \type{G} }
% \end{array}
% $
\\\\
\rulename{Lower}
& $
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot_1 \type{A} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot_1 \type{L} }
\end{array}
$
\\\\
\rulename{Lower}
& $
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \ntv{a} \lessdot_1 \type{A} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \ntv{a} \lessdot_1 \type{L} }
\end{array} \quad \type{A} \notin \Delta_{in}
$ %TODO: a <. X with X in Delta_in => a =. X
% other possibliity: is it allowed to see X extends List<X> as class X extends List<X> {}
% other way round: every class declaration comes in Delta_in
\\\\
\rulename{Bot}
& $
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \bot \lessdot \type{T} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash C
\end{array}
$
\quad
\rulename{Pit}
$
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \bot } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash C \cup \set{ \tv{a} \doteq \bot }
\end{array}
$
\\\\
\end{tabular}}
\end{center}
\caption{Wildcard reduce rules}\label{fig:wildcard-rules}
\end{figure}
\begin{figure}
\begin{center}
\leavevmode
@ -855,85 +858,6 @@ Prepare, Capture, Reduce, Trim, Clear, Exclude, Adapt
\end{array}
$
\\\\
\rulename{Prepare} %The lessdotCC constraint only ensures that the left side looses its wildcardEnvironment.
%It does not ensure that the left side doesn't contain free variables. If you want to ensure that you have to give the left side a normal placeholder
&
$
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \wctype{\Delta'}{C}{\ol{T}} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdotCC \wctype{\Delta'}{C}{\ol{T}} } \\
\end{array}
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin{array}[c]{l}
\text{fv}(\wctype{\Delta'}{C}{\ol{T}}) \subseteq \Delta_{in}
\end{array}
\end{array}
$
\\\\
\rulename{Trim}
&
$
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\Delta,\Delta'}{C}{\ol{S}} \lessdot \type{T} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} } \\
\end{array}
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin{array}[c]{l}
\text{fv}(\ol{S}) \cap \Delta' = \emptyset
\end{array}
\end{array}
$
\\\\
\rulename{Clear}
&
$
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}} \vdash
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} } \\
\hline
\vspace*{-0.4cm}\\
\subst{\type{U}}{\rwildcard{A}}\wildcardEnv \vdash
[\type{U}/\rwildcard{A}]C \cup \, [\type{U}/\rwildcard{A}]\set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T}, \type{U} \doteq \type{L} } \\
\end{array}
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin{array}[c]{l}
\Delta \neq \emptyset\\
\rwildcard{A} \in \text{fv}(\type{T})
\end{array}
\end{array}
$
\\\\
\rulename{Exclude}
&
$
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} } \\
\hline
\vspace*{-0.4cm}\\
\subst{\tv{a}}{\wtv{a}}\wildcardEnv \vdash
[\tv{a}/\wtv{a}]C \cup \, [\tv{a}/\wtv{a}]\set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T}, \type{U} \doteq \type{L} } \\
\end{array}
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin{array}[c]{l}
\Delta \neq \emptyset\\
\wtv{a} \in \text{fv}(\type{T}), \tv{a} \ \text{fresh}
\end{array}
\end{array}
$
\\\\
\rulename{Adopt}
& $
\begin{array}[c]{@{}ll}
@ -975,6 +899,95 @@ $
\caption{Constraint reduce rules}\label{fig:reduce-rules}
\end{figure}
\begin{figure}
\begin{center}
\leavevmode
\fbox{
\begin{tabular}[t]{l@{~}l}
\rulename{Prepare} %The lessdotCC constraint only ensures that the left side looses its wildcardEnvironment.
%It does not ensure that the left side doesn't contain free variables. If you want to ensure that you have to give the left side a normal placeholder
&
$
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \wctype{\Delta'}{C}{\ol{T}} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdotCC \wctype{\Delta'}{C}{\ol{T}} } \\
\end{array}
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin{array}[c]{l}
\text{fv}(\wctype{\Delta'}{C}{\ol{T}}) \subseteq \Delta_{in}
\end{array}
\end{array}
$
\\\\
\rulename{Trim}
&
$
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\Delta,\Delta'}{C}{\ol{S}} \lessdot \type{T} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} } \\
\end{array}
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin{array}[c]{l}
\text{fv}(\ol{S}) \cap \Delta' = \emptyset
\end{array}
\end{array}
$
\\\\
\rulename{Clear}
&
$
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}} \vdash
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} } \\
\hline
\vspace*{-0.4cm}\\
\subst{\type{U}}{\rwildcard{A}}\wildcardEnv \vdash
[\type{U}/\rwildcard{A}]C \cup \, [\type{U}/\rwildcard{A}]\set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T}, \type{U} \doteq \type{L} } \\
\end{array}
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin{array}[c]{l}
\Delta \neq \emptyset\\
\rwildcard{A} \in \text{fv}(\type{T})
\end{array}
\end{array}
$
\\\\
\rulename{Exclude}
&
$
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} } \\
\hline
\vspace*{-0.4cm}\\
\subst{\tv{a}}{\wtv{a}}\wildcardEnv \vdash
[\tv{a}/\wtv{a}]C \cup \, [\tv{a}/\wtv{a}]\set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} } \\
\end{array}
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin{array}[c]{l}
\Delta \neq \emptyset\\
\wtv{a} \in \text{fv}(\type{T}), \tv{a} \ \text{fresh}
\end{array}
\end{array}
$
\end{tabular}}
\end{center}
\caption{Dealing with wildcard types on the left side of a subtype constraint}
\end{figure}
\begin{figure}
If we find an illicit constraint assigning a type containing free variables to a type placeholder not flagged as a wildcard placeholder the algorithm fails.
@ -1356,22 +1369,59 @@ $
%The type reduction is done by the rules in figure \ref{fig:reductionRules}
\begin{description}
\item[Prepare]
The \rulename{Prepare} transformation is always applied together with the \rulename{Reduce} transformation.
\unify{} cannot reduce constraints without checking a few prerequisites.
Take the constraint $\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdot \exptype{C}{\wtv{a}}$ for example.
If we apply a reduction here we get $\rwildcard{X} \doteq \wtv{a}$.
The resulting $\sigma(\wtv{a}) = \rwildcard{X}$ seems like a correct substitution,
but by S-Exists $\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \nless: \exptype{C}{\rwildcard{X}}$.
Reason: Free variables on the right side of a subtype relations are not allowed to show up as bound variables on the left side.
$\rwildcard{X}$ in this case.
Therefore the \rulename{Reduce} rule only reduces constraints where the left side does not declare any wildcards.
But if the right side neither contains wildcard type placeholders nor free variables the constraint can be reduced anyways.
The \rulename{Prepare} rule then converts this constraint to a capture constraint.
Afterwards the \rulename{Capture} rule removes the wildcard declarations on the left side an the constraint can be reduced.
%Take the constraint $\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdot \exptype{C}{\wtv{a}}$ for example.
%If we apply a reduction here we get $\rwildcard{X} \doteq \wtv{a}$.
%The resulting $\sigma(\wtv{a}) = \rwildcard{X}$ seems like a correct substitution,
%but by S-Exists $\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \nless: \exptype{C}{\rwildcard{X}}$.
%Reason: Free variables on the right side of a subtype relations are not allowed to show up as bound variables on the left side.
%$\rwildcard{X}$ in this case.
%Therefore the \rulename{Reduce} rule only reduces constraints where the left side does not declare any wildcards.
%But if the right side neither contains wildcard type placeholders nor free variables the constraint can be reduced anyways.
%The \rulename{Prepare} rule then converts this constraint to a capture constraint.
%Afterwards the \rulename{Capture} rule removes the wildcard declarations on the left side an the constraint can be reduced.
%We loose information during the unification process.
When reducing the constraint
$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\wtv{x}}}$
it turns into $\exptype{List}{\rwildcard{X}} \doteq \exptype{List}{\wtv{x}}$
and now it seems that $\wtv{x} \doteq \rwildcard{X}$ is a correct solution.
This is indeed wrong because $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}} \nless: \exptype{List}{\exptype{List}{\rwildcard{X}}}$.
A correct solution is to remove the wildcard $\rwildcard{X}$ if possible.
% X.List<X> <. List<x> // incorrect
% X.List<List<X>> <. List<List<x>> // incorrect
Therefore the \rulename{Prepare} rule checks if there are any free variables or wildcard placeholders on the right side of the constraint.
If that is the case one of the rules \rulename{Trim}, \rulename{Clear}, or \rulename{Exclude} have to be applied.
In our example this would be the \rulename{Exclude} rule replacing the wildcard placeholder with $\wtv{x}$ with a normal placeholder.
Afterwards \rulename{Prepare} can be used eventually leading to the erasure of the wildcard $\rwildcard{X}$ by equalizing its upper and lower bounds:
\begin{displaymath}
\prftree[r]{\rulename{Contract}}{
\prftree[r]{\rulename{Reduce}}{
\prftree[r]{\rulename{Equals}}{
\prftree[r]{\rulename{Prepare}}{
\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\ntv{x}}}
}
{
\wildcard{X}{\tv{u}}{\tv{l}} \vdash \exptype{List}{\rwildcard{X}} \doteq \exptype{List}{\ntv{x}}
}}
{
\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\ntv{x}}, \exptype{List}{\ntv{x}} \lessdot \exptype{List}{\rwildcard{X}}
}
}
{
\wildcard{X}{\tv{u}}{\tv{l}} \vdash \ntv{x} \doteq \rwildcard{X}
}}{
\text{equalize upper and lower bound of }\rwildcard{X}: \quad
\ntv{x} \doteq \tv{u}, \tv{u} \doteq \tv{l}
}
\end{displaymath}
\end{description}
\subsection{Examples}
\textit{Example} of the type reduction rules in figure \ref{fig:reductionRules} with the input
$\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$
The first step is the \rulename{Capture} rule.