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

Rework Capture COnstraints chapter

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-05-21 19:16:13 +02:00
parent 6a679f8ab0
commit 04fc640903
1 changed files with 55 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

83
constraints.tex
View File

@ -1,39 +1,12 @@
\section{Capture Constraints}
%TODO: General Capture Constraint explanation
The equality relation on Capture constraints is not reflexive.
A capture constraint is never equal to another capture constraint even when structurally the same
($\type{T} \lessdotCC \type{S} \neq \type{T} \lessdotCC \type{S}$).
This is necessary to solve challenge \ref{challenge:1}.
A capture constraint is bound to a specific let statement.
For example the statement \lstinline{let x = v in x.get()}
generates a constraint like $\tv{x} \lessdotCC \exptype{List}{\wtv{a}}$.
This means that the type variable $\tv{x}$ on the left side of the capture constraint is actually a placeholder
for a type that is subject to capture conversion.
It is possible that two syntactically equal capture constraints evolve
during constraint generation or the \unify{} process.
Take the two constraints in listing \ref{lst:sameConstraints}
which originate from the \texttt{concat} method invocation in listing \ref{lst:faultyConcat} for example.
To illustrate their connection to a let statement each capture constraint is annoted with its respective variable.
After a capture conversion step the constraints become
$\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}},
\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}
$
making obvious that this constraint set is unsolvable.
\textit{Note:}
In the special case \lstinline{let x = v in concat(x,x)} the constraint would look like
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}},
\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
and we could actually delete one of them without loosing information.
But this case will never occur in our algorithm, because the let statements for our input programs are generated by a ANF transformation (see \ref{sec:anfTransformation}).
In this paper we do not annotate capture constraint with their source let statement.
Instead we consider every capture constraint as distinct to other constraints even when syntactically the same,
because we know that each capture constraint originates from a different let statement.
\textit{Hint:} An implementation of this algorithm has to consider that seemingly equal capture constraints are actually not the same
and has to allow doubles in the constraint set.
Capture Constraints are bound to a variable.
For example a let statement like \lstinline{let x = v in x.get()} will create the capture constraint
$\tv{x} \lessdotCC_x \exptype{List}{\wtv{a}}$.
This time we annotated the capture constraint with an $x$ to show its relation to the variable \texttt{x}.
Let's do the same with the constraints generated by the \texttt{concat} method invocation in listing \ref{lst:faultyConcat},
creating the constraints \ref{lst:sameConstraints}.
\begin{figure}
\begin{minipage}[t]{0.49\textwidth}
@ -47,12 +20,51 @@ let x = v in
\hfill
\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[caption=Annotated constraints,mathescape=true,style=constraints,label=lst:sameConstraints]
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{y} \exptype{List}{\wtv{a}}$
$\tv{x} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{x}$
$\tv{y} \lessdotCC_\texttt{y} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{y}$
\end{lstlisting}
\end{minipage}
\end{figure}
During the \unify{} process it could happen that two syntactically equal capture constraints evolve,
but they are not the same because they are each linked to a different let introduced variable.
In this example this happens when we substitute $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\tv{x}$ and $\tv{y}$
resulting in:
%For example by substituting $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{x}]$ and $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{y}]$:
\begin{displaymath}
\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_x \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_y \exptype{List}{\wtv{a}}
\end{displaymath}
Thanks to the original annotations we can still see that those are different constraints.
After \unify{} uses the \rulename{Capture} rule on those constraints
it gets obvious that this constraint set is unsolvable:
\begin{displaymath}
\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}},
\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}
\end{displaymath}
%In this paper we do not annotate capture constraint with their source let statement.
The rest of this paper will not annotate capture constraints with variable names.
Instead we consider every capture constraint as distinct to other capture constraints even when syntactically the same,
because we know that each of them originates from a different let statement.
\textit{Hint:} An implementation of this algorithm has to consider that seemingly equal capture constraints are actually not the same
and has to allow doubles in the constraint set.
% %We see the equality relation on Capture constraints is not reflexive.
% A capture constraint is never equal to another capture constraint even when structurally the same
% ($\type{T} \lessdotCC \type{S} \neq \type{T} \lessdotCC \type{S}$).
% This is necessary to solve challenge \ref{challenge:1}.
% A capture constraint is bound to a specific let statement.
\textit{Note:}
In the special case \lstinline{let x = v in concat(x,x)} the constraints would look like
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}},
\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
and we could actually delete one of them without loosing information.
But this case will never occur in our algorithm, because the let statements for our input programs are generated by a ANF transformation (see \ref{sec:anfTransformation}).
\section{Constraint generation}\label{chapter:constraintGeneration}
% Our type inference algorithm is split into two parts.
% A constraint generation step \textbf{TYPE} and a \unify{} step.
@ -143,6 +155,7 @@ $\begin{array}{lrcl}
\end{figure}
\begin{figure}
\center
$
\begin{array}{lrcl}
%\hline