constraints.tex

@@ -1,4 +1,4 @@
-\section{Constraint generation}\label{chapter:constraintGeneration}
+\section{Constraint generation}
 % Our type inference algorithm is split into two parts.
 % A constraint generation step \textbf{TYPE} and a \unify{} step.
 

tRules.tex

@@ -3,28 +3,21 @@
 The input syntax for our algorithm is shown in figure \ref{fig:syntax}
 and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}.
 
-Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
+The algorithm presented in this paper is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
+Additional features like overriding methods and method overloading can be added by copying the respective parts from there.
 The input language is designed to showcase type inference involving existential types.
-Method call rule T-Call is the most interesting part, because it emulates the behaviour of a Java method call,
+We introduce the type rule T-Call which emulates a Java method call,
 where existential types are implicitly \textit{opened} and \textit{closed}.
-
-%The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}.
-%and is solely used for examples.
-The calculus does not include method overloading or method overriding for simplicity reasons.
-Type inference for both are described in \cite{TIforFGJ} and can be added to this algorithm accordingly.
-Our algorithm is designed for extensibility with the final goal of full support for Java.
-\unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
-Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
-
-%Additional features like overriding methods and method overloading can be added by copying the respective parts from there.
+The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}
+and is solely used for examples.
 %Additional features can be easily added by generating the respective constraints (Plümicke hier zitieren)
 
-% The type system in \cite{WildcardsNeedWitnessProtection} allows a method to \textit{override} an existing method declaration in one of its super classes,
-% but only by a method with the exact same type.
-% The type system presented here does not allow the \textit{overriding} of methods.
-% Our type inference algorithm consumes the input classes in succession and could only do a type check instead of type inference
-% on overriding methods, because their type is already determined.
-% Allowing overriding therefore has no implication on our type inference algorithm.
+The type system in \cite{WildcardsNeedWitnessProtection} allows a method to \textit{override} an existing method declaration in one of its super classes,
+but only by a method with the exact same type.
+The type system presented here does not allow the \textit{overriding} of methods.
+Our type inference algorithm consumes the input classes in succession and could only do a type check instead of type inference
+on overriding methods, because their type is already determined.
+Allowing overriding therefore has no implication on our type inference algorithm.
 
 \begin{figure}
 $

unify.tex

@@ -463,24 +463,24 @@ Their upper and lower bounds are fresh type variables.
     \end{array}
     $
   \\\\
-        \rulename{Adopt}
-        & $
-        \begin{array}[c]{@{}ll}
-        \begin{array}[c]{l}
-          \wildcardEnv \vdash C \cup \, \set{
-           \tv{b} \lessdot \tv{a},
-\tv{a} \lessdot \type{N}, \tv{b} \lessdot \type{N'}} \\ 
-          \hline
-          \vspace*{-0.4cm}\\
-          \wildcardEnv \vdash C \cup \, \set{
- \tv{b} \lessdot \type{N},
-           \tv{b} \lessdot \tv{a},
-\tv{a} \lessdot \type{N} , \tv{b} \lessdot \type{N'}
-           }
-        \end{array}
-        \end{array}
-        $
-      \\\\
+%         \rulename{Adopt}
+%         & $
+%         \begin{array}[c]{@{}ll}
+%         \begin{array}[c]{l}
+%           \wildcardEnv \vdash C \cup \, \set{
+%            \tv{b} \lessdot \tv{a},
+% \tv{a} \lessdot \type{N}, \tv{b} \lessdot \type{N'}} \\ 
+%           \hline
+%           \vspace*{-0.4cm}\\
+%           \wildcardEnv \vdash C \cup \, \set{
+%  \tv{b} \lessdot \type{N},
+%            \tv{b} \lessdot \tv{a},
+% \tv{a} \lessdot \type{N} , \tv{b} \lessdot \type{N'}
+%            }
+%         \end{array}
+%         \end{array}
+%         $
+%       \\\\
   \rulename{Adapt}
   & 
   $
@@ -747,28 +747,28 @@ This builds a search tree over multiple possible solutions.
         \end{array}
         $
       \\\\ 
-      \rulename{Settle}
-      & $
-      \begin{array}[c]{l}
-        \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
-        \tv{a} \lessdot^* \tv{b}}
-        \\
-        \hline
-        \wildcardEnv \vdash C \cup \set{  \tv{a} \lessdot^* \tv{b}, \tv{b} \lessdot \type{N}  }
-      \end{array}
-      $
-    \\\\ 
-    \rulename{Raise}
-    & $
-    \begin{array}[c]{l}
-      \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
-      \tv{a} \lessdot \tv{b}}
-      \\
-      \hline
-      \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b}  }
-    \end{array}
-    $
-  \\\\ 
+  %     \rulename{Settle}
+  %     & $
+  %     \begin{array}[c]{l}
+  %       \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
+  %       \tv{a} \lessdot^* \tv{b}}
+  %       \\
+  %       \hline
+  %       \wildcardEnv \vdash C \cup \set{  \tv{a} \lessdot^* \tv{b}, \tv{b} \lessdot \type{N}  }
+  %     \end{array}
+  %     $
+  %   \\\\ 
+  %   \rulename{Raise}
+  %   & $
+  %   \begin{array}[c]{l}
+  %     \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
+  %     \tv{a} \lessdot \tv{b}}
+  %     \\
+  %     \hline
+  %     \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b}  }
+  %   \end{array}
+  %   $
+  % \\\\ 
     \end{tabular}}
   \end{center}
 \caption{Step 2 branching: Multiple rules can be applied to the same constraint}
