Cleanup. Explain \Ðelta_in

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*}

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.