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

Match example

Browse Source
This commit is contained in:
JanUlrich 2024-05-22 12:06:51 +02:00
parent a74e20802c
commit 95636f3379
1 changed files with 206 additions and 161 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

367
unify.tex
View File

@ -247,10 +247,192 @@ Afterwards \rulename{Prepare} can be used eventually leading to the erasure of t
} }
\end{displaymath} \end{displaymath}
Note that the \rulename{Prepare} rule is always applied together with the \rulename{Capture} and the \rulename{Reduce} rule: 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 \rulename{Trim} removes unused wildcard declarations.
whereas \rulename{Clear} and \rulename{Exclude} remove wildcard placeholders or wildcards to \rulename{Clear} and \rulename{Exclude} remove wildcard placeholders or wildcards to
allow the constraint to be processed by \rulename{Prepare}. allow the constraint to be processed by \rulename{Prepare}.
\unify{} keeps $\tv{a} \lessdot \type{T}$ constraints as long as possible.
The \rulename{Match} rule reduces two $\tv{a} \lessdot \type{T}$ constraints to one.
There has to be a common subtype $\type{C}$ of $\type{D}$ and $\type{D'}$ for this rule to work
expressed as premises $\type{C} \ll \type{D}$ and $\type{C} \ll \type{D'}$.
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}
For example the constraints $\tv{a} \lessdot \type{String}$ and $\tv{a} \lessdot \type{Integer}$
are unsolvable, because there exists no common subtype of $\type{String}$ and $\type{Integer}$.
Whereas the constraints $\tv{a} \lessdotCC \exptype{List}{\type{Integer}}$ and
$\tv{a} \lessdotCC \exptype{List}{\tv{b}}$ can be processed by \rulename{Match}:
\begin{displaymath}
\prftree[r]{\rulename{Tame}}{
\prftree[r]{\rulename{Reduce}}{
\prftree[r]{\rulename{Capture}}{
\prftree[r]{\rulename{Match}}{
\tv{a} \lessdotCC \exptype{List}{\type{Integer}}, \tv{a} \lessdotCC \exptype{List}{\tv{b}}
}{
\begin{array}{l}
\tv{a} \lessdot \wctype{\wildcard{A}{\tv{u}}{\tv{l}}}{List}{\rwildcard{A}}, \\
\wctype{\wildcard{A}{\tv{u}}{\tv{l}}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\type{Integer}}, \\
\wctype{\wildcard{A}{\tv{u}}{\tv{l}}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\tv{b}}
\end{array}
}}{
\wildcard{A}{\tv{u}}{\tv{l}} \vdash
\begin{array}[t]{l}
\tv{a} \lessdot \wctype{\wildcard{A}{\tv{u}}{\tv{l}}}{List}{\rwildcard{A}}, \\
\exptype{List}{\rwildcard{A}} \lessdot \exptype{List}{\type{Integer}}, \\
\exptype{List}{\rwildcard{A}} \lessdot \exptype{List}{\tv{b}}
\end{array}
}}{
\wildcard{A}{\tv{u}}{\tv{l}} \vdash \tv{a} \lessdot \wctype{\wildcard{A}{\tv{u}}{\tv{l}}}{List}{\rwildcard{A}},
\rwildcard{A} \doteq \type{Integer}, \rwildcard{A} \doteq \tv{b}
}}{
\wildcard{A}{\tv{u}}{\tv{l}} \vdash \tv{a} \lessdot \wctype{\wildcard{A}{\tv{u}}{\tv{l}}}{List}{\rwildcard{A}},
\tv{u} \doteq \type{Integer}, \tv{l} \doteq \type{Integer}, \tv{u} \doteq \tv{b}
}
\end{displaymath}
After \rulename{Subst} and \rulename{Same} the remaining constraints are $\tv{b} \doteq \type{Integer}$ and
$\tv{a} \lessdot \wctype{\wildcard{A}{\type{Integer}}{\type{Integer}}}{List}{\rwildcard{A}}$
%which is equal to $\tv{a} \lessdot \exptype{List}{\type{Integer}}$ and additionally we have $\tv{b} \doteq \type{Integer}$.
\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_1 \wctype{\Delta}{D}{\ol{T}}, \tv{a} \lessdot_2 \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_1 \wctype{\Delta}{D}{\ol{T}}, \\
\wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}}
\lessdot_2 \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
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{Adopt}
& $
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \, \set{
\tv{b} \lessdot_1 \tv{a},
\tv{a} \lessdot_2 \type{N}, \tv{b} \lessdot_3 \type{N'}} \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash C \cup \, \set{
\tv{b} \lessdot \type{N},
\tv{b} \lessdot_1 \tv{a},
\tv{a} \lessdot_2 \type{N} , \tv{b} \lessdot_3 \type{N'}
}
\end{array}
\end{array}
$
\\\\
\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}
\subsection{Adding Wildcards to the mix} \subsection{Adding Wildcards to the mix}
%\unify{} is able to create wildcard solutions even when the input set of constraints do not contain any wildcard variables. %\unify{} is able to create wildcard solutions even when the input set of constraints do not contain any wildcard variables.
%Input constraints originating from a completely untyped input program do not contain any existential types. %Input constraints originating from a completely untyped input program do not contain any existential types.
@ -590,10 +772,6 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
\end{description} \end{description}
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 as $\wtv{a}$ it can be used by the \rulename{Subst-WC} rule in step 1.
With \texttt{C} being class names and \texttt{A} being wildcard names. With \texttt{C} being class names and \texttt{A} being wildcard names.
The wildcard type $\wildcard{X}{U}{L}$ consist of an upper bound $\type{U}$, a lower bound $\type{L}$ The wildcard type $\wildcard{X}{U}{L}$ consist of an upper bound $\type{U}$, a lower bound $\type{L}$
and a name $\mathtt{X}$. and a name $\mathtt{X}$.
@ -617,36 +795,10 @@ This is used by the \rulename{Tame} rule.
\item[$\tph{}$] returns all type placeholders inside a given type. \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}}$ \textit{Example:} $\tph(\wctype{\wildcard{X}{\tv{a}}{\bot}}{Pair}{\wtv{b},\rwildcard{X}}) = \set{\tv{a}, \wtv{b}}$
\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}\\ %\textbf{Wildcard renaming}\\
\item[Wildcard renaming:] \item[Wildcard renaming:]
The \rulename{reduce} rule separates wildcards from their environment. The \rulename{Reduce} rule separates wildcards from their environment.
At this point each wildcard gets a new and unique name. 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: To only rename the respective wildcards the reduce rule renames wildcards up to alpha conversion:
($[\ol{C}/\ol{B}]$ in the \rulename{reduce} rule) ($[\ol{C}/\ol{B}]$ in the \rulename{reduce} rule)
@ -727,6 +879,19 @@ which are used for the upper and lower bounds.
% if there are a <. List<x?> constraints remaining in the end, then this can be a sign of a irregular input constraint set. % if there are a <. List<x?> constraints remaining in the end, then this can be a sign of a irregular input constraint set.
\unify{} must not replace normal type placeholders with free variables
except variables initially passed by $\Delta_{in}$.
The \rulename{Subst} rule checks if a type $\type{T}$ contains any
free variables or wildcard placeholders before replacing a normal type placeholder with it.
This ensures that free variables are never substituted for normal type placeholders.
\rulename{Subst-WC} does not need to do that and can freely replace wildcard placehodlers with types despite their free variables.
We do not keep replacements for wildcard placeholders and they also will not show up in the final type solution.
If the \rulename{Subst} rule is not applicable then either the \rulename{Normalize}
or \rulename{Contract} transformation has to be used to remove wildcard placeholders and
wildcards.
\begin{figure} \begin{figure}
\begin{center} \begin{center}
\leavevmode \leavevmode
@ -779,6 +944,9 @@ C \cup [\type{U}/\type{A}]\set{\ntv{a} \doteq \type{T}, \type{L} \doteq \type{U}
\caption{Substitution rules}\label{fig:subst-rules} \caption{Substitution rules}\label{fig:subst-rules}
\end{figure} \end{figure}
% all possible variations have to be converted % all possible variations have to be converted
There are n different rules to deal with $\type{N} \lessdot \type{N}$ constraints. There are n different rules to deal with $\type{N} \lessdot \type{N}$ constraints.
Prepare, Capture, Reduce, Trim, Clear, Exclude, Adapt Prepare, Capture, Reduce, Trim, Clear, Exclude, Adapt
@ -916,124 +1084,6 @@ Prepare, Capture, Reduce, Trim, Clear, Exclude, Adapt
\caption{Rules for normal placeholders}\label{fig:reduce-rules} \caption{Rules for normal placeholders}\label{fig:reduce-rules}
\end{figure} \end{figure}
\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_1 \wctype{\Delta}{D}{\ol{T}}, \tv{a} \lessdot_2 \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_1 \wctype{\Delta}{D}{\ol{T}}, \\
\wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}}
\lessdot_2 \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
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{Adopt}
& $
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \, \set{
\tv{b} \lessdot_1 \tv{a},
\tv{a} \lessdot_2 \type{N}, \tv{b} \lessdot_3 \type{N'}} \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash C \cup \, \set{
\tv{b} \lessdot \type{N},
\tv{b} \lessdot_1 \tv{a},
\tv{a} \lessdot_2 \type{N} , \tv{b} \lessdot_3 \type{N'}
}
\end{array}
\end{array}
$
\\\\
\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}
\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.
@ -1366,20 +1416,15 @@ $\begin{array}{c}
\end{NiceTabular} \end{NiceTabular}
\subsection{Capture Conversion during Unification} \subsection{Capture Conversion during Unification}
The \unify{} algorithm applies a capture conversion when needed. % The \unify{} algorithm applies a capture conversion when needed.
A constraint of the form $\wcNtype{\Delta'}{N} \lessdot \type{T}$, % A constraint of the form $\wcNtype{\Delta'}{N} \lessdot \type{T}$,
where $\text{fv}(\type{T}) \neq \emptyset$ is not solvable without capture conversion. % where $\text{fv}(\type{T}) \neq \emptyset$ is not solvable without capture conversion.
\unify{} converts those constraints to $\type{N} \lessdot \type{T}$. % \unify{} converts those constraints to $\type{N} \lessdot \type{T}$.
This is only possible for subtype constraints which originated from a method call. % This is only possible for subtype constraints which originated from a method call.
Capture conversion only works with constraints containing free variables. Capture conversion only works with constraints containing free variables.
It also introduces fresh free variables into the constraint set. It also introduces fresh free variables into the constraint set.
Both have to be regulated. 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. The challenge for a type inference algorithm is to apply capture conversion during type inference.
Given a program Given a program