@@ -860,25 +860,25 @@ $
 \end{tabular}}
 \end{center}
 
-% \textbf{Step 4:}
-% If there are constraints of the form $(\tv{a} \lessdot \tv{b})$ remaining in the constraint set then
-% apply the \rulename{Sub-Elim} rule and start over with step 1.
-% Otherwise continue to step 5.
-% \begin{center}
-%   \fbox{
-%   \begin{tabular}[t]{l@{~}l}
-%     \rulename{SubElim} 
-%     & $\begin{array}[c]{l}
-%       \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \tv{b}}\\
-%       \hline
-%       [\tv{a}/\tv{b}]\wildcardEnv \vdash [\tv{a}/\tv{b}]C \cup \set{ \tv{b} \doteq \tv{a} }
-%     \end{array}
-%     $
-% \end{tabular}}
-% \end{center}
+\textbf{Step 4:}
+If there are constraints of the form $(\tv{a} \lessdot \tv{b})$ remaining in the constraint set then
+apply the \rulename{Sub-Elim} rule and start over with step 1.
+Otherwise continue to step 5.
+\begin{center}
+  \fbox{
+  \begin{tabular}[t]{l@{~}l}
+    \rulename{SubElim} 
+    & $\begin{array}[c]{l}
+      \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \tv{b}}\\
+      \hline
+      [\tv{a}/\tv{b}]\wildcardEnv \vdash [\tv{a}/\tv{b}]C \cup \set{ \tv{b} \doteq \tv{a} }
+    \end{array}
+    $
+\end{tabular}}
+\end{center}
 
 \noindent
-\textbf{Step 4:}
+\textbf{Step 5:}
 We apply the rules in figure \ref{fig:cleanup-rules} exhaustively and proceed with step 6.
 
 \begin{figure}
@@ -886,14 +886,6 @@ We apply the rules in figure \ref{fig:cleanup-rules} exhaustively and proceed wi
       \leavevmode
       \fbox{
       \begin{tabular}[t]{l@{~}l}
-\rulename{SubElim} 
-& $\begin{array}[c]{l}
-  \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \tv{b}}\\
-  \hline
-  [\tv{a}/\tv{b}]\wildcardEnv \vdash [\tv{a}/\tv{b}]C \cup \set{ \tv{b} \doteq \tv{a} }
-\end{array}
-$
-\\\\
 \rulename{Ground}
 & $\begin{array}[c]{@{}ll}
 \begin{array}[c]{l}