2023-12-27 13:29:33 +00:00
\section { Unify} \label { sec:unify}
2024-02-06 17:04:31 +00:00
\subsection { Description}
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 } } $ .
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.
2024-02-07 09:28:28 +00:00
A constraint set is convertable to a correct type solution if it only contains constraints of the form
2024-02-06 17:04:31 +00:00
$ \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 \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.
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.
2024-02-07 09:28:28 +00:00
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:}
2024-02-06 17:04:31 +00:00
$ \exptype { List } { \tv { a } } \lessdot \wctype { \wildcard { X } { \type { Object } } { \bot } } { List } { \rwildcard { X } } $
The \rulename { Reduce} rule converts this 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.
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
% 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
\subsection { Algorithm}
2023-12-27 13:29:33 +00:00
\newcommand { \gtype } [1]{ \type { #1} }
%\newcommand{\tw}[1]{\tv{#1}_?}
The \unify { } algorithm computes the type solution.
\begin { description}
2024-01-23 15:30:24 +00:00
\item [Input:] An environment $ \Delta ' $
2024-02-05 18:18:16 +00:00
and a set of constraints $ C = \set { \type { T } \lessdot \type { T } , \type { T } \doteq \type { T } \ldots } $
and a list of constraints $ C' = \set { \type { T } \lessdotCC \type { T } } $ .
2023-12-27 13:29:33 +00:00
The input constraints must be of the following format:
\begin { tabular} { lcll}
$ c $ & $ :: = $ & $ \type { T } \lessdot \type { U } $ & Constraint \\
$ \type { T } , \type { U } , \type { L } $ & $ :: = $ & $ \tv { a } \mid \wtv { a } \mid \ntype { N } $ & Type variable or Wildcard Variable or Type \\
$ \ntype { N } , \ntype { S } $ & $ :: = $ & $ \wctype { \overline { \wildcard { X } { U } { L } } } { C } { \ol { T } } $ & Class Type \\
\end { tabular} \\ [0.5em]
\noindent
Additional requirements:
\begin { itemize}
2024-01-23 15:30:24 +00:00
\item Every wildcard $ \rwildcard { X } \in \Delta ' $ has to have an unique name which is not defined anywhere in the constraint set $ C $ .
2023-12-27 13:29:33 +00:00
\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.
2024-02-02 18:23:00 +00:00
\item All types have to be well-formed: $ \wcNtype { \Delta } { N } \in C \implies \Delta _ { in } \vdash \wcNtype { \Delta } { N } \ \ok $
2023-12-27 13:29:33 +00:00
\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
%Example:
Although alpha renaming of wildcards inside a type is allowed by the type system the \unify { } algorithm never does it.
Renaming wildcards leads to additional problems in the substitution rules and in the result containing substitutions with renamed wildcards.
For the \rulename { Equals} to work properly it is adviced to name all wildcards in a specific scheme.
For example by numbering them according to their appereance inside the type parameters
(e.g. $ \wctype { \rwildcard { 1 } , \rwildcard { 2 } } { Pair } { \rwildcard { 1 } , \rwildcard { 2 } } $ ).
\end { itemize}
\item [Output:]
Set of unifiers $ Uni = \set { \sigma _ 1 , \ldots , \sigma _ n } $ and an environment $ \Delta $
\end { description}
The \unify { } algorithm internally uses the following data types:
\begin { tabular} { lcll}
$ C $ & $ :: = $ & $ \overline { c } $ & Constraint set \\
2024-01-09 15:28:19 +00:00
$ c $ & $ :: = $ & $ \type { T } \lessdot \type { T } \mid \type { T } \lessdotCC \type { T } \mid \type { T } \doteq \type { T } $ & Constraint \\
2023-12-27 13:29:33 +00:00
$ \type { T } , \type { U } , \type { L } $ & $ :: = $ & $ \tv { a } \mid \wtv { a } \mid \gtype { G } $ & Type variable or Type \\
$ \gtype { G } $ & $ :: = $ & $ \type { X } \mid \ntype { N } $ & Wildcard, or Class Type \\
$ \ntype { N } , \ntype { S } $ & $ :: = $ & $ \wctype { \triangle } { C } { \ol { T } } $ & Class Type \\
$ \triangle $ & $ :: = $ & $ \overline { \wtype { W } } $ & Wildcard Environment \\
$ \wtype { W } $ & $ :: = $ & $ \wildcard { X } { U } { L } $ & Wildcard \\
\end { tabular}
The $ \wtv { a } $ type variables are flagged as wildcard type variables.
These type variables can be substituted by a wildcard or a type with free wildcard variables.
As long as a type variable is flagged with as $ \wtv { a } $ it will only be used by the subst-wc rule in step 1.
In step 2 all of the wildcard flags are dismissed.
The output therefore never contains these flags.
\unify { } applies a capture conversion everywhere it is possible (see \rulename { Capture} rule).
Capture conversion removes a types bounding environment $ \Delta $ .
Type variables used in its type parameters are now bound to a global scope and not locally anymore.
With \texttt { C} being class names and \texttt { A} being wildcard names.
2024-01-21 13:31:48 +00:00
The wildcard type $ \wildcard { X } { U } { L } $ consist of an upper bound $ \type { U } $ , a lower bound $ \type { L } $
2023-12-27 13:29:33 +00:00
and a name $ \mathtt { X } $ .
The \rulename { Normalize} rule eliminates wildcards. % TODO
This is done by setting the upper and lower bound to the same value.
2024-01-10 15:03:23 +00:00
\unify { } generates wildcards with the \rulename { \generalizeRule } rule.
2023-12-27 13:29:33 +00:00
It is important to generate new wildcards in a standardized fashion.
When having two constraints $ \type { T } \lessdot \tv { a } $ and $ \type { T } \lessdot \tv { b } $ ,
then after applying the \rulename { \generalizeRule } rule the freshly generated constraints are
$ \tv { a } \doteq \type { T' } , \tv { b } \doteq \type { T' } $ .
Both type variables get assigned the same type.
This is necessary for the \rulename { Equals} rule to work properly.
\begin { figure}
\begin { center}
\leavevmode
\fbox {
\begin { tabular} [t]{ l@{ ~} l}
\rulename { Subst} &
$ \begin { array } [ c ] { l }
\wildcardEnv \vdash C \cup \set { \tv { a} \doteq \type { T} } \\
\hline
[\type { T} /\tv { a} ]\wildcardEnv \vdash [\type { T} /\tv { a} ]
C \cup \set { \tv { a} \doteq \type { T} }
\end { array}
\quad \begin { array} { c}
\tv { a} \notin \type { T} \\
2024-01-23 15:30:24 +00:00
\text { fv} (\type { T} ) \subseteq \Delta '
2023-12-27 13:29:33 +00:00
\end { array} $ \\
\\
\rulename { Subst-WC} & $
\begin { array} [c]{ l}
2024-02-06 17:04:31 +00:00
\wildcardEnv \vdash C \cup \set { \wtv { a} \doteq \rwildcard { T} } \\
2023-12-27 13:29:33 +00:00
\hline
2024-02-06 17:04:31 +00:00
[\type { T} /\wtv { a} ]\wildcardEnv \vdash [\type { T} /\wtv { a} ]C
\end { array} \quad \wtv { a} \notin \type { T}
2023-12-27 13:29:33 +00:00
$
\end { tabular} }
\end { center}
\caption { Substitution rules} \label { fig:subst-rules}
\end { figure}
\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}
2024-02-05 00:33:39 +00:00
\wildcardEnv \cup \set { \wildcard { A} { U} { L} } \vdash C \cup \, \set { \type { A} \lessdot \type { G} } \\
2023-12-27 13:29:33 +00:00
\hline
\vspace * { -0.4cm} \\
2024-02-05 00:33:39 +00:00
\wildcardEnv \cup \set { \wildcard { A} { U} { L} } \vdash C \cup \, \set { \type { U} \lessdot \type { G} }
2023-12-27 13:29:33 +00:00
\end { array}
2024-01-30 15:19:01 +00:00
\quad \quad
\begin { array} [c]{ l}
2024-02-05 00:33:39 +00:00
\wildcardEnv \cup \set { \wildcard { A} { U} { L} } \vdash C \cup \, \set { \type { A} \lessdotCC \type { G} } \\
2024-01-30 15:19:01 +00:00
\hline
\vspace * { -0.4cm} \\
2024-02-05 00:33:39 +00:00
\wildcardEnv \cup \set { \wildcard { A} { U} { L} } \vdash C \cup \, \set { \type { U} \lessdotCC \type { G} }
2024-01-30 15:19:01 +00:00
\end { array}
2023-12-27 13:29:33 +00:00
$
\\ \\
\rulename { Lower}
& $
\begin { array} [c]{ l}
2024-02-05 00:33:39 +00:00
\wildcardEnv \cup \set { \wildcard { A} { U} { L} } \vdash C \cup \set { \type { G} \lessdot \type { A} } \\
2023-12-27 13:29:33 +00:00
\hline
\vspace * { -0.4cm} \\
2024-02-05 00:33:39 +00:00
\wildcardEnv \cup \set { \wildcard { A} { U} { L} } \vdash C \cup \set { \type { G} \lessdot \type { L} }
2023-12-27 13:29:33 +00:00
\end { array}
$
\\ \\
\rulename { Bot}
& $
\begin { array} [c]{ l}
\wildcardEnv \vdash C \cup \set { \bot \lessdot \type { T} } \\
\hline
\vspace * { -0.4cm} \\
\wildcardEnv \vdash C
\end { array}
$
\\ \\
\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
\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 { L'} , \type { U} \doteq \type { U'} }
2024-02-09 20:49:41 +00:00
\end { array}
% \quad \text{fv}(\type{U}, \type{U'}, \type{L}, \type{L'}) \subseteq \Delta_in
2023-12-27 13:29:33 +00:00
$
\\ \\
\rulename { Tame}
& $
\begin { array} [c]{ l}
\wildcardEnv \cup \set { \wildcard { A} { \type { U} } { \type { L} } } \vdash C \cup \, \set { \rwildcard { A} \doteq \type { T} } \\
\hline
\vspace * { -0.4cm} \\
\wildcardEnv \cup \set { \wildcard { A} { \type { U} } { \type { L} } } \vdash C \cup \, \set { \type { L} \doteq \type { T} , \type { U} \doteq \type { T} }
2024-02-09 20:49:41 +00:00
\end { array} %\quad \text{fv}(\type{U}, \type{L}) \subseteq \Delta_in
2023-12-27 13:29:33 +00:00
$
\\ \\
2024-02-08 13:53:40 +00:00
% \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}
$
\\ \\
2023-12-27 13:29:33 +00:00
\rulename { Erase}
& $
\begin { array} [c]{ l}
\wildcardEnv \vdash C \cup \, \set { \type { T} \doteq \type { T} } \\
\hline
\vspace * { -0.4cm} \\
\wildcardEnv \vdash C
\end { array}
$
\\ \\
\rulename { Erase}
& $
\begin { array} [c]{ l}
\wildcardEnv \vdash C \cup \, \set { \type { T} \lessdot \type { T} } \\
\hline
\vspace * { -0.4cm} \\
\wildcardEnv \vdash C
\end { array}
$
\\ \\
\rulename { Swap} & $
\begin { array} [c]{ l}
\wildcardEnv \vdash C \cup \set { \type { G} \doteq \tv { a} } \\
\hline
\wildcardEnv \vdash C \cup \set { \tv { a} \doteq \type { G} }
\end { array}
\quad
\begin { array} [c]{ l}
2024-02-06 17:04:31 +00:00
\wildcardEnv \vdash C \cup \set { \type { T} \doteq \wtv { a} } \\
2023-12-27 13:29:33 +00:00
\hline
2024-02-06 17:04:31 +00:00
\wildcardEnv \vdash C \cup \set { \wtv { a} \doteq \type { T} }
2023-12-27 13:29:33 +00:00
\end { array} \quad
\begin { array} [c]{ l}
\wildcardEnv \vdash C \cup \set { \type { N} \doteq \rwildcard { A} } \\
\hline
\wildcardEnv \vdash C \cup \set { \rwildcard { A} \doteq \type { N} }
\end { array} $
\end { tabular} }
\end { center}
\caption { Constraint normalize rules} \label { fig:normalizing-rules}
\end { figure}
The \rulename { match} rule generates fresh wildcards $ \overline { \wildcard { A } { \tv { u } } { \tv { l } } } $ .
Their upper and lower bounds are fresh type variables.
%Unify only renames the wildcards in the reduce rule
% It's the only place where wildcards are coming into play (theres always a reduce step before a wildcard substitution is possible)
% die wildcard variablen sollten erst am Ende ausgetauscht werden gegen normale variablen
% das funktioniert, da die im Reduce step erstellten direkt substituiert werden
% die anderen erlauben Capture Conversion aber nur wenn der Methodentyp und Parametertyp schon feststeht! (gleich Mächtig wie TI in Java)
% a? <. T ->
% T <. a? ->
% a? =. T -> substitute!
% bei normalen Typvariablen werden keine Wildcards substituiert
% \begin{tcolorbox}
% $
% \wctype{\rwildcard{X}}{Box}{\rwildcard{X}} \lessdot \exptype{Box}{\tv{a}_?}, \\
% \exptype{Box}{\tv{a}_?} \lessdot \wctype{\rwildcard{X}}{Box}{\rwildcard{X}}
% $
% \end{tcolorbox}
\begin { figure}
\begin { center}
\leavevmode
\fbox {
\begin { tabular} [t]{ l@{ ~} l}
\rulename { Match}
& $
\begin { array} [c]{ @{ } ll}
\begin { array} [c]{ l}
\wildcardEnv \vdash C \cup \, \set {
\tv { a} \lessdot \wctype { \Delta } { D} { \ol { T} } , \tv { a} \lessdot \wctype { \Delta '} { D'} { \ol { T'} } } \\
\hline
\vspace * { -0.4cm} \\
\wildcardEnv \vdash C \cup \, \left \{ \begin { array} [c]{ l}
\tv { a} \lessdot \wctype { \overline { \wildcard { A} { \tv { u} } { \tv { l} } } } { C} { \overline { \rwildcard { A} } } ,
\ol { \tv { l} } \lessdot \ol { \tv { u} } , \\
\wctype { \overline { \wildcard { A} { \tv { u} } { \tv { l} } } } { C} { \overline { \rwildcard { A} } }
\lessdot \wctype { \Delta } { D} { \ol { T} } , \\
\wctype { \overline { \wildcard { A} { \tv { u} } { \tv { l} } } } { C} { \overline { \rwildcard { A} } }
\lessdot \wctype { \Delta '} { D'} { \ol { T'} }
\end { array}
\right \}
\end { array}
& \begin { array} [c]{ l}
\text { fresh} \ \overline { \wildcard { A} { \tv { u} } { \tv { l} } } \\
\type { C} \ll \type { D} \\
\type { C} \ll \type { D'} % TODO: THe match rule has to pick the most general type for C
\end { array}
\end { array}
$
\\ \\
\ruleReduceWC { }
&
$
\begin { array} [c]{ @{ } ll}
\begin { array} [c]{ l}
\wildcardEnv \vdash
C \cup \, \set { \exptype { C} { \ol { S} } \lessdot
\wctype { \overline { \wildcard { A} { \type { U} } { \type { L} } } } { C} { \ol { T} } } \\
\hline
\vspace * { -0.4cm} \\
\wildcardEnv
\vdash C \cup \, \set {
\ol { \type { S} } \doteq [\ol { \wtv { a} } /\overline { \rwildcard { A} } ]\ol { \type { T} } ,
\ol { \wtv { a} } \lessdot [\ol { \wtv { a} } /\overline { \rwildcard { A} } ]\ol { U} , [\ol { \wtv { a} } /\overline { \rwildcard { A} } ]\ol { L} \lessdot \ol { \wtv { a} } }
\end { array}
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin { array} [c]{ l}
\ol { \wtv { a} } \ \text { fresh} \\
%\text{fv}(\exptype{C}{\ol{S}}) \subseteq \text{dom}(\overline{\wildcard{B}{\type{U'}}{\type{L'}}})
%\text{dom}(\overline{\wildcard{A}{\type{U}}{\type{L}}}) \subseteq \text{fv}(\exptype{C}{\ol{T}}) \\
%\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
\end { array}
\end { array}
$
\\ \\
\rulename { Capture}
&
$
\begin { array} [c]{ @{ } ll}
\begin { array} [c]{ l}
\wildcardEnv \vdash
2024-01-30 15:19:01 +00:00
C \cup \, \set { \wctype { \overline { \wildcard { B} { \type { U} } { \type { L} } } } { C} { \ol { S} } \lessdotCC \type { T} } \\
2023-12-27 13:29:33 +00:00
\hline
\vspace * { -0.4cm} \\
2024-01-10 15:03:23 +00:00
\wildcardEnv \cup \overline { \wildcard { C} { \type { U} } { \type { L} } }
2023-12-27 13:29:33 +00:00
\vdash C \cup \, \set {
2024-01-30 15:19:01 +00:00
[\ol { \rwildcard { C} } /\ol { \rwildcard { B} } ] \exptype { C} { \ol { S} } \lessdot \type { T} }
2023-12-27 13:29:33 +00:00
\end { array}
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin { array} [c]{ l}
\ol { \rwildcard { C} } \ \text { fresh} \\
%\text{fv}(\type{T}) \neq \emptyset
\end { array}
\end { array}
$
2024-01-10 15:03:23 +00:00
\\ \\
\rulename { Prepare}
&
$
\begin { array} [c]{ @{ } ll}
\begin { array} [c]{ l}
\wildcardEnv \vdash
2024-01-17 04:52:01 +00:00
C \cup \, \set { \wctype { \Delta } { C} { \ol { S} } \lessdot \wctype { \Delta '} { C} { \ol { T} } } \\
2024-01-10 15:03:23 +00:00
\hline
\vspace * { -0.4cm} \\
2024-01-16 17:03:54 +00:00
\wildcardEnv \vdash
2024-01-17 04:52:01 +00:00
C \cup \, \set { \wctype { \Delta } { C} { \ol { S} } \lessdotCC \wctype { \Delta '} { C} { \ol { T} } } \\
2024-01-10 15:03:23 +00:00
\end { array}
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin { array} [c]{ l}
2024-02-06 17:04:31 +00:00
\text { fv} (\wctype { \Delta } { C} { \ol { S} } , \wctype { \Delta '} { C} { \ol { T} } ) \subseteq \Delta _ { in}
2024-01-10 15:03:23 +00:00
\end { array}
\end { array}
$
2023-12-27 13:29:33 +00:00
\\ \\
2024-02-08 09:49:03 +00:00
\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}
$
\\ \\
2024-02-02 18:23:00 +00:00
% \rulename{Adopt}
% & $
% \begin{array}[c]{@{}ll}
% \begin{array}[c]{l}
% \wildcardEnv \vdash C \cup \, \set{
% \tv{b} \lessdot \tv{a},
% \tv{a} \lessdot \type{N}, \tv{b} \lessdot \type{N'}} \\
% \hline
% \vspace*{-0.4cm}\\
% \wildcardEnv \vdash C \cup \, \set{
% \tv{b} \lessdot \type{N},
% \tv{b} \lessdot \tv{a},
% \tv{a} \lessdot \type{N} , \tv{b} \lessdot \type{N'}
% }
% \end{array}
% \end{array}
% $
% \\\\
2023-12-27 13:29:33 +00:00
\rulename { Adapt}
&
$
\begin { array} [c]{ @{ } ll}
\begin { array} [c]{ l}
\wildcardEnv \vdash C \cup \, \set { \wctype { \Delta } { C} { \ol { T} } \lessdot
\wctype { \Delta '} { D'} { \ol { T'} } } \\
\hline
\vspace * { -0.4cm} \\
\wildcardEnv \vdash C \cup \, \set { \wctype { \Delta } { D} { [\ol { \type { T} } /\ol { X} ]\ol { S} } \lessdot \wctype { \Delta '} { D'} { \ol { T'} } }
\end { array}
& \begin { array} [c]{ l}
\type { C} \ll \type { D'} \\
\texttt { class} \ \exptype { C} { \ol { X} \triangleleft \ol { N} } \triangleleft \exptype { D} { \ol { S} }
\end { array}
\end { array}
$
\end { tabular} }
\end { center}
\caption { Constraint reduce rules} \label { fig:reduce-rules}
\end { figure}
The new constraint generated by the adopt rule may be eliminated by the match rule.
The adopt rule still needs to be applied only once per constraint.
Wildcards consist out of three parts.
A name, a scope and a upper and lower bound.
% The \unify{} algorithm from \cite{plue09_1} substitutes type variables with wildcards.
% A constraint $\wctype{\wildcard{X}{\type{Object}}{\bot}}{C}{\rwildcard{X}} \lessdot \exptype{C}{\tv{a}}$
% has no solution.
% Replacing the type variable $\tv{a}$ with the wildcard $\rwildcard{X}$ is not correct!
% The wildcard $\rwildcard{X}$ cannot leave its scope and the type $\exptype{C}{\rwildcard{X}}$
% is considered invalid.
Wildcards are not reflexive. A box of type $ \wctype { \rwildcard { X } } { Box } { \rwildcard { X } } $
is able to hold a value of any type. It could be a $ \exptype { Box } { String } $ or a $ \exptype { Box } { Integer } $ etc.
Also two of those boxes do not necessarily contain the same type.
But there are situations where it is possible to assume that.
For example the type $ \wctype { \rwildcard { X } } { Pair } { \exptype { Box } { \rwildcard { X } } , \exptype { Box } { \rwildcard { X } } } $
is a pair of two boxes, which always contain the same type.
Inside the scope of the \texttt { Pair} type, the wildcard $ \rwildcard { X } $ stays the same.
The algorithm starts with an empty wildcard environment $ \wildcardEnv { } $ .
Only the reduce 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.
When a new type is generated by the \unify { } algorithm it always has the form
$ \wctype { \ol { \rwildcard { A } } } { C } { \ol { \rwildcard { A } } } $ .
\textbf { Step 1:}
Apply the rules depicted in the figures \ref { fig:normalizing-rules} , \ref { fig:reduce-rules} and \ref { fig:wildcard-rules} exhaustively.
Starting with the \rulename { circle} rule. Afterwards the other rules in figure \ref { fig:normalizing-rules} .
2024-02-06 17:04:31 +00:00
\begin { figure}
2023-12-31 02:32:26 +00:00
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.
2024-02-06 17:04:31 +00:00
$ \set { \tv { a } \doteq \type { N } } \in C $ with $ \text { fv } ( \type { N } ) \cap \Delta _ { in } \neq \emptyset $ $ \implies $ fail!
% if T <. S with not T << S
% T <. S with fv(T) cup fv(S) not empty (free variables in a non capture conversion constraint)
\caption { Fail conditions}
\end { figure}
2023-12-31 02:32:26 +00:00
2023-12-27 13:29:33 +00:00
The first step of the algorithm is able to remove wildcards.
Removing a wildcard works by setting its lower and upper bound to be equal.
(Def: $ \type { Object } = \wildcard { A } { Object } { Object } $ ).
The \rulename { Equals} rule is responsible for this.
\textbf { Example:}
\begin { displaymath}
\begin { array} [c]{ @{ } ll}
\begin { array} [c]{ l}
\wildcardEnv \cup \set { \wildcard { X} { \tv { u} } { \tv { l} } } \vdash
C \cup \, \set { \type { Object} \doteq \type { X} , \tv { l} \lessdot \tv { u} } \\
\hline
\vspace * { -0.4cm} \\
\wildcardEnv \cup \set { \wildcard { X} { \tv { u} } { \tv { l} } } \vdash C \cup \,
\set { \type { Object} \lessdot \type { X} , \type { X} \lessdot \type { Object} , \tv { l} \lessdot \tv { u}
} \\
\hline
\vspace * { -0.4cm} \\
\wildcardEnv \cup \set { \wildcard { X} { \tv { u} } { \tv { l} } } \vdash C \cup \,
\set { \type { Object} \lessdot \tv { l} , \tv { u} \lessdot \type { Object} , \tv { l} \lessdot \tv { u}
} \\
\hline
\vspace * { -0.4cm} \\
\ldots \\
\hline
\vspace * { -0.4cm} \\
\wildcardEnv \cup \set { \wildcard { X} { \type { Object} } { \type { Object} } } \vdash C \\
\end { array}
\end { array}
\end { displaymath}
2023-12-27 18:03:25 +00:00
\textbf { Helper functions:}
2023-12-27 13:29:33 +00:00
\begin { description}
2023-12-27 18:03:25 +00:00
\item [$\tph{}$] returns all type placeholders inside a given type.
\textit { Example:} $ \tph ( \wctype { \wildcard { X } { \tv { a } } { \bot } } { Pair } { \wtv { b } , \rwildcard { X } } ) = \set { \tv { a } , \wtv { b } } $
2023-12-27 13:29:33 +00:00
\item [$ \ll $ relation:]
The $ \ll $ relation is the reflexive and transitive closure of the \texttt { extends} relations:
\begin { displaymath}
\begin { array} [c]{ c}
\exptype { C} { \ol { X} \triangleleft \ol { N} } \triangleleft \exptype { D} { \ol { N} } \\
\hline
\vspace * { -0.4cm} \\
\texttt { C} \ll \texttt { D}
\end { array}
\quad
\begin { array} [c]{ l}
\\
\hline
\vspace * { -0.4cm} \\
\texttt { C} \ll \texttt { C}
\end { array}
\quad
\begin { array} [c]{ l}
\texttt { C} \ll \texttt { D} , \texttt { D} \ll \texttt { E} \\
\hline
\vspace * { -0.4cm} \\
\texttt { C} \ll \texttt { E}
\end { array}
\end { displaymath}
The algorithm uses it to determine if two types are possible subtypes of one another.
This is needed in the \rulename { adapt} and \rulename { match} rules.
%\textbf{Wildcard renaming}\\
\item [Wildcard renaming:]
The \rulename { reduce} rule separates wildcards from their environment.
At this point each wildcard gets a new and unique name.
To only rename the respective wildcards the reduce rule renames wildcards up to alpha conversion:
($ [ \ol { C } / \ol { B } ] $ in the \rulename { reduce} rule)
\begin { align*}
[\type { A} /\type { B} ]\type { B} & = \type { A} \\
[\type { A} /\type { B} ]\type { C} & = \type { C} & \text { if} \ \type { B} \neq \type { C} \\
[\type { A} /\type { B} ]\wcNtype { \Delta } { N} & = \wcNtype { \Delta } { [\type { A} /\type { B} ]N} & \text { if} \ \type { B} \notin \Delta \\
[\type { A} /\type { B} ]\wcNtype { \Delta } { N} & = \wcNtype { \Delta } { N} & \text { if} \ \type { B} \in \Delta \\
\end { align*}
\item [Free Variables:]
The $ \text { fv } $ function assumes every wildcard type variable to be a free variable aswell.
%\textbf{Fresh Wildcards}\\
\item [Fresh Wildcards:]
$ \text { fresh } \ \overline { \wildcard { A } { \tv { u } } { \tv { l } } } $ generates fresh wildcards.
The new names $ \ol { A } $ are fresh, aswell as the type variables $ \ol { \tv { u } } $ and $ \ol { \tv { l } } $ ,
which are used for the upper and lower bounds.
\end { description}
% \noindent
% \textbf{Example: (reduce-rule)}
% %The \ruleReduceWC{} resembles the \texttt{S-Exists} subtyping rule.
% %It converts wildcard types to fresh type variables.
% %For example take the input constraint $\exptype{Pair}{\ntype{Object},\tv{b}} \lessdot \wctype{\wildcard{A}{\tv{c}}{\tv{d}}}{Pair}{\wildcard{A}{\tv{c}}{\tv{d}},\wildcard{A}{\tv{c}}{\tv{d}}}$.
% %First we apply the \ruleReduceWC{} rule, which replaces $\wildcard{A}{\tv{c}}{\tv{d}}$ with a fresh type variable $\tv{a}$:
% We assume the input constraints $C = \exptype{Pair}{\ntype{Object},\tv{b}} \lessdot \wctype{\wildcard{A}{\tv{c}}{\tv{d}}}{Pair}{\wildcard{A}{\tv{c}}{\tv{d}},\wildcard{A}{\tv{c}}{\tv{d}}}$.
% The type on the right side $\wctype{\wildcard{A}{\tv{c}}{\tv{d}}}{Pair}{\wildcard{A}{\tv{c}}{\tv{d}},\wildcard{A}{\tv{c}}{\tv{d}}}$
% \begin{align*}
% \ddfrac{
% \exptype{Pair}{\ntype{Object},\tv{b}} \lessdot \wctype{\wildcard{A}{\tv{c}}{\tv{d}}}{Pair}{\wildcard{A}{\tv{c}}{\tv{d}},\wildcard{A}{\tv{c}}{\tv{d}}}
% }{
% \ntype{Object} \doteq \tv{a}, \tv{b} \doteq \tv{a}, \tv{a} \lessdot \tv{c}, \tv{d} \lessdot \tv{a}
% } \ruleReduceWC{}
% \end{align*}
% By substition we get the result: % $\tv{a} \doteq \type{Object}$, $\tv{a} \doteq \type{Object}$, $\ldots$.
% \begin{align*}
% \ddfrac{
% \ntype{Object} \doteq \tv{a}, \tv{b} \doteq \tv{a}, \tv{a} \lessdot \tv{c}, \tv{d} \lessdot \tv{a}
% }{
% \tv{a} \doteq \ntype{Object} , \tv{b} \doteq \ntype{Object}, \ntype{Object} \lessdot \tv{c}, \tv{d} \lessdot \ntype{Object}
% } \rulename{Subst}
% \end{align*}
% \\[1em]
\noindent
\textbf { Step 2:}
%If there are no $(\type{T} \lessdot \tv{a})$ constraints remaining in the constraint set $C$
%resume with step 4.
The rules in figure \ref { fig:step2-rules} offer multiple possibilities to deal with constraints of the form $ \type { N } \lessdot \tv { a } $ .
This builds a search tree over multiple possible solutions.
\unify { } has to try each branch and accumulate the resulting solutions into a solution set.
\begin { figure}
\begin { center}
\fbox {
\begin { tabular} [t]{ l@{ ~} l}
2024-02-05 00:33:39 +00:00
\rulename { Same}
& $
\begin { array} [c]{ l}
\wildcardEnv \vdash
C \cup \type { G} \lessdot \tv { a} \\
\hline
\wildcardEnv \vdash
C \cup \set {
\tv { a} \doteq \type { G}
}
\end { array} \quad \begin { array} [c]{ l}
\text { fv} (\type { G} ) \in \Delta _ { in}
\end { array}
$
\\ \\
2023-12-27 13:29:33 +00:00
\rulename { \generalizeRule }
& $
\begin { array} [c]{ l}
\wildcardEnv \vdash C \cup \wctype { \Delta } { C} { \ol { T} } \lessdot \tv { a} \\
\hline
\wildcardEnv \vdash C \cup \set { \wctype { \Delta } { C} { \ol { T} } \lessdot \tv { a} ,
\tv { a} \doteq \wctype { \overline { \wildcard { X} { \tv { u} } { \tv { l} } } } { C} { \overline { \rwildcard { X} } } ,
%\overline{\tv{l} \lessdot \tv{u}}, % not needed, due to subst and reduce rule which are used afterwards
\overline { \tv { 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} { \tv { u} } { \tv { l} } }
\end { array}
$
\\ \\
2024-02-02 18:23:00 +00:00
\rulename { Subst-X}
& $
\begin { array} [c]{ l}
\wildcardEnv \cup \set { \wildcard { X} { \type { U} } { \type { L} } } \vdash
C \cup \rwildcard { X} \lessdot \tv { a} \\
\hline
\wildcardEnv \cup \set { \wildcard { X} { \type { U} } { \type { L} } } \vdash
C \cup \set {
\tv { a} \doteq \rwildcard { X}
}
\end { array} \quad \begin { array} [c]{ l}
\rwildcard { X} \in \Delta _ { in}
\end { array}
$
\\ \\
\rulename { Gen-X}
& $
\begin { array} [c]{ l}
\wildcardEnv \cup \set { \wildcard { X} { \type { U} } { \type { L} } } \vdash
C \cup \rwildcard { X} \lessdot \tv { a} \\
\hline
\wildcardEnv \cup \set { \wildcard { X} { \type { U} } { \type { L} } } \vdash
C \cup \set {
\type { U} \lessdot \tv { a}
}
\end { array}
$
\\ \\
2023-12-27 13:29:33 +00:00
\rulename { Super}
& $
\begin { array} [c]{ l}
\wildcardEnv \vdash C \cup \wctype { \Delta } { C} { \ol { T} } \lessdot \tv { a} \\
\hline
2024-02-02 18:23:00 +00:00
\wildcardEnv \vdash C \cup \set { \wctype { \Delta '} { D} { [\ol { T} /\ol { X} ]\ol { N} } \lessdot \tv { a} }
2023-12-27 13:29:33 +00:00
%\set{\wctype{\ol{\wtype{W}}}{D}{[\ol{X}/\ol{Y}]\ol{Z}} \lessdot \tv{a}}
\end { array} \quad
\begin { array} { l}
\texttt { class} \ \exptype { C} { \ol { X} } \triangleleft \exptype { D} { \ol { N} } \\
2024-02-02 18:23:00 +00:00
\ol { X} \notin \wildcardEnv \cup \Delta ,\, \Delta ' = \Delta \cap \text { fv} ([\ol { T} /\ol { X} ]\ol { N} )
2023-12-27 13:29:33 +00:00
\end { array}
$
\\ \\
2024-02-05 00:33:39 +00:00
% \rulename{Settle}
% & $
% \begin{array}[c]{l}
% \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
% \tv{a} \lessdot^* \tv{b}}
% \\
% \hline
% \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot^* \tv{b}, \tv{b} \lessdot \type{N} }
% \end{array}
% $
% \\\\
% \rulename{Raise}
% & $
% \begin{array}[c]{l}
% \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
% \tv{a} \lessdot \tv{b}}
% \\
% \hline
% \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b} }
% \end{array}
% $
% \\\\
2023-12-27 13:29:33 +00:00
\end { tabular} }
\end { center}
\caption { Step 2 branching: Multiple rules can be applied to the same constraint}
\label { fig:step2-rules}
\end { figure}
%For every $\type{T} \lessdot \tv{a}$ constraint, the unify algorithm has to consider every possible supertype of $\type{T}$.
%For every $\type{N}$ with $\type{T} \leq \type{N}$: ($\texttt{class} \ \exptype{T}{\ol{Y} \triangleleft \ol{N}} \triangleleft \type{N}$)
%There are two different ways of handling a $\type{T} \lessdot \tv{a}$ constraint:
%TODO: why the \generalizeRule is basically the Same rule for regular type placeholders
2023-12-27 18:03:25 +00:00
%where is the mistake in the old unify algorithm?
%when working with equality the problems arise! Free variables should not escape their scope
2023-12-27 13:29:33 +00:00
% Replacing regular type placeholders causes problems related to method calls and capture conversion.
% <X> List<X> same(List<X> a, List<X> b){}
2023-12-27 18:03:25 +00:00
% This program has no correct type. the same method requires
2023-12-27 13:29:33 +00:00
% \begin{lstlisting}
% List<?> f;
% List<?> problem(){
% return same(problem(), problem()) ?: f;
% }
% \end{lstlisting}
% \begin{constraints}
% r <. List<x?>
% r <. List<x?>
% X.List<X> <. r
% \end{constraints}
% %TODO
\unify { } generates wildcard types for constraints of the form $ \type { N } \lessdot \tv { a } $ with the \rulename { \generalizeRule } rule.
Otherwise only the wildcards already defined in the input constraints will be included in the result.
\rulename { \generalizeRule } attempts to give $ \tv { a } $ a more general type by replacing only the type parameters with fresh wildcards.
The second variation sets $ \tv { a } $ to the direct supertype of type \texttt { C} .
For the constraint $ \texttt { Object } \lessdot \tv { a } $ the algorithm can only apply $ \tv { a } \doteq \texttt { Object } $ ,
because \texttt { Object} has no other supertype than itself.
Constraints of the form $ \set { \tv { a } \lessdot \type { N } , \tv { a } \lessdot ^ * \tv { b } } $
need to be handled in a similiar fashion.
The type variable $ \tv { b } $ could either be a sub or a supertype of the type $ \type { N } $ .
We have to consider both possibilities.
\\ [1em]
% The specification of the \unify{} algorithm has only two rules generating $\doteq$-Constraints
% , \rulename{Reduce} and \rulename{Ground}.
% $\doteq$-Constraints and the accompaning substitutions are dangerous respective to the soundness of the algorithm.
% For the soundness proof of the \unify{} algorithm we have to show every generation of equals constraints
% and the subsequent application of the \rulename{subst} rule is correct.
% We try to use them as sparsely as possible to simplify the soundness proof.
% You can notice this at \rulename{Equals} or \rulename{Force}:
% Instead of setting $\type{U} \doteq \type{L}$, we say
% $\type{U} \lessdot \type{L}, \type{L} \lessdot \type{U}$.
\noindent
\textbf { Step 3}
\textbf { (Eliminate Wildcard Variables):}
2024-01-30 15:19:01 +00:00
If no more rules in step 2 are applicable \unify { } has to eliminate all wildcard variables and $ \lessdotCC $ constraints by applying the \rulename { Remove} rule
2023-12-27 13:29:33 +00:00
and start over at step 1.
If $ C $ does not contain any wildcard variables the algorithm proceeds with step 4.
2024-01-09 06:33:02 +00:00
\begin { center}
\fbox {
\begin { tabular} [t]{ l@{ ~} l}
\rulename { Remove}
& $
\begin { array} [c]{ @{ } ll}
\begin { array} [c]{ l}
\wildcardEnv \vdash C \\
% \cup \, \set{ \wtv{a} \lessdot \type{T} }\\
\hline
\vspace * { -0.4cm} \\
\subst { \tv { a} } { \wtv { a} } \wildcardEnv \vdash [\tv { a} /\wtv { a} ]C
\end { array}
& \begin { array} [c]{ l}
\wtv { a} \in C \\
\tv { a} \ \text { fresh}
\end { array}
\end { array}
2024-01-31 17:05:42 +00:00
$
2024-01-30 15:19:01 +00:00
\\ \\
\rulename { Remove-Cons} & $
\begin { array} [c]{ l}
\wildcardEnv \vdash C \cup \set { \type { S} \lessdotCC \type { T} } \\
\hline
\vspace * { -0.4cm} \\
\wildcardEnv \vdash C \cup \set { \type { S} \lessdot \type { T} }
\end { array}
2024-01-09 06:33:02 +00:00
$
\end { tabular} }
\end { center}
2023-12-27 13:29:33 +00:00
2024-02-02 18:23:00 +00:00
\textbf { Step 4:}
If there are constraints of the form $ ( \tv { a } \lessdot \tv { b } ) $ remaining in the constraint set then
apply the \rulename { Sub-Elim} rule and start over with step 1.
Otherwise continue to step 5.
\begin { center}
\fbox {
\begin { tabular} [t]{ l@{ ~} l}
\rulename { SubElim}
& $ \begin { array } [ c ] { l }
\wildcardEnv \vdash C \cup \set { \tv { a} \lessdot \tv { b} } \\
\hline
[\tv { a} /\tv { b} ]\wildcardEnv \vdash [\tv { a} /\tv { b} ]C \cup \set { \tv { b} \doteq \tv { a} }
\end { array}
$
\end { tabular} }
\end { center}
2023-12-27 13:29:33 +00:00
\noindent
2024-02-02 18:23:00 +00:00
\textbf { Step 5:}
We apply the rules in figure \ref { fig:cleanup-rules} exhaustively and proceed with step 6.
2023-12-27 13:29:33 +00:00
\begin { figure}
\begin { center}
\leavevmode
\fbox {
\begin { tabular} [t]{ l@{ ~} l}
\rulename { Ground}
& $ \begin { array } [ c ] { @ { } ll }
\begin { array} [c]{ l}
\wildcardEnv \cup \overline { \set { \wildcard { X} { \type { U} } { \tv { a} } } } \vdash C \cup \, \set {
\overline { \tv { a} \lessdot \type { T} } } \\
\hline
\vspace * { -0.4cm} \\
\wildcardEnv \cup \overline { \set { \wildcard { X} { \type { U} } { \bot } } } \vdash
C \cup \set { \tv { a} \doteq \bot }
\end { array}
& \begin { array} [c]{ l}
%\forall \wctype{\Delta}{C}{\ol{T}} \in C: \tv{a} \notin \ol{T} \\
\tv { a} \notin C, \, \rwildcard { X} \notin C, \, \tv { a} \notin \overline { T} %\\
%\text{length}( \overline{\tv{a} \lessdot \type{T}} ) > 1
\end { array}
\end { array} $
\\ \\
\rulename { Crunch}
& $ \begin { array } [ c ] { @ { } ll }
\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} } } \\
\hline
\vspace * { -0.4cm} \\
\wildcardEnv \vdash
C \cup \set { \tv { a} \doteq \wctype { \Delta '} { C} { [\ol { U} /\ol { X} ]\ol { S} } }
\end { array}
& \begin { array} [c]{ l}
\ol { U} = \ol { L}
\end { array}
\end { array} $
\\ \\
\rulename { Crunch}
& $ \begin { array } [ c ] { @ { } ll }
\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} } } \\
\hline
\vspace * { -0.4cm} \\
\wildcardEnv \vdash
C \cup \set { \tv { a} \lessdot \wctype { \Delta '} { C} { [\ol { U} /\ol { X} ]\ol { S} } }
\end { array}
& \begin { array} [c]{ l}
\ol { U} = \ol { L}
\end { array}
\end { array} $
% \\\\ % The force rule is unnecessary because every type placeholder has an upper bound Object (a <. Object) The match rule eliminates those wildcards
% \rulename{Force} &$
% \begin{array}[c]{@{}ll}
% \begin{array}[c]{l}
% \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}}
% \vdash C \cup \, \set{
% \tv{a} \lessdot \type{N} } \\
% \hline
% \vspace*{-0.4cm}\\
% \wildcardEnv
% \vdash
% C \cup \, \set{ \tv{a} \lessdot [\type{U}/\rwildcard{X}]\type{N},
% \type{U} \doteq \type{L} }
% \end{array}
% &\begin{array}[c]{l}
% \type{X} \in \text{fv}(\type{N}) \\
% %\Delta' = \Delta \cup \set{\wildcard{X}{\type{U}}{\type{L}}}
% \end{array}
% \end{array}$
% \\\\
% \rulename{FlatOut} &$
% \begin{array}[c]{@{}ll}
% \begin{array}[c]{l}
% \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}}
% \vdash C \cup \, \set{
% \tv{a} \lessdot \wcNtype{\Delta}{N} } \\
% \hline
% \vspace*{-0.4cm}\\
% \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}}
% \vdash
% C
% \end{array}
% &\begin{array}[c]{l}
% \type{X} \in \text{fv}(\wcNtype{\Delta}{N}) \\
% \tv{a} \notin C , \, \tv{a} \notin \wildcardEnv, \tv{a} \notin \sigma
% \end{array}
% \end{array}$
\end { tabular} }
\end { center}
\caption { Cleanup rules} \label { fig:cleanup-rules}
\end { figure}
The cleanup step prepares the constraint set for the last step by applying the following concepts:
%Two transformations are done which also help to remove unnecessary types from the solution set.
\begin { description}
\item [Bottom type]
The bottom type $ \bot $ is used to generate \texttt { ? extends} wildcard definitions.
This is the only possible solution when dealing with multiple upper bounds:
$ \tv { a } \lessdot \type { T } , \tv { a } \lessdot \type { S } $ is usually not a correct solution (given $ \type { S } $ and $ \type { T } $ are no subtypes of eachother).
But if $ \tv { a } $ is a lower bound of a wildcard it can be set to $ \bot $ .
Those constraints only stay in the constraint set after the first step if $ \type { S } $ and $ \type { T } $ do not have a common subtype.
The \rulename { Ground} rule uses this concept to generate \texttt { extends} Wildcards.
\item [Eliminating Wildcards]
Wildcards that have the same upper and lower bounds can be removed.
This is done by the \rulename { Crunch} rule.
\textit { Example:} The type $ \wctype { \wildcard { X } { \type { String } } { \type { String } } } { List } { \rwildcard { X } } $
becomes $ \exptype { List } { \type { String } } $ .
%TODO: The a =. T (with T containing free variables) could be removed here.
% Not needed for the soundness of the algorithm, but handy for the implementation (check this when implementing the algorithm)
\end { description}
\noindent
2024-02-02 18:23:00 +00:00
\textbf { Step 6 (Generating Result):}
2023-12-27 13:29:33 +00:00
Apply the rules in figure \ref { fig:generation-rules} until $ \wildcardEnv = \emptyset $ and $ C = \emptyset $ .
The resulting $ \Delta , \sigma $ is a correct solution.
For this step to succeed there should only be four kinds of constraints left.
\begin { enumerate}
%\item\label{item:3} $\tv{a} \lessdot \tv{b}$ %, with $a$ and $b$ both isolated type variables
\item $ \tv { a } \doteq \tv { b } $
%\item $\wtv{a} \doteq \type{G}$
2024-01-31 17:05:42 +00:00
\item \label { item:1} $ \tv { a } \lessdot \wctype { \ol { \wtype { W } } } { C } { \ol { \type { T } } } $ , with $ \text { fv } ( \wctype { \ol { \wtype { W } } } { C } { \ol { \type { T } } } ) \subseteq \Delta _ in $
2023-12-27 13:29:33 +00:00
\item \label { item:2} $ \tv { a } \doteq \wctype { \ol { \wtype { W } } } { C } { \ol { \type { T } } } $ , with $ \tv { a } \notin \ol { \type { T } } $ % and $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) = \emptyset$
\item \label { item:3} $ \tv { a } \doteq \rwildcard { X } $
\end { enumerate}
% Constraints of the form $\tv{a} \doteq \rwildcard{X}$ are also possible.
% should we add those to the \Delta environment?
% How about removing them completely from the result set? Check with soundness condition
%Each type placeholder $\tv{a}$ must solely appear on the left side of a constraint.
\unify { } fails if there is any $ \tv { a } \doteq \type { T } $ such that $ \tv { a } $ occurs in $ \type { T } $ .
For the cases \ref { item:1} , \ref { item:2} , and \ref { item:3} the placeholder $ \tv { a } $
cannot appear anywhere else in the constraint set.
Otherwise the generation rules \rulename { GenSigma} and \rulename { GenDelta} will not be able to process every constraint.
% After applying the GenDelta and GenSigma rules unifiers $\sigma$ do not contain
% a unifier of the form $\tv{a} \to \tv{b}$.
% 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}$.
% \begin{displaymath}
% \deduction{
% \wildcardEnv \cup \set{\wildcard{B}{\type{G}}{\type{G'}}} \vdash C \implies \Delta, \sigma
% }{
% \wildcardEnv \vdash C \implies \Delta \cup \set{\wildcard{B}{\type{G}}{\type{G'}}}, \sigma
% }\quad \text{tph}(\type{G}) = \emptyset, \text{tph}(\type{G'}) = \emptyset,
% \rwildcard{B} \notin \text{dom}(\Delta)
% \quad \rulename{AddDelta}
% \end{displaymath}
\begin { figure}
\begin { center}
\fbox {
\begin { tabular} [t]{ l@{ ~} l}
\rulename { GenDelta}
& $
\deduction {
2024-02-02 12:22:55 +00:00
\wildcardEnv \vdash C \cup \set { \tv { b} \lessdot \type { T} } \implies \Delta , \sigma
2023-12-27 13:29:33 +00:00
} {
2024-02-02 12:22:55 +00:00
\wildcardEnv \vdash [\type { B} /\tv { b} ]C \implies \Delta \cup \set { \wildcard { B} { \type { T} } { \bot } } , \sigma \cup \set { \tv { b} \to \type { B} }
2023-12-27 13:29:33 +00:00
} \quad
\begin { array} { l}
2024-02-02 12:22:55 +00:00
\tph (\type { T} ) = \emptyset , \text { fv} (\type { T} ) \subseteq \Delta \cup \Delta _ { in} \\
\rwildcard { B} \ \text { fresh} , \tv { b} \notin \text { dom} (\sigma ), \Delta , \Delta _ { in} \vdash \type { T} \ \ok
2023-12-27 13:29:33 +00:00
\end { array}
$
\\ \\
\rulename { GenSigma}
& $
\deduction {
\wildcardEnv \vdash C \cup
\set { \tv { a} \doteq \type { T} } \implies \Delta , \sigma
} {
\wildcardEnv \vdash C \implies \Delta , \sigma \cup
\set { \tv { a} \to \type { T} }
} \quad
\begin { array} { l}
2024-01-04 00:33:36 +00:00
\tph (\type { T} ) = \emptyset \\ %,\, \text{fv}(\type{T}) \subseteq \Delta \\ % T ok implies that
2024-02-02 12:22:55 +00:00
\tv { a} \notin \text { dom} (\sigma ),\, \Delta , \Delta _ { in} \vdash \type { T} \ \ok
2023-12-27 13:29:33 +00:00
\end { array}
$
\\ \\
\end { tabular} }
\end { center}
\caption { Generate result}
\label { fig:generation-rules}
\end { figure}
2024-01-21 13:31:48 +00:00
\subsection { Capture Conversion during Unification}
The \unify { } algorithm applies a capture conversion when needed.
A constraint of the form $ \wcNtype { \Delta ' } { N } \lessdot \type { T } $ ,
where $ \text { fv } ( \type { T } ) \neq \emptyset $ is not solvable without capture conversion.
\unify { } converts those constraints to $ \type { N } \lessdot \type { T } $ .
This is only possible for subtype constraints which originated from a method call.
Capture conversion only works with constraints containing free variables.
It also introduces fresh free variables into the constraint set.
Both have to be regulated.
It is not allowed to substitute free type variables freely.
The algorithm introduces a new type of variables: $ \wtv { a } $ .
\unify { } treats those as free type variables.
This makes it possible to replace a $ \wtv { a } $ with a captured wildcard variable
without having to worry about introducing free type variables at unwanted places.
The challenge for a type inference algorithm is to apply capture conversion during type inference.
Given a program
\begin { verbatim}
class TypeInferenceExample{
m(l){
return swap(make(l));
}
}
\end { verbatim}
During the time of the type inference algorithm the type of the parameter \texttt { l} is not known.
Due to the call to the method \texttt { make} it is clear that it has to be a subtype of
\texttt { List} .
These subtype relations are expressed with constraints.
$ \tv { l } \lessdot \exptype { List } { \tv { a } } $ in this case.
$ \tv { l } $ and $ \tv { a } $ are type placeholders.
$ \tv { l } $ is a type placeholder for the method parameter \texttt { l} .
One correct solution for this constraint is the substitution $ \tv { l } \doteq \exptype { List } { \type { Object } } $ ,
which leads to the program:
\begin { verbatim}
class TypeInferenceExample{
Pair<Object, Object> m(List<Object> l){
return swap(make(l));
}
}
\end { verbatim}
But $ \tv { l } \doteq \wctype { \rwildcard { X } } { List } { \rwildcard { X } } $ is also a possible solution.
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}
\item Capture conversion is not allowed for every constraint.
\item Capture Converted variables are not allowed to leave their scope
\item \unify { } generates type substitution which cannot be translated to Java types.
\end { itemize}
