Add to introduction

introduction.tex

@@ -17,6 +17,9 @@ In Java this is done implicitly by a process called capture conversion \cite{Jav
 The type system in \cite{WildcardsNeedWitnessProtection} makes this process explicit by using \texttt{let} statements.
 Our type inference algorithm will accept an input program without let statements and add them where necessary.
 
+The input to the type inference algorithm is a Featherweight Java program without let statements (see figure \ref{fig:syntax}).
+Type inference adds \texttt{let} statements in a fashion similar to the Java capture conversion \cite{WildFJ}.
+
 We figured the \texttt{let} statements to be obsolete for our use case.
 Once the type inference algorithm found a correct type solution 
 

martin.bib

@@ -138,6 +138,42 @@ keywords = {subtyping, type inference, principal types}
   bibsource = {DBLP, http://dblp.uni-trier.de}
 }
 
+@inproceedings{WildFJ,
+  author = 	 "Torgersen, Mads and Ernst, Erik and
+                  Hansen, Christian Plesner",
+  title = 	 "Wild {F}{J}",
+  booktitle = 	 "Proceedings of FOOL 12",
+  year = 	 2005,
+  editor = 	 "Wadler, Philip",
+  address = 	 "Long Beach, California, USA",
+  month = 	 Jan,
+  organization = "ACM",
+  publisher = 	 "School of Informatics, University of
+                  Edinburgh",
+  anote = 	 "Electronic publication, at the URL given
+                  below",
+  abstract = 	 "This paper presents a formalization of
+                  wildcards, which is one of the new features of
+                  the Java programming language in version
+                  JDK5.0. Wildcards help alleviating the
+                  impedance mismatch between generics, or
+                  parametric polymorphism, and traditional
+                  object-oriented subtype polymorphism. They do
+                  this by quantifying over parameterized types
+                  with different type arguments. Wildcards take
+                  inspiration from several sources including
+                  use-site variance, and they could be considered
+                  as a way to introduce a syntactically
+                  light-weight kind of existential types into a
+                  main-stream language. This formalization
+                  describes the mechanism, in particular the
+                  wildcard capture process where the existential
+                  nature of wildcards becomes evident.",
+  url = 	 "http://homepages.inf.ed.ac.uk/wadler/fool/",
+  annote =         "wild-fj.pdf"
+}
+
+
 
 @inproceedings{TEP05,
   author = 	 "Torgersen, Mads and Ernst, Erik and
@@ -308,3 +344,11 @@ keywords = {Null, Java Wildcards, Existential Types}
   doi =		{10.4230/LIPIcs.ECOOP.2022.28},
   annote =	{Keywords: type inference, Java, subtyping, generics}
 }
+
+@book{JavaLanguageSpecification,
+  title={The Java language specification},
+  author={Gosling, James},
+  year={2000},
+  publisher={Addison-Wesley Professional}
+}
+

tRules.tex

@@ -1,8 +1,9 @@
 \section{Syntax}
+\begin{figure}
 $
 \begin{array}{lrcl}
 \hline
-\text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{W}} \\
+\text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
 \text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
 \text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
 \text{Type variable contexts} &  \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
@@ -17,6 +18,8 @@ $
 \hline
 \end{array}
 $
+\caption{Input Syntax}\label{fig:syntax}
+\end{figure}
 
 Each class type has a set of wildcard types $\overline{\Delta}$ attached to it.
 The type $\wctype{\overline{\Delta}}{C}{\ol{T}}$ defines a set of wildcards $\overline{\Delta}$,

unify.tex

@@ -10,7 +10,7 @@ which is a supertype of $\exptype{List}{String}$ aswell as $\exptype{List}{Integ
 The algorithm works in a recursive fashion.
 The input constraints are transformed until they reach a irreducible state,
 which the last step of the algorithm eventually transforms into a solution.
-A constraint set is convertable to a correct type solution, if it only contains constraints of the form
+A constraint set is convertable to a correct type solution if it only contains constraints of the form
 $\tv{a} \doteq \type{T}$ (where $\tv{a} \notin \text{tph}(\type{T})$) and $\tv{a} \lessdot \type{T}$.
 We call this \textit{Solved Form}.
 
@@ -21,7 +21,12 @@ A $\bot \lessdot \type{T}$ constraint is always satisfied and can be ignored. It
 For the type placeholder $\tv{a}$ in the constraint $\tv{a} \lessdot \bot$ only the $\bot$ type is a possible substitution,
 which is set by the \rulename{Pit} rule.
 
-Example:
+The \rulename{Reduce} rule represents the S-Exists type rule.
+This rule uses wildcard placeholders ($\ol{\wtv{a}}$) to find a possible substitution for the wildcards on the right side.
+The constraint $\type{N} \lessdot \wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N'}$ is satisfied if
+there is a substitution $[\ol{T}/\ol{X}]\type{N} = \type{N'}$ with $\ol{T}$ inside the bounds $\ol{U}$ and $\ol{L}$.
+
+\textbf{Example:}
 $\exptype{List}{\tv{a}} \lessdot \wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$ 
 The \rulename{Reduce} rule converts this to 
 $\set{\tv{a} \doteq \wtv{x}, \wtv{x} \lessdot \type{Object}, \bot \lessdot \wtv{x} }$.