Add Prepare explanation. Restructure
This commit is contained in:
JanUlrich
parent
4890fa79c2
commit
11dd427c3f
419
unify.tex
419
unify.tex
@ -25,35 +25,10 @@ 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 atleas one constraint of the form
|
The \rulename{Subst} rule 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$.
|
||||||
|
|
||||||
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{figure}
|
||||||
\begin{center}
|
\begin{center}
|
||||||
\leavevmode
|
\leavevmode
|
||||||
@ -114,6 +89,167 @@ Note that the new generated constraint $\wtv{b} \lessdot \type{String}$ is a nor
|
|||||||
\caption{Wildcard reduce rules}\label{fig:wildcard-rules}
|
\caption{Wildcard reduce rules}\label{fig:wildcard-rules}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
|
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$).
|
||||||
|
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{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}(\type{N'}) \subseteq \Delta_{in} \\
|
||||||
|
\text{wtv}(\type{N'}) = \emptyset
|
||||||
|
\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}
|
||||||
|
|
||||||
|
An existential type can never be a subtype of a regular type:
|
||||||
|
$\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \nless: \exptype{C}{\rwildcard{X}}$.
|
||||||
|
This is a problem for constraints of the form $\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdot \type{N}$.
|
||||||
|
Take the constraint $\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdot \exptype{C}{\wtv{a}}$ for example.
|
||||||
|
After applying a reduction we get $\rwildcard{X} \doteq \wtv{a}$ which is not a valid solution.
|
||||||
|
The problem is that we loose the information of the left side being an existential type with the reduction step.
|
||||||
|
Therefore we have to assure beforehand that errors (like $\rwildcard{X} \doteq \wtv{a}$ in this example) cannot occur.
|
||||||
|
But we alsod don't want to exclude reductions for these kind of constraints in general.
|
||||||
|
The solution is to check 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{Reduce}}{
|
||||||
|
\prftree[r]{\rulename{Capture}}{
|
||||||
|
\prftree[r]{\rulename{Prepare}}{
|
||||||
|
\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\ntv{x}}}
|
||||||
|
}
|
||||||
|
{
|
||||||
|
\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\exptype{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\ntv{x}}}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
{
|
||||||
|
\wildcard{X}{\tv{u}}{\tv{l}} \vdash \exptype{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}}
|
||||||
|
}}
|
||||||
|
{
|
||||||
|
\wildcard{X}{\tv{u}}{\tv{l}} \vdash \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}
|
||||||
|
Note that the \rulename{Prepare} rule is always applied together with the \rulename{Capture} and the \rulename{Reduce} rule:
|
||||||
|
\rulename{Trim} removes unused wildcard declarations
|
||||||
|
whereas \rulename{Clear} and \rulename{Exclude} remove wildcard placeholders or wildcards to
|
||||||
|
allow the constraint to be processed by \rulename{Prepare}.
|
||||||
|
|
||||||
\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.
|
||||||
@ -899,95 +1035,6 @@ Prepare, Capture, Reduce, Trim, Clear, Exclude, Adapt
|
|||||||
\caption{Constraint reduce rules}\label{fig:reduce-rules}
|
\caption{Constraint reduce rules}\label{fig:reduce-rules}
|
||||||
\end{figure}
|
\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}
|
\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.
|
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.
|
||||||
|
|
||||||
@ -1275,152 +1322,10 @@ $
|
|||||||
\label{fig:generation-rules}
|
\label{fig:generation-rules}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
\begin{figure}
|
|
||||||
|
|
||||||
\begin{center}
|
|
||||||
\fbox{
|
|
||||||
\begin{tabular}[t]{l@{~}l}
|
|
||||||
\rulename{Equals} %TODO
|
|
||||||
& $
|
|
||||||
\begin{array}[c]{l}
|
|
||||||
\wildcardEnv \vdash C \cup \, \set{ \wcNtype{\Delta}{N} \doteq \wcNtype{\Delta'}{N'} } \\
|
|
||||||
\hline
|
|
||||||
\vspace*{-0.4cm}\\
|
|
||||||
\wildcardEnv \vdash C \cup \,
|
|
||||||
\set{
|
|
||||||
\wcNtype{\Delta}{N} \lessdot \wcNtype{\Delta'}{N'}, \wcNtype{\Delta'}{N'} \lessdot \wcNtype{\Delta}{N}
|
|
||||||
}
|
|
||||||
\end{array} %\quad |\Delta| = |\Delta'|
|
|
||||||
% \quad \text{fv}(\type{N}) = \text{fv}(\type{N'}) = \emptyset
|
|
||||||
$
|
|
||||||
\\\\
|
|
||||||
\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
|
|
||||||
C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdotCC \type{T} } \\
|
|
||||||
\hline
|
|
||||||
\vspace*{-0.4cm}\\
|
|
||||||
\wildcardEnv \cup \overline{\wildcard{C}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{U}}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{L}}}
|
|
||||||
\vdash C \cup \, \set{
|
|
||||||
[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} \lessdot \type{T} }
|
|
||||||
\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}
|
|
||||||
$
|
|
||||||
\\\\
|
|
||||||
\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{ \type{N} \lessdot \type{N'} } \\
|
|
||||||
\hline
|
|
||||||
\vspace*{-0.4cm}\\
|
|
||||||
\wildcardEnv \vdash
|
|
||||||
C \cup \, \set{ \type{N} \lessdotCC \type{N'} } \\
|
|
||||||
\end{array}
|
|
||||||
%\quad \ol{Y} = \textit{fresh}(\ol{X})
|
|
||||||
\quad \begin{array}[c]{l}
|
|
||||||
\text{fv}(\type{N'}) \subseteq \Delta_{in} \\
|
|
||||||
\text{wtv}(\type{N'}) = \emptyset
|
|
||||||
\end{array}
|
|
||||||
\end{array}
|
|
||||||
$
|
|
||||||
\end{tabular}}
|
|
||||||
\end{center}
|
|
||||||
\caption{Type Reduction rules}\label{fig:reductionRules}
|
|
||||||
\end{figure}
|
|
||||||
|
|
||||||
\subsection{Explanations}
|
\subsection{Explanations}
|
||||||
|
|
||||||
%The type reduction is done by the rules in figure \ref{fig:reductionRules}
|
%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.
|
|
||||||
%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}
|
\subsection{Examples}
|
||||||
\textit{Example} of the type reduction rules in figure \ref{fig:reductionRules} with the input
|
\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}}$
|
$\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$
|
||||||
|
|||||||
Loading…
Reference in New Issue
Block a user