Intro to type rules

constraints.tex

@@ -1,4 +1,4 @@
-\section{Constraint generation}
+\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.
 

tRules.tex

@@ -3,21 +3,28 @@
 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}.
 
-The algorithm presented in this paper is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
+Our algorithm 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.
-We introduce the type rule T-Call which emulates a Java method call,
+Method call rule T-Call is the most interesting part, because it emulates the behaviour of 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 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.
 %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,
+% 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.
+% but only by a method with the exact same type.
-The type system presented here does not allow the \textit{overriding} of methods.
+% 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
+% 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.
+% on overriding methods, because their type is already determined.
-Allowing overriding therefore has no implication on our type inference algorithm.
+% 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}
+        \rulename{Adopt}
-%         & $
+        & $
-%         \begin{array}[c]{@{}ll}
+        \begin{array}[c]{@{}ll}
-%         \begin{array}[c]{l}
+        \begin{array}[c]{l}
-%           \wildcardEnv \vdash C \cup \, \set{
+          \wildcardEnv \vdash C \cup \, \set{
-%            \tv{b} \lessdot \tv{a},
+           \tv{b} \lessdot \tv{a},
-% \tv{a} \lessdot \type{N}, \tv{b} \lessdot \type{N'}} \\ 
+\tv{a} \lessdot \type{N}, \tv{b} \lessdot \type{N'}} \\ 
-%           \hline
+          \hline
-%           \vspace*{-0.4cm}\\
+          \vspace*{-0.4cm}\\
-%           \wildcardEnv \vdash C \cup \, \set{
+          \wildcardEnv \vdash C \cup \, \set{
-%  \tv{b} \lessdot \type{N},
+ \tv{b} \lessdot \type{N},
-%            \tv{b} \lessdot \tv{a},
+           \tv{b} \lessdot \tv{a},
-% \tv{a} \lessdot \type{N} , \tv{b} \lessdot \type{N'}
+\tv{a} \lessdot \type{N} , \tv{b} \lessdot \type{N'}
-%            }
+           }
-%         \end{array}
+        \end{array}
-%         \end{array}
+        \end{array}
-%         $
+        $
-%       \\\\
+      \\\\
   \rulename{Adapt}
   & 
   $
@@ -747,28 +747,28 @@ This builds a search tree over multiple possible solutions.
         \end{array}
         $
       \\\\ 
-  %     \rulename{Settle}
+      \rulename{Settle}
-  %     & $
+      & $
-  %     \begin{array}[c]{l}
+      \begin{array}[c]{l}
-  %       \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
+        \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
-  %       \tv{a} \lessdot^* \tv{b}}
+        \tv{a} \lessdot^* \tv{b}}
-  %       \\
+        \\
-  %       \hline
+        \hline
-  %       \wildcardEnv \vdash C \cup \set{  \tv{a} \lessdot^* \tv{b}, \tv{b} \lessdot \type{N}  }
+        \wildcardEnv \vdash C \cup \set{  \tv{a} \lessdot^* \tv{b}, \tv{b} \lessdot \type{N}  }
-  %     \end{array}
+      \end{array}
-  %     $
+      $
-  %   \\\\ 
+    \\\\ 
-  %   \rulename{Raise}
+    \rulename{Raise}
-  %   & $
+    & $
-  %   \begin{array}[c]{l}
+    \begin{array}[c]{l}
-  %     \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
+      \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
-  %     \tv{a} \lessdot \tv{b}}
+      \tv{a} \lessdot \tv{b}}
-  %     \\
+      \\
-  %     \hline
+      \hline
-  %     \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b}  }
+      \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b}  }
-  %   \end{array}
+    \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:}
+% \textbf{Step 4:}
-If there are constraints of the form $(\tv{a} \lessdot \tv{b})$ remaining in the constraint set then
+% 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.
+% apply the \rulename{Sub-Elim} rule and start over with step 1.
-Otherwise continue to step 5.
+% Otherwise continue to step 5.
-\begin{center}
+% \begin{center}
-  \fbox{
+%   \fbox{
-  \begin{tabular}[t]{l@{~}l}
+%   \begin{tabular}[t]{l@{~}l}
-    \rulename{SubElim} 
+%     \rulename{SubElim} 
-    & $\begin{array}[c]{l}
+%     & $\begin{array}[c]{l}
-      \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \tv{b}}\\
+%       \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \tv{b}}\\
-      \hline
+%       \hline
-      [\tv{a}/\tv{b}]\wildcardEnv \vdash [\tv{a}/\tv{b}]C \cup \set{ \tv{b} \doteq \tv{a} }
+%       [\tv{a}/\tv{b}]\wildcardEnv \vdash [\tv{a}/\tv{b}]C \cup \set{ \tv{b} \doteq \tv{a} }
-    \end{array}
+%     \end{array}
-    $
+%     $
-\end{tabular}}
+% \end{tabular}}
-\end{center}
+% \end{center}
 
 \noindent
-\textbf{Step 5:}
+\textbf{Step 4:}
 We apply the rules in figure \ref{fig:cleanup-rules} exhaustively and proceed with step 6.
 
 \begin{figure}
@@ -886,6 +886,14 @@ 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}