From a74e20802c97114e708e4f98d2b3a7aefb1fbf7d Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Tue, 21 May 2024 20:53:15 +0200 Subject: [PATCH] =?UTF-8?q?Cleanup.=20Explain=20\=C3=90elta=5Fin?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- constraints.tex | 35 ++++++++--------------------------- unify.tex | 2 +- 2 files changed, 9 insertions(+), 28 deletions(-) diff --git a/constraints.tex b/constraints.tex index 1c98c98..7cd5e74 100644 --- a/constraints.tex +++ b/constraints.tex @@ -1,4 +1,4 @@ -\section{Capture Constraints} +\subsection{Capture Constraints} %TODO: General Capture Constraint explanation Capture Constraints are bound to a variable. @@ -66,9 +66,6 @@ But this case will never occur in our algorithm, because the let statements for \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. - % Method names are not unique. % It is possible to define the same method in multiple classes. % The \TYPE{} algorithm accounts for that by generating Or-Constraints. @@ -94,9 +91,6 @@ We will focus on those two parts where also the new capture constraints and wild %They will be added by an ANF transformation (see chapter \ref{sec:anfTransformation}). Before generating constraints the input is transformed by an ANF transformation (see section \ref{sec:anfTransformation}). -Capture conversion is only needed for wildcard types, -but we don't know which expressions will spawn wildcard types because there are no type annotations yet. -We preemptively enclose every expression in a let statement before using it as a method argument. %Constraints are generated on the basis of the program in A-Normal form. %After adding the missing type annotations the resulting program is valid under the typing rules in \cite{WildFJ}. @@ -193,22 +187,6 @@ So no types like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ or Type variables declared in the class header are passed to \unify{}. Those type variables count as regular types and can be held by normal type placeholders. - -There are two different types of constraints: -\begin{description} -\item[$\lessdot$] \textit{Example:} - -$\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}$ - -\noindent -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}$. -This paper describes a \unify{} algorithm to solve these constraints and calculate a type solution $\sigma$. -For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$. -\item[$\lessdotCC$] TODO -% The \fjtype{} algorithm assumes capture conversions for every method parameter. -\end{description} - %Why do we need a constraint generation step? %% The problem is NP-Hard %% a method call, does not know which type it will produce @@ -216,6 +194,7 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi %NO equals constraints during the constraint generation step! \begin{figure}[tp] + \center \begin{tabular}{lcll} $C $ &$::=$ &$\overline{c}$ & Constraint set \\ $c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \lessdotCC \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\ @@ -233,17 +212,19 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi \begin{figure}[tp] \begin{gather*} \begin{array}{@{}l@{}l} - \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\ol{X} \triangleleft \ol{N}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\ + \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\overline{\type{X} \triangleleft \type{N}}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\ & \begin{array}{ll@{}l} \textbf{let} & \ol{\methodAssumption} = \set{ \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \mid \set{ \mv{m}(\ol{x}) = \expr{e} } \in \ol{M}, \, \tv{a}, \ol{\tv{a}}\ \text{fresh} } \\ - \textbf{in} - & \begin{array}[t]{l} + & \Delta = \set{ \overline{\wildcard{X}{\type{N}}{\bot}} } \\ + & C = \begin{array}[t]{l} \set{ \typeExpr(\mtypeEnvironment \cup \ol{\methodAssumption} \cup \set{\mv{this} : \exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}} }, \texttt{e}, \tv{a}) \\ \quad \quad \quad \quad \mid \set{ \mv{m}(\ol{x}) = \expr{e} } \in \ol{M},\, \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \in \ol{\methodAssumption}} - \end{array} + \end{array} \\ + \textbf{in} + & (\Delta, C) \end{array} \end{array} \end{gather*} diff --git a/unify.tex b/unify.tex index 682bbf2..eca4499 100644 --- a/unify.tex +++ b/unify.tex @@ -19,7 +19,7 @@ Afterwards \unify{} substitutes type placeholder $\tv{a}$ with $\type{T}$. This is done until a substitution for all type placeholders and therefore a valid solution is reached. The reduction and substitutions are done in the first step of the algorithm. The algorithms state consists out of a wildcard environment and a constraint set ($\wildcardEnv \vdash C$). -Initially they are set to $\Delta_{in}$ and the input constraints. +Initially they are set to the input environment $\Delta_{in}$ and the input constraints. Each calculation step of the algorithm is expressed as a transformation rule consisting of three parts. The input is shown above the line, the output below, and additional premises are displayed on the right side.