diff --git a/TIforWildFJ.tex b/TIforWildFJ.tex
index c83103d..958f66a 100644
--- a/TIforWildFJ.tex
+++ b/TIforWildFJ.tex
@@ -112,51 +112,26 @@
\input{tRules}
+\input{typeinference}
+
%\input{tiRules}
\input{constraints}
\input{Unify}
-\section{Limitations}
-
-This example does not work:
-
-\begin{minipage}{0.35\textwidth}
- \begin{verbatim}
-class Example{
- Pair make(List l){...}
- bool compare(Pair p){...}
-
- bool test(List> l){
- return compare(make(l));
- }
-}
-\end{verbatim}
- \end{minipage}%
- \hfill
- \begin{minipage}{0.55\textwidth}
-\begin{constraintset}
- \textbf{Constraints:}\\
- $
- \wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{x}}, \\
- \exptype{Pair}{\wtv{x},\wtv{x}} \lessdot \tv{r}, \\
- \tv{r} \lessdot \exptype{Pair}{\tv{z}, \tv{z}}%,\\
- %\tv{y} \lessdot \tv{m}
- $\\
-\end{constraintset}
- \end{minipage}
-
+\include{relatedwork}
\input{conclusion}
-\include{soundness}
%\include{termination}
-\include{relatedwork}
\bibliography{martin}
\appendix
+
+\include{soundness}
+\include{helpers}
%\include{examples}
%\input{exampleWildcardParameter}
%\input{commonPatternsProof}
diff --git a/conclusion.tex b/conclusion.tex
index 42b4b01..4f68eb5 100644
--- a/conclusion.tex
+++ b/conclusion.tex
@@ -9,7 +9,56 @@
%TODO: how are the challenges solved: Describe this in the last chapter with examples!
\section{Soundness}\label{sec:soundness}
+\begin{theorem}\label{testenv-theorem}
+Type inference produces a correctly typed program.
+\begin{description}
+ \item[If] $\fjtypeinference(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
+ \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \mtypeEnvironment{}'$
+ \item[Then] $\texttt{class}\ \exptype{C}{\ol{X}
+ \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \} \text{ok}$,
+ with $\ol{M} = $
+\end{description}
+\end{theorem}
+
+To prove soundness we have to show two things.
+The vital parts are method calls and field access.
+The generated constraints have to resemble the \TamedFJ{}'s type system.
+
\section{Completeness}\label{sec:completeness}
+We couldn't verify it with an implementation yet, but we assume atleast the same functionality
+as the global type inference algorithm for Featherweight Java without Wildcards \cite{TIforFGJ}.
+
+
+\begin{example} Limitation:
+
+This example does not work:
+
+\begin{minipage}{0.35\textwidth}
+ \begin{verbatim}
+class Example{
+ Pair make(List l){...}
+ bool compare(Pair p){...}
+
+ bool test(List> l){
+ return compare(make(l));
+ }
+}
+\end{verbatim}
+ \end{minipage}%
+ \hfill
+ \begin{minipage}{0.55\textwidth}
+\begin{constraintset}
+ \textbf{Constraints:}\\
+ $
+ \wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{x}}, \\
+ \exptype{Pair}{\wtv{x},\wtv{x}} \lessdot \tv{r}, \\
+ \tv{r} \lessdot \exptype{Pair}{\tv{z}, \tv{z}}%,\\
+ %\tv{y} \lessdot \tv{m}
+ $\\
+\end{constraintset}
+ \end{minipage}
+\end{example}
+
The algorithm can find a solution to every program which the Unify by Plümicke finds
a correct solution aswell.
It will not infer intermediat type like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X},\rwildcard{X}}$.
diff --git a/constraints.tex b/constraints.tex
index 2d05df5..e5e72fd 100644
--- a/constraints.tex
+++ b/constraints.tex
@@ -1,70 +1,3 @@
-\subsection{Capture Constraints}
-%TODO: General Capture Constraint explanation
-
-Capture Constraints are bound to a variable.
-For example a let statement like \lstinline{let x = v in x.get()} will create the capture constraint
-$\tv{x} \lessdotCC_x \exptype{List}{\wtv{a}}$.
-This time we annotated the capture constraint with an $x$ to show its relation to the variable \texttt{x}.
-Let's do the same with the constraints generated by the \texttt{concat} method invocation in listing \ref{lst:faultyConcat},
-creating the constraints \ref{lst:sameConstraints}.
-
-\begin{figure}
- \begin{minipage}[t]{0.49\textwidth}
- \begin{lstlisting}[caption=Faulty Method Call,label=lst:faultyConcat]{tamedfj}
- List> v = ...;
-
- let x = v in
- let y = v in
- concat(x, y) // Error!
- \end{lstlisting}\end{minipage}
- \hfill
- \begin{minipage}[t]{0.49\textwidth}
- \begin{lstlisting}[caption=Annotated constraints,mathescape=true,style=constraints,label=lst:sameConstraints]
- $\tv{x} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{x}$
- $\tv{y} \lessdotCC_\texttt{y} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{y}$
- \end{lstlisting}
- \end{minipage}
-\end{figure}
-
-
-During the \unify{} process it could happen that two syntactically equal capture constraints evolve,
-but they are not the same because they are each linked to a different let introduced variable.
-In this example this happens when we substitute $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\tv{x}$ and $\tv{y}$
-resulting in:
-%For example by substituting $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{x}]$ and $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{y}]$:
-\begin{displaymath}
- \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_x \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_y \exptype{List}{\wtv{a}}
-\end{displaymath}
-Thanks to the original annotations we can still see that those are different constraints.
-After \unify{} uses the \rulename{Capture} rule on those constraints
-it gets obvious that this constraint set is unsolvable:
-\begin{displaymath}
- \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}},
-\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}
-\end{displaymath}
-
-%In this paper we do not annotate capture constraint with their source let statement.
-The rest of this paper will not annotate capture constraints with variable names.
-Instead we consider every capture constraint as distinct to other capture constraints even when syntactically the same,
-because we know that each of them originates from a different let statement.
-\textit{Hint:} An implementation of this algorithm has to consider that seemingly equal capture constraints are actually not the same
-and has to allow doubles in the constraint set.
-
-% %We see the equality relation on Capture constraints is not reflexive.
-% A capture constraint is never equal to another capture constraint even when structurally the same
-% ($\type{T} \lessdotCC \type{S} \neq \type{T} \lessdotCC \type{S}$).
-% This is necessary to solve challenge \ref{challenge:1}.
-% A capture constraint is bound to a specific let statement.
-
-\textit{Note:}
-In the special case \lstinline{let x = v in concat(x,x)} the constraints would look like
-$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}},
-\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
-and we could actually delete one of them without loosing information.
-But this case will never occur in our algorithm, because the let
-statements for our input programs are generated by transformation to ANF (see \ref{sec:anfTransformation}).
-
-
\section{Constraint generation}\label{chapter:constraintGeneration}
% Method names are not unique.
@@ -78,11 +11,6 @@ statements for our input programs are generated by transformation to ANF (see \r
% But it can be easily adapted to Featherweight Java or Java.
% We add T <. a for every return of an expression anyway. If anything returns a Generic like X it is not directly used in a method call like X List add(List l, A v)
-
-List super String> l = ...;
-add(l, "String");
-\end{lstlisting}
-\end{minipage}\hfill
-\begin{minipage}{0.49\textwidth}
-\begin{lstlisting}[style=tamedfj, caption=\TamedFJ{} representation, label=lst:addExampleLet]
- List add(List l, A v)
-List super String> l = ...;
-let v:(*@$\tv{v}$@*) = l
- in add(v, "String");
-\end{lstlisting}
-\end{minipage}\\
-\begin{minipage}{0.49\textwidth}
-\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:addExampleCons]
-(*@$\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}} \lessdot \tv{v}$@*)
-(*@$\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$@*)
-(*@$\type{String} \lessdot \wtv{a}$@*)
-\end{lstlisting}
-\end{minipage}\hfill
-\begin{minipage}{0.49\textwidth}
-\begin{lstlisting}[style=letfj, caption=Type solution, label=lst:addExampleSolution]
- List add(List l, A v)
-List super String> l = ...;
-let l2:(*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l
- in add(l2, "String");
-\end{lstlisting}
-\end{minipage}
-\end{figure}
-
-% \begin{description}
-% \item[input] \tifj{} program
-% \item[output] type solution
-% \item[postcondition] the type solution applied to the input must yield a valid \letfj{} program
-% \end{description}
-
-%Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
-Listings~\ref{lst:addExample}, \ref{lst:addExampleLet}, \ref{lst:addExampleCons}, and
-\ref{lst:addExampleSolution} showcase the global type inference algorithm step by step.
-In the Java code in Listing~\ref{lst:addExample}, the type of variable
-\texttt{l} is an existential type so that it has to undergo a capture conversion
-before being passed to a method call.
-To this end we convert the program to A-Normal form (Listing~\ref{lst:addExampleLet}),
-which introduces a let statement defining a new variable \texttt{v}.
-As the type of \texttt{v} is unknown, the algorithm puts a type
-placeholder $\tv{v}$ for the type of \texttt{v} before generating constraints (see Listing~\ref{lst:addExampleCons}).
-These constraints mirror the typing rules of the \TamedFJ{} calculus (section~\ref{sec:tifj}).
-% During the constraint generation step the type of the variable \texttt{v} is unknown
-% and given the type placeholder $\tv{v}$.
-The call to \texttt{add} generates the \emph{capture constraint} $\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$.
-This constraint ($\lessdotCC$) is a kind of subtype constraint, which additionally
-expresses that the left side of the constraint is subject to a capture conversion.
-Next, the unification algorithm \unify{} (section~\ref{sec:unify}) solves the constraints.
-Initially, no type is assigned to $\tv{v}$.
-% During the course of \unify{} more and more types emerge.
-As soon as a concrete type for $\tv{v}$ is appears during constraint
-solving, \unify{} can conduct a capture conversion if needed.
-%The constraints where this is possible are marked as capture constraints.
-In this example, $\tv{v}$ will be set to
-$\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$
-leaving us with the following constraints:
-
-\begin{displaymath}
-\prftree[r]{Capture}{
-\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}, \, \type{String} \lessdotCC \wtv{a}
-}{
-\wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
-}
-\end{displaymath}
-
-%Capture Constraints $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ allow for a capture conversion,
-%which converts a constraint of the form $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ to $(\exptype{C}{\rwildcard{X}} \lessdot \type{T})$
-The constraint $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$
-allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
-The captured wildcard $\rwildcard{X}$ gets a fresh name \texttt{Y}, which is stored in the wildcard environment of the \unify{} algorithm.
-Substituting \texttt{Y} for $\wtv{a}$ yields the constraints almost
-solved: $\exptype{List}{\rwildcard{Y}} \lessdot
-\exptype{List}{\rwildcard{Y}}$, $\type{String} \lessdot
-\rwildcard{Y}$.
-The first constraint is obviously satisfied and $\type{String} \lessdot \rwildcard{Y}$ is satisfied
-because $\rwildcard{Y}$ has $\type{String}$ as lower bound.
-
-
-A correct Featherweight Java program including all type annotations and an explicit capture conversion via let statement is shown in Listing \ref{lst:addExampleSolution}.
-This program can be deduced from the solution of the \unify{} algorithm presented in Section~\ref{sec:unify}.
-In the body of the let statement the type $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$
-becomes $\exptype{List}{\rwildcard{X}}$ and the capture converted wildcard $\wildcard{X}{\type{Object}}{\type{String}}$ can be used as
-a type parameter of the call \texttt{add(v, "String")}.
-
-% The input to our type inference algorithm is a modified version of the calculus in \cite{WildcardsNeedWitnessProtection} (see chapter \ref{sec:tifj}).
-% First \fjtype{} (see section \ref{chapter:constraintGeneration}) generates constraints
-% and afterwards \unify{} (section \ref{sec:unify}) computes a solution for the given constraint set.
-% Constraints consist out of subtype constraints $(\type{T} \lessdot \type{T})$ and capture constraints $(\type{T} \lessdotCC \type{T})$.
-% \textit{Note:} a type $\type{T}$ can either be a named type, a type placeholder or a wildcard type placeholder.
-% A subtype constraint is satisfied if the left side is a subtype of the right side according to the rules in figure \ref{fig:subtyping}.
-% \textit{Example:} $\exptype{List}{\ntv{a}} \lessdot \exptype{List}{\type{String}}$ is fulfilled by replacing type placeholder $\ntv{a}$ with the type $\type{String}$.
-% Subtype constraints and type placeholders act the same as the ones used in \emph{Type Inference for Featherweight Generic Java} \cite{TIforFGJ}.
-% The novel capture constraints and wildcard placeholders are needed for method invocations involving wildcards.
-
-% The central piece of this type inference algorithm, the \unify{} process, is described with implication rules (chapter \ref{sec:unify}).
-% We try to keep the branching at a minimal amount to improve runtime behavior.
-% Also the transformation steps of the \unify{} algorithm are directly related to the subtyping rules of our calculus.
-% There are no informal parts in our \unify{} algorithm.
-% It solely consist out of transformation rules which are bound to simple checks.
-
-\subsection{Challenges}\label{challenges}
-%TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
-
-% Wildcards are not reflexive.
-% ( on the equals property ), every wildcard has to be capture converted when leaving its scope
-
-% do not substitute free type variables
-
-Global type inference for Featherweight Generic Java without wildcards
-has been considered elsewher \cite{TIforFGJ}.
-Adding wildcards to the calculus created new problems, which have not
-been recognized by existing work on type unification for Java with wildcards~\cite{plue09_1}.
-% what is the problem?
-% Java does invisible capture conversion steps
-Java's wildcard types are represented as existential types that have to be opened before they can be used.
-Opening can either be done implicitly
-(\cite{aModelForJavaWithWildcards}, \cite{javaTIisBroken}) or
-explicitly via a let statement (\cite{WildcardsNeedWitnessProtection}).
-For all variations it is vital to know the argument types with which a method is called.
-In the absence of type annotations,
-we do not know where an existential type will emerge and where a capture conversion is necessary.
-Rather, the type inference algorithm has to figure out the placement
-of existentials.
-We identified three main challenges related to Java wildcards and global type inference.
-\begin{enumerate}
-\item \label{challenge:1}
-One challenge is to design the algorithm in a way that it finds a
-correct solution for programs like the one shown in Listing~\ref{lst:addExample}
-and rejects programs like the one in Listing~\ref{lst:concatError}.
-The first one is a valid Java program,
-because the type \texttt{List super String>} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$
-which is used as the generic method parameter for the call to \texttt{add} as shown in Listing~\ref{lst:addExampleLet}.
-Because we know that the type \texttt{String} is a subtype of the free variable $\rwildcard{X}$,
-it is safe to pass \texttt{"String"} for the first parameter of the function.
-
-The second program shown in Listing~\ref{lst:concatError} is incorrect.
-The method call to \texttt{concat} with two wildcard lists is unsound.
-The element types of the lists may be unrelated, therefore the call to \texttt{concat} cannot succeed.
-The problem gets apparent if we try to write the \texttt{concat}
-method call in the \TamedFJ{} calculus
-(Listing~\ref{lst:concatTamedFJ}):
-\texttt{l1'} and \texttt{l2'} are two different lists inside the body of the let statements, namely
-$\exptype{List}{\rwildcard{X}}$ and $\exptype{List}{\rwildcard{Y}}$.
-For the method call \texttt{concat(x1, x2)} no replacement for the generic \texttt{A}
-exists to satisfy
-$\exptype{List}{\type{A}} <: \exptype{List}{\type{X}},
-\exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$.
-
-% \textbf{Solution:}
-% Capture Conversion during Unify.
-
-\item
-\unify{} transforms a constraint set into a correct type solution by
-gradually assigning types to type placeholders during that process.
-Solved constraints are removed and never considered again.
-In the following example, \unify{} solves the constraint generated by the expression
-\texttt{l.add(l.head())} first, which results in $\ntv{l} \lessdot \exptype{List}{\wtv{a}}$.
-\begin{verbatim}
-anyList() = new List() :? new List()
-
-add(anyList(), anyList().head());
-\end{verbatim}
-The type for \texttt{l} can be an arbitrary list, but it has to be a invariant one.
-Assigning a \texttt{List>} for \texttt{l} is unsound, because the type list hiding behind
-\texttt{List>} could be a different one for the \texttt{add} call than the \texttt{head} method call.
-An additional constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
-is solved by removing the wildcard $\rwildcard{X}$ if possible.
-
-This problem is solved by ANF transformation
-
-\item
-% This problem is solved by assuming everything is a wildcard and lateron erasing excessive wildcards
-% this is solved by having wildcards bound to a type. But this makes it necessary to remove wildcards lateron otherwise Unify would have to backtrack
-The program in Listing~\ref{shuffleExample} exhibits a challenge involving wildcards and subtyping.
-The method call \texttt{shuffle(l)} is incorrect, because \texttt{l} has type
-$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ representing a list of unknown lists.
-However, $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ is a subtype of
-$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ which represents a list of lists, all of the same type $\rwildcard{X}$,
-and can be passed safely to \texttt{shuffle}.
-This behavior can also be explained by looking at the types and their capture converted versions:
-\begin{center}
-\begin{tabular}{l | l | l}
-Java type & \TamedFJ{} representation & Capture Conversion \\
-\hline
-$\exptype{List}{\exptype{List}{\texttt{?}}}$ & $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ & $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ \\
-$\exptype{List2D}{\texttt{?}}$ & $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ & $\exptype{List2D}{\rwildcard{X}}$ \\
-%Supertype of $\exptype{List2D}{\texttt{?}}$ & $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ & $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ \\
-\end{tabular}
-\end{center}
-%The direct supertype of $\exptype{List2D}{\rwildcard{X}}$ is $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
-%One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}.
-%A wildcard in the Java syntax has no name and is bound to its enclosing type:
-%$\exptype{List}{\exptype{List}{\type{?}}}$ equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
-%During type checking \emph{intermediate types}
-%can emerge, which have no equivalent in the Java syntax.
-
-\begin{lstlisting}[style=java,label=shuffleExample,caption=Intermediate Types Example]
-class List extends Object {...}
-class List2D extends List> {...}
-
- void shuffle(List> list) {...}
-
-List> l = ...;
-List2D> l2d = ...;
-
-shuffle(l); // Error
-shuffle(l2d); // Valid
-\end{lstlisting}
-% Java is using local type inference to allow method invocations which are not describable with regular Java types.
-% The \texttt{shuffle} method in this case is invoked with the type $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$
-% which is a subtype of $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
-% After capture conversion \texttt{l2d'} has the type $\exptype{List}{\exptype{List}{\rwildcard{X}}}$
-% and \texttt{shuffle} can be invoked with the type parameter $\rwildcard{X}$:
-% \begin{lstlisting}[style=TamedFJ]
-% let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in shuffle(l2d')
-% \end{lstlisting}
-
-% For the example shown in listing \ref{shuffleExample} the method call \texttt{shuffle(l2d)} creates the constraints:
-% \begin{constraintset}
-% \begin{center}
-% $
-% \begin{array}{l}
-% \wctype{\rwildcard{X}}{List2D}{\rwildcard{X}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
-% \\
-% \hline
-% \wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
-% \\
-% \hline
-% \textit{Capture Conversion:}\
-% \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\wtv{x}}}
-% \\
-% \hline
-% \textit{Solution:} \wtv{x} \doteq \rwildcard{X} \implies \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\rwildcard{X}}}
-% \end{array}
-% $
-% \end{center}
-% \end{constraintset}
-
-Given such a program the type inference algorithm has to allow the call \texttt{shuffle(l2d)} and
-decline the call to \texttt{shuffle(l)}.
-
-% The method call \texttt{shuffle(l)} is invalid however,
-% because \texttt{l} has the type
-% $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
-% There is no solution for the subtype constraint:
-% $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$
-
-\item \label{challenge3} \textbf{Free variables cannot leave their scope}:
-Let's assume we have a variable \texttt{ls} with type $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$
-%When calling the \texttt{id} function with an element of this list we have to apply capture conversion.
-and the following program:
-
-\noindent
-\begin{minipage}{0.62\textwidth}
-\begin{lstlisting}
-let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = ls.get(0) in id(x) : (*@$\ntv{z}$@*)
-\end{lstlisting}\end{minipage}
- \hfill
-\begin{minipage}{0.36\textwidth}
- \begin{lstlisting}[style=constraints]
-(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$@*),
-(*@$\exptype{List}{\wtv{x}} \lessdot \ntv{z},$@*)
- \end{lstlisting}
-\end{minipage}
-% the variable z has to
-
-Take the Java program in listing \ref{lst:mapExample} for example.
-It uses map to apply a polymorphic method \texttt{id} to every element of a list
-$\expr{l} :
-\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$.
-
-How do we get the \unify{} algorithm to determine the correct type for the
-variable \expr{l2}?
-Although we do not specify constraint generation for language constructs like
-lambda expressions used in this example,
-we can imagine that the constraints have to look like in Listing~\ref{lst:mapExampleCons}.
-
-\begin{minipage}{0.45\textwidth}
-\begin{lstlisting}[caption=List Map Example,label=lst:mapExample]
- List id(List l){ ... }
-List> ls;
-l2 = l.map(x -> id(x));
-\end{lstlisting}\end{minipage}
-\hfill
-\begin{minipage}{0.45\textwidth}
-\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:mapExampleCons]
-(*@$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}$@*)
-(*@$\exptype{List}{\wtv{x}} \lessdot \tv{z},$@*)
-(*@$\exptype{List}{\tv{z}} \lessdot \tv{l2}$@*)
-\end{lstlisting}
-\end{minipage}
-
-The constraints
-$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}},
-\exptype{List}{\wtv{x}} \lessdot \tv{z}$
-stem from the body of the lambda expression
-\texttt{id(x)}.
-\textit{For clarification:} This method call would be represented as the following expression in \letfj{}:
-\texttt{let x1 :$\wctype{\rwildcard{A}}{List}{\rwildcard{A}}$ = x in id(x) :$\tv{z}$}
-
-The T-Let rule prevents us from using free variables created by the method call to \expr{id}
-to be used in the return type $\tv{z}$.
-But this restriction has to be communicated to the \unify{} algorithm,
-which does not know about the origin and context of
-the constraints.
-If we naively substitute $\sigma(\tv{z}) = \exptype{List}{\rwildcard{A}}$
-the return type of the \texttt{map} function would be the type
-$\exptype{List}{\exptype{List}{\rwildcard{A}}}$, which would be unsound.
-The type of \expr{l2} is the same as the one of \expr{l}:
-$\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
-
-\textbf{Solution:}
-We solve this issue by distinguishing between wildcard placeholders
-and normal placeholders and introducing them as needed.
-$\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.
-
-\end{enumerate}
-
-%TODO: Move this part. or move the third challenge some underneath.
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "TIforWildFJ"
-%%% End:
diff --git a/soundness.tex b/soundness.tex
index ae68ebf..7a5e547 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -1,118 +1,109 @@
\section{Soundness}
-\begin{lemma}
-A sound TypelessFJ program is also sound under LetFJ type rules.
-\begin{description}
- \item[if:]
-$\Gamma | \Delta \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \ \text{in}\ C \text{with} \ \generics{\ol{Y \triangleleft P}}$
-\end{description}
-\end{lemma}
+% \begin{lemma}
+% A sound TypelessFJ program is also sound under LetFJ type rules.
+% \begin{description}
+% \item[if:]
+% $\Gamma | \Delta \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \ \text{in}\ C \text{with} \ \generics{\ol{Y \triangleleft P}}$
+% \end{description}
+% \end{lemma}
-TODO: Beforehand we have to show that $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
-Here $\Delta$ does not contain every $\overline{\Delta}$ ever created.
-%what prevents a free variable to emerge in \Delta.N example Y^Object |- C <: X^Y.C
-% if the Y is later needed for an equals: same(id(x), x2)
-Free wildcards do not move inwards. We can show that every new type is either well-formed and therefore does not contain any free variables.
-Or it is a generic method call: is it possible to use any free wildcards here?
-let empty
+% TODO: Beforehand we have to show that $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
+% Here $\Delta$ does not contain every $\overline{\Delta}$ ever created.
+% %what prevents a free variable to emerge in \Delta.N example Y^Object |- C <: X^Y.C
+% % if the Y is later needed for an equals: same(id(x), x2)
+% Free wildcards do not move inwards. We can show that every new type is either well-formed and therefore does not contain any free variables.
+% Or it is a generic method call: is it possible to use any free wildcards here?
+% let empty
- Box empty()
-same(Box>, empty())
-let p1 : X.Box = Box> in let
-X.Box <. Box
-Box <. Box
+% Box empty()
+% same(Box>, empty())
+% let p1 : X.Box = Box> in let
+% X.Box <. Box
+% Box <. Box
-boxin(empty()), Box2>
+% boxin(empty()), Box2>
-Where can a problem arise? When we use free wildcards before they are freed.
-But we can always CC them first. Exception two types: X.Pair and Y.Pair
-Here y = Y and x = X but
+% Where can a problem arise? When we use free wildcards before they are freed.
+% But we can always CC them first. Exception two types: X.Pair and Y.Pair
+% Here y = Y and x = X but
- void same(Pair a, Pair b){}
- Pair, X> left() { return null; }
- Pair right() { return null; }
+% void same(Pair a, Pair b){}
+% Pair, X> left() { return null; }
+% Pair right() { return null; }
- Box id(Box extends Box> x)
-here it could be beneficial to use a free wildcard as the parameter X to have it later
-Box> x = ...
-same(id(x), id(x)) <- this will be accepted by TI
+% Box id(Box extends Box> x)
+% here it could be beneficial to use a free wildcard as the parameter X to have it later
+% Box> x = ...
+% same(id(x), id(x)) <- this will be accepted by TI
-let left : X,Y.Pair = left() in
- let right : Pair = right() in
+% let left : X,Y.Pair = left() in
+% let right : Pair = right() in
-Compromise:
-- Generate constraints so that they comply with LetFJ
-- Propose a version which is close to Java
+% Compromise:
+% - Generate constraints so that they comply with LetFJ
+% - Propose a version which is close to Java
-Version for LetFJ:
-Is it still possible to do the capture conversion in form of constraints?
-X.C <. C
-T <. X.C
-how to proof: X.C ok
+% Version for LetFJ:
+% Is it still possible to do the capture conversion in form of constraints?
+% X.C <. C
+% T <. X.C
+% how to proof: X.C ok
-If $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
-then there exists a $|\texttt{e}|$ with $\Delta | \Theta \vdash |\texttt{e}| : \wcNtype{\Delta'}{N}$ in LetFJ.
-This is possible by starting with the parameter types as the base case $\overline{\Delta} = \emptyset$.
+% If $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
+% then there exists a $|\texttt{e}|$ with $\Delta | \Theta \vdash |\texttt{e}| : \wcNtype{\Delta'}{N}$ in LetFJ.
+% This is possible by starting with the parameter types as the base case $\overline{\Delta} = \emptyset$.
-Each type $\wcNtype{\Delta'}{N}$ can only use wildcards already freed.
+% Each type $\wcNtype{\Delta'}{N}$ can only use wildcards already freed.
-\textit{Proof} by structural induction.
-\begin{description}
- \item[$\texttt{e} = \texttt{x}$] $\Delta | \Theta \vdash \texttt{e} : \type{T} \mid \emptyset$
- $\Delta \vdash \type{T} \ \ok$ by \rulename{T-Method}
- and therefore $\Delta | \Theta \vdash \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$.
+% \textit{Proof} by structural induction.
+% \begin{description}
+% \item[$\texttt{e} = \texttt{x}$] $\Delta | \Theta \vdash \texttt{e} : \type{T} \mid \emptyset$
+% $\Delta \vdash \type{T} \ \ok$ by \rulename{T-Method}
+% and therefore $\Delta | \Theta \vdash \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$.
-$|\texttt{x}, \texttt{e}| = \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$
+% $|\texttt{x}, \texttt{e}| = \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$
-\item[$\texttt{e} = \texttt{e}.\texttt{m}(\ol{e})$] there must be atleast one value in $\texttt{e}$ or $\ol{e}$
-\item[$\texttt{e}.f$] given let x : T = e' in x
-let x : T = e' in let xf = x.f in xf
+% \item[$\texttt{e} = \texttt{e}.\texttt{m}(\ol{e})$] there must be atleast one value in $\texttt{e}$ or $\ol{e}$
+% \item[$\texttt{e}.f$] given let x : T = e' in x
+% let x : T = e' in let xf = x.f in xf
-Required:
-$ \Delta | \Theta \vdash e' : \type{T}_1$
-$\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$
-$\Delta, \Delta' | \Theta, x : \type{N} \vdash let xf = x.f in xf : \type{T}_2$
+% Required:
+% $ \Delta | \Theta \vdash e' : \type{T}_1$
+% $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$
+% $\Delta, \Delta' | \Theta, x : \type{N} \vdash let xf = x.f in xf : \type{T}_2$
-\end{description}
+% \end{description}
-\textbf{Proof:} Every program complying with our type rules can be converted to a correct LetFJ program.
-First we convert the program so that every wildcards used in an expression are in the $\Delta$ environment:
-m(p) = e => let xp = p in [xp/p]e
-x1.m(x2) => let xm = x1.m(x2=) in xm
-x.f => let xf = x.f in xf
-Then we have to proof there is never a wildcard used before it is declared.
-Wildcards are introduced by the capture conversions and nothing else.
+% \textbf{Proof:} Every program complying with our type rules can be converted to a correct LetFJ program.
+% First we convert the program so that every wildcards used in an expression are in the $\Delta$ environment:
+% m(p) = e => let xp = p in [xp/p]e
+% x1.m(x2) => let xm = x1.m(x2=) in xm
+% x.f => let xf = x.f in xf
+% Then we have to proof there is never a wildcard used before it is declared.
+% Wildcards are introduced by the capture conversions and nothing else.
-\begin{theorem}\label{testenv-theorem}
-Type inference produces a correctly typed program.
-\begin{description}
- \item[If] $\fjtypeinference(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
- \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \mtypeEnvironment{}'$
- \item[Then] $\texttt{class}\ \exptype{C}{\ol{X}
- \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \} \text{ok}$,
- with $\ol{M} = $
-\end{description}
-\end{theorem}
-
-\begin{lemma}{Well-formedness:}
-TODO:
-\end{lemma}
+% \begin{lemma}{Well-formedness:}
+% TODO:
+% \end{lemma}
\begin{lemma}{Soundness:}
\unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
\begin{description}
- \item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = C$
- and $(\Delta_u, \sigma) = \unify{}(\Delta', C)$ and let $\Delta = \Delta_u \cup \Delta'$
+ \item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = (\Delta', C)$
+ and $(\Delta_u, \sigma) = \unify{}(\Delta', C)$ and let $\Delta= \Delta_u \cup \Delta'$
+ $\Delta, \Delta' \vdash $
% , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } }$
% and $\vdash \ol{L} : \mtypeEnvironment{}$
% and $\Gamma \subseteq \mtypeEnvironment{}$
% \item[given] a $(\Delta, \sigma)$ with $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
% and there exists a $\Delta'$ with $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T'})}$
- \item[then] there is a completion $|\texttt{e}|$ with $\Delta|\Gamma \vdash |\texttt{e}| : \sigma(\tv{a})$
+ %\item[then] there is a completion $|\texttt{e}|$ with $\Delta|\Gamma \vdash |\texttt{e}| : \sigma(\tv{a})$
+ \item[then] $\Delta|\Gamma \vdash \texttt{e} : \sigma(\tv{a})$
\end{description}
\end{lemma}
Regular type placeholders represent type annotations.
@@ -129,6 +120,16 @@ used in let statements and as type parameters for generic method calls.
\textit{Proof:}
By structural induction over the expression $\texttt{e}$.
\begin{description}
+ \item[$\texttt{let}\ \texttt{x} = \texttt{t}_1 \ \texttt{in}\ \expr{t}_2$]
+ $\Delta|\Gamma \vdash \expr{t}_1: \type{T}_1$ by assumption.
+ The body of the let statement will only use the free variables provided by $\Delta$ and $\Delta'$ (see lemma \ref{lemma:wildcardsStayInScope}).
+ \item[$\expr{v}.\texttt{f}$]
+ We are alowwed to use capture conversion for $\expr{v}$ here.
+
+ \item[$\texttt{let}\ \texttt{x} = \texttt{e} \ \texttt{in} \ \texttt{x}.\texttt{f}$]
+ $\Delta|\Gamma \vdash \expr{e}: \type{T}$ by assumption.
+ $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ by lemma \ref{lemma:wildcardWellFormedness}.
+ $\Delta, \Delta' | \Gamma, \expr{x} : \type{T} \vdash \texttt{x}.\texttt{f}$
\item[$\texttt{e}.\texttt{f}$] Let $\sigma(\tv{r}) = \wcNtype{\Delta_c}{N}$,
then $\Delta|\Gamma \vdash \texttt{e} : \wcNtype{\Delta_c}{N}$ by assumption.
$\Delta', \Delta, \Delta_c \vdash \type{N} <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
@@ -157,28 +158,29 @@ By structural induction over the expression $\texttt{e}$.
% This can be given by the constraints generated. We can proof if T ok and S <: T and T <: S' then S ok and S' ok
% If S ok and T <. S , then Unify generates a T ok
- S typeinference:
- T <: [S/Y]U
- We apply the following lemma
- Lemma
- if T ok and T <: S then S ok
- until
- T = [S/Y]U
+ % S typeinference:
+ % T <: [S/Y]U
+ % We apply the following lemma
+ % Lemma
+ % if T ok and T <: S then S ok
- and then we can say by
- Lemma:
- If [S/Y]U ok then S ok (TODO: proof!)
+ % until
+ % T = [S/Y]U
- So we do not have to proof S ok (but T)
+ % and then we can say by
+ % Lemma:
+ % If [S/Y]U ok then S ok (TODO: proof!)
- % T_r <: C (S is in T)
- % Is C ok?
- % if every type environment \Delta supplied to Unify is ok (L <: U), then \sigma(a) = \Delta'.N implies \Delta' conforms to (L <: U)
- % this together with the X <. N constraints proofs T_r ok
+ % So we do not have to proof S ok (but T)
- $\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
- %Easy, because unify only generates substitutions for normal type placeholders which are OK
+ % % T_r <: C (S is in T)
+ % % Is C ok?
+ % % if every type environment \Delta supplied to Unify is ok (L <: U), then \sigma(a) = \Delta'.N implies \Delta' conforms to (L <: U)
+ % % this together with the X <. N constraints proofs T_r ok
+
+ % $\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
+ % %Easy, because unify only generates substitutions for normal type placeholders which are OK
\item[$\texttt{e}.\texttt{m}(\ol{e})$]
Lets have a look at the case where the receiver and parameter types are all named types.
@@ -194,7 +196,8 @@ $\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\
% Solution: Make this a lemma and guarantee that Unify does only create types Delta.T with \Delta subset fv(T)
% This is possible because free variables (except those in \Delta_in) are never used in wildcard environments
-By lemma \ref{lemma:unifyWeakening} we know that
+%By lemma \ref{lemma:unifyWeakening}
+We know that
$\unify{}(\Delta, [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{ \overline{\wcNtype{\Delta}{N}} \lessdotCC \ol{T}, \wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}})$
has a solution.
Also $\overline{\wcNtype{\Delta}{N}} \lessdot \ol{T}$ and $\wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}$ will be converted to
@@ -206,12 +209,13 @@ which shows $\Delta, \Delta', \overline{\Delta} \vdash \overline{N} <: [\ol{S}/\
$\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T}$,
$\Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$
- are guaranteed by the generated constraints and lemma \ref{lemma:unifySoundness} and \ref{lemma:unifyCC}.
+ are guaranteed by the generated constraints and lemma \ref{lemma:unifySoundness}.% and \ref{lemma:unifyCC}.
$\Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}$ due to $\ol{T} = \ol{\wcNtype{\Delta}{N}}$ and S-Refl. $\Delta, \Delta' \vdash \type{T}_r <: \wcNtype{\Delta'}{N}$ accordingly.
$\Delta|\Gamma \vdash \texttt{t}_r : \type{T}_r$ and $\Delta|\Gamma \vdash \ol{t} : \ol{T}_r$ by assumption.
$\Delta, \Delta' \vdash \ol{\wcNtype{\Delta}{N}} \ \ok$ by lemma \ref{lemma:unifyWellFormedness},
therefore $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} \ \ok$, which implies $\Delta, \Delta', \overline{\Delta} \vdash \ol{U} \ \ok$
- by lemma \ref{lemma:wfHereditary} and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok $ by premise of WF-Class.
+ %by lemma \ref{lemma:wfHereditary}
+ and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok $ by premise of WF-Class.
The same goes for $\wcNtype{\Delta'}{N}$.
% \begin{gather}
@@ -270,29 +274,45 @@ by induction over every step of the \unify{} algorithm.
Hint: a type placeholder $\tv{a}$ will never be replaced by a free variable or a type containing free variables.
This fact together with the presumption that every supplied type is well-formed we can easily show that this lemma is true.
-\textit{Proof: (Variant 2)}
-The GenSigma and GenDelta rules check for well-formedness.
+% \textit{Proof: (Variant 2)}
+% The GenSigma and GenDelta rules check for well-formedness.
+
+
+\begin{lemma}\label{lemma:wildcardWellFormedness}
+\unify{} generates well-formed existential types
+\begin{description}
+\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$
+\item[and] $\forall \wcNtype{\Delta''}{N} \in C: \text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
+\item[and] $\sigma(\tv{a}) = \wcNtype{\Delta'}{N}$
+%\item[then] $\Delta \vdash \ol{L <: U}$ and $\Delta \vdash \ol{U <: U'}$ % (with U' being upper limit by class definition)
+\item[then] $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
+\end{description}
+\end{lemma}
+\textit{Proof} is straightforward induction over the transformation rules of \unify{}
+under the assumption that all supplied existential types are satisfying the premise.
+All parts of \unify{} that generate wildcard types always spawn types $\wcNtype{\Delta'}{N}$
+with $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$.
% All types supplied to the Unify algorithm by TYPEs only contain ? extends or ? super wildcards. (X : [bot..T] or X : [T .. Object]).
% Both are well formed!
-\begin{lemma}\label{lemma:wfHereditary}
- Well-formedness is hereditary
- \begin{description}
- \item[If] $\triangle \vdash \exptype{C}{\ol{X}} \ \ok$ and $\triangle \vdash \exptype{C}{\ol{X}} <: \type{S}$
- \item[Then] $\triangle \vdash \type{S} \ \ok$
- \end{description}
-\end{lemma}
-\textit{Proof:}
+% \begin{lemma}\label{lemma:wfHereditary}
+% Well-formedness is hereditary
+% \begin{description}
+% \item[If] $\triangle \vdash \exptype{C}{\ol{X}} \ \ok$ and $\triangle \vdash \exptype{C}{\ol{X}} <: \type{S}$
+% \item[Then] $\triangle \vdash \type{S} \ \ok$
+% \end{description}
+% \end{lemma}
+% \textit{Proof} by induction on subtyping rules in figure \ref{fig:subtyping}
-\begin{lemma}
+% \begin{lemma}
- \begin{description}
- \item[If] $\Delta \vdash \wctype{\Delta'}{C}{\ol{T}} \ \ok$
- \item[Then] $\Delta, \Delta' \vdash \ok{T} \ \ok$
- \end{description}
-\end{lemma}
-\textit{Proof:} by definition of WF-Class
+% \begin{description}
+% \item[If] $\Delta \vdash \wctype{\Delta'}{C}{\ol{T}} \ \ok$
+% \item[Then] $\Delta, \Delta' \vdash \ok{T} \ \ok$
+% \end{description}
+% \end{lemma}
+% \textit{Proof:} by definition of WF-Class
\begin{lemma} \label{lemma:tvsNoFV}
@@ -313,16 +333,30 @@ Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.
% Delta |- N <. T
% \end{lemma}
-\begin{lemma} \label{lemma:unifyWeakening}
-Removing constraints does not render \unify{} impossible as long as the removed constraints do not share wildcard placeholders.
-If there is a solution for a constraint set $C$, then there is also a solution for a subset of that constraint set.
+\begin{lemma}\label{lemma:wildcardsStayInScope}
+Free variables can only hop to another constraint if they share the same wildcard placeholder.
\begin{description}
- \item[If] $(\sigma, \Delta) = \unify{}( C \cup C')$ and $\text{wtv}(C) \cap \text{wtv}(C') = \emptyset$
- \item[then] $ (\sigma', \Delta') = \unify{}( C')$
+ \item[If] $(\sigma, \Delta) = \unify{} (\Delta', C \cup \set{\wcNtype{\Delta'}{N} \lessdot \tv{a}})$
+ \item[and] $\tv{a}$ being a type placeholders used in $C$
+ \item[then] $\text{fv}(\sigma(\tv{a})) \subseteq \Delta, \Delta'$
\end{description}
-
+If $\wcNtype{\Delta'}{N} \lessdot \tv{a}$
\end{lemma}
-\textit{Proof:}
+
+
+
+%TODO: use this to proof soundness. Wildcard placeholders are not shared with other constraints and therefore only the wildcards generated by capture conversion are used in a let statement.
+
+% \begin{lemma} \label{lemma:unifyWeakening}
+% Removing constraints does not render \unify{} impossible as long as the removed constraints do not share wildcard placeholders.
+% If there is a solution for a constraint set $C$, then there is also a solution for a subset of that constraint set.
+% \begin{description}
+% \item[If] $(\sigma, \Delta) = \unify{}( C \cup C')$% and $\text{wtv}(C) \cap \text{wtv}(C') = \emptyset$
+% \item[then] $ (\sigma', \Delta') = \unify{}( C')$
+% \end{description}
+
+% \end{lemma}
+%\textit{Proof:}
%TODO
% does this really work. We have to show that the algorithm never gets stuck as long as there is a solution
% maybe there are substitutions with types containing free variables that make additional solutions possible. Check!
@@ -507,158 +541,158 @@ Same as Subst
\end{description}
-\subsection{Converting to Wild FJ}
-Wildcards are existential types which have to be \textit{unpacked} before they can be used.
-In Java this is done implicitly by a process called capture conversion \cite{JavaLanguageSpecification}.
-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.
+% \subsection{Converting to Wild FJ}
+% Wildcards are existential types which have to be \textit{unpacked} before they can be used.
+% In Java this is done implicitly by a process called capture conversion \cite{JavaLanguageSpecification}.
+% 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.
-%Type inference adds \texttt{let} statements in a fashion similar to the Java capture conversion \cite{WildFJ}.
-%We wrap every parameter of a method invocation in \texttt{let} statement unknowing if a capture conversion is necessary.
+% %Type inference adds \texttt{let} statements in a fashion similar to the Java capture conversion \cite{WildFJ}.
+% %We wrap every parameter of a method invocation in \texttt{let} statement unknowing if a capture conversion is necessary.
-Figure \ref{fig:tletexpr} shows type rules for fields and method calls.
-They have been merged with let statements and simplified.
+% Figure \ref{fig:tletexpr} shows type rules for fields and method calls.
+% They have been merged with let statements and simplified.
-The let statements and the type $\wcNtype{\Delta'}{N}$, which the type inference algorithm can freely choose,
-are necessary for the soundness proof.
+% The let statements and the type $\wcNtype{\Delta'}{N}$, which the type inference algorithm can freely choose,
+% are necessary for the soundness proof.
-%TODO: Show that well-formed implies witnessed!
-We change the type rules to require the well-formedness instead of the witnessed property.
-See figure \ref{fig:well-formedness}.
+% %TODO: Show that well-formed implies witnessed!
+% We change the type rules to require the well-formedness instead of the witnessed property.
+% See figure \ref{fig:well-formedness}.
-Our well-formedness criteria is more restrictive than the ones used for \wildFJ{}.
-\cite{WildcardsNeedWitnessProtection} works with the two different judgements $\ok$ and \texttt{witnessed}.
-With \texttt{witnessed} being the stronger one.
-We rephrased the $\ok$ judgement to include \texttt{witnessed} aswell.
-$\type{T} \ \ok$ in this paper means $\type{T} \ \ok$ and $\type{T} \ \texttt{witnessed}$ in the sense of the \wildFJ{} type rules.
-Java's type system is complex enough as it is. Simplification, when possible, is always appreciated.
-Our $\ok$ rule may not be able to express every corner of the Java type system, but is sufficient to show soundness regarding type inference for a Java core calculus.
+% Our well-formedness criteria is more restrictive than the ones used for \wildFJ{}.
+% \cite{WildcardsNeedWitnessProtection} works with the two different judgements $\ok$ and \texttt{witnessed}.
+% With \texttt{witnessed} being the stronger one.
+% We rephrased the $\ok$ judgement to include \texttt{witnessed} aswell.
+% $\type{T} \ \ok$ in this paper means $\type{T} \ \ok$ and $\type{T} \ \texttt{witnessed}$ in the sense of the \wildFJ{} type rules.
+% Java's type system is complex enough as it is. Simplification, when possible, is always appreciated.
+% Our $\ok$ rule may not be able to express every corner of the Java type system, but is sufficient to show soundness regarding type inference for a Java core calculus.
-The \rulename{WF-Class} rule requires upper and lower bounds to be direct subtypes of each other $\type{L} <: \type{U}$.
-The type rules from \cite{WildcardsNeedWitnessProtection} use a witness type instead.
-Stating that a type is well formed (\texttt{witnessed}) if there exists atleast one simple type $\type{N}$ as a possible subtype:
-$\Delta \vdash \type{N} <: \wctype{\Delta'}{C}{\ol{T}}$.
+% The \rulename{WF-Class} rule requires upper and lower bounds to be direct subtypes of each other $\type{L} <: \type{U}$.
+% The type rules from \cite{WildcardsNeedWitnessProtection} use a witness type instead.
+% Stating that a type is well formed (\texttt{witnessed}) if there exists atleast one simple type $\type{N}$ as a possible subtype:
+% $\Delta \vdash \type{N} <: \wctype{\Delta'}{C}{\ol{T}}$.
-A witness type is easy to find by replacing every wildcard $\ol{W}$ in $\wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$ by its upper bound:
-$\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} <: \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$.
-$\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} \ \texttt{witnessed}$ is given due to $\Delta \vdash \ol{T}, \ol{L}, \ol{U} \ \ok$
-and $\Delta \vdash \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}} \ \ok$.
+% A witness type is easy to find by replacing every wildcard $\ol{W}$ in $\wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$ by its upper bound:
+% $\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} <: \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$.
+% $\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} \ \texttt{witnessed}$ is given due to $\Delta \vdash \ol{T}, \ol{L}, \ol{U} \ \ok$
+% and $\Delta \vdash \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}} \ \ok$.
-\begin{figure}[tp]
-$\begin{array}{l}
- \typerule{T-Var}\\
- \begin{array}{@{}c}
- x : \type{T} \in \Gamma
- \\
- \hline
- \vspace*{-0.3cm}\\
- \Delta | \Gamma \vdash x : \type{T}
- \end{array}
-\end{array}$
-\\[1em]
-$\begin{array}{l}
- \typerule{T-New}\\
- \begin{array}{@{}c}
- \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} \ \ok \quad \quad
- \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
- \Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
- \Delta \vdash \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
- \Delta, \overline{\Delta} \vdash \overline{\type{N}} <: \overline{\type{U}} \quad \quad
- \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
- \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
- \Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok
- \\
- \hline
- \vspace*{-0.3cm}\\
- \Delta | \Gamma \vdash \letstmt{\ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}{\texttt{new} \ \exptype{C}{\ol{T}}(\overline{t})} : \type{T}
- \end{array}
-\end{array}$
-\\[1em]
-$\begin{array}{l}
- \typerule{T-Field}\\
- \begin{array}{@{}c}
- \Delta | \Gamma \vdash \texttt{t} : \type{T} \quad \quad
- \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
- \textit{fields}(\type{N}) = \ol{U\ f} \\
-\Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
-\text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
-\Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
- \\
- \hline
- \vspace*{-0.3cm}\\
- \Delta | \Gamma \vdash \texttt{let}\ x : \wcNtype{\Delta'}{N} = \texttt{t} \ \texttt{in}\ x.\texttt{f}_i : \type{S}
- \end{array}
-\end{array}$
-\\[1em]
-$\begin{array}{l}
- \typerule{T-Call}\\
- \begin{array}{@{}c}
- \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
- \textit{mtype}(\texttt{m}, \type{N}) = \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \quad \quad
- \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
- \\
- \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
- \Delta | \Gamma \vdash \texttt{t}_r : \type{T}_r \quad \quad
- \Delta | \Gamma \vdash \ol{t} : \ol{T} \quad \quad
- \Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
- \Delta \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
- \\
- \Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
- \Delta, \Delta', \Delta'' \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
- \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
- \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
- \\
- \hline
- \vspace*{-0.3cm}\\
- \Delta | \Gamma \vdash \letstmt{x : \wcNtype{\Delta'}{N} = t_r, \ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}
- {\texttt{x}.\generics{\ol{S}}\texttt{m}(\ol{x})} : \type{T}
- \end{array}
-\end{array}$
-\\[1em]
-$\begin{array}{l}
- \typerule{T-Elvis}\\
- \begin{array}{@{}c}
- \Delta | \Gamma \vdash t_1 : \type{T}_1 \quad \quad
- \Delta | \Gamma \vdash t_2 : \type{T}_2 \quad \quad
- \Delta \vdash \type{T}_1 <: \type{T} \quad \quad
- \Delta \vdash \type{T}_2 <: \type{T}
- \\
- \hline
- \vspace*{-0.3cm}\\
- \Delta | \Gamma \vdash t_1 \elvis{} t_2 : \type{T}
- \end{array}
-\end{array}$
-\\[1em]
-$\begin{array}{l}
- \typerule{T-Method}\\
- \begin{array}{@{}c}
- \text{dom}(\Delta)=\ol{X} \quad \quad
- \Delta' = \overline{\type{Y} : \bot .. \type{U}} \quad \quad
- \Delta, \Delta' \vdash \ol{U}, \type{T}, \ol{T}\ \ok \quad \quad
- \texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \set{\ldots} \\
- \Delta, \Delta' | \overline{x:\type{T}}, \texttt{this} : \exptype{C}{\ol{X}} \vdash t:\type{S} \quad \quad
- \Delta, \Delta' \vdash \type{S} <: \type{T} \quad \quad
- \text{override}(\texttt{m}, \type{N}, \generics{\ol{Y \triangleleft U}}\ol{T} \to \type{T})
- \\
- \hline
- \vspace*{-0.3cm}\\
- \Delta \vdash \generics{\ol{Y \triangleleft U}} \type{T} \ \texttt{m}(\overline{\type{T} \ x}) = t \ \ok \ \texttt{in C}
- \end{array}
-\end{array}$
-\\[1em]
-$\begin{array}{l}
- \typerule{T-Class}\\
- \begin{array}{@{}c}
- \Delta = \overline{\type{X} : \bot .. \type{U}} \quad \quad
- \Delta \vdash \ol{U}, \ol{T} \ \ok \quad \quad
- \Delta \vdash \type{N} \ \ok \quad \quad
- \Delta \vdash \ol{M} \ \ok \texttt{ in C}
- \\
- \hline
- \vspace*{-0.3cm}\\
- \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M} } \ \ok
- \end{array}
-\end{array}$
-\caption{T-Call and T-Field} \label{fig:tletexpr}
-\end{figure}
+% \begin{figure}[tp]
+% $\begin{array}{l}
+% \typerule{T-Var}\\
+% \begin{array}{@{}c}
+% x : \type{T} \in \Gamma
+% \\
+% \hline
+% \vspace*{-0.3cm}\\
+% \Delta | \Gamma \vdash x : \type{T}
+% \end{array}
+% \end{array}$
+% \\[1em]
+% $\begin{array}{l}
+% \typerule{T-New}\\
+% \begin{array}{@{}c}
+% \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} \ \ok \quad \quad
+% \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
+% \Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
+% \Delta \vdash \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
+% \Delta, \overline{\Delta} \vdash \overline{\type{N}} <: \overline{\type{U}} \quad \quad
+% \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
+% \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
+% \Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok
+% \\
+% \hline
+% \vspace*{-0.3cm}\\
+% \Delta | \Gamma \vdash \letstmt{\ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}{\texttt{new} \ \exptype{C}{\ol{T}}(\overline{t})} : \type{T}
+% \end{array}
+% \end{array}$
+% \\[1em]
+% $\begin{array}{l}
+% \typerule{T-Field}\\
+% \begin{array}{@{}c}
+% \Delta | \Gamma \vdash \texttt{t} : \type{T} \quad \quad
+% \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
+% \textit{fields}(\type{N}) = \ol{U\ f} \\
+% \Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
+% \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
+% \Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
+% \\
+% \hline
+% \vspace*{-0.3cm}\\
+% \Delta | \Gamma \vdash \texttt{let}\ x : \wcNtype{\Delta'}{N} = \texttt{t} \ \texttt{in}\ x.\texttt{f}_i : \type{S}
+% \end{array}
+% \end{array}$
+% \\[1em]
+% $\begin{array}{l}
+% \typerule{T-Call}\\
+% \begin{array}{@{}c}
+% \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
+% \textit{mtype}(\texttt{m}, \type{N}) = \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \quad \quad
+% \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
+% \\
+% \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
+% \Delta | \Gamma \vdash \texttt{t}_r : \type{T}_r \quad \quad
+% \Delta | \Gamma \vdash \ol{t} : \ol{T} \quad \quad
+% \Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
+% \Delta \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
+% \\
+% \Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
+% \Delta, \Delta', \Delta'' \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
+% \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
+% \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
+% \\
+% \hline
+% \vspace*{-0.3cm}\\
+% \Delta | \Gamma \vdash \letstmt{x : \wcNtype{\Delta'}{N} = t_r, \ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}
+% {\texttt{x}.\generics{\ol{S}}\texttt{m}(\ol{x})} : \type{T}
+% \end{array}
+% \end{array}$
+% \\[1em]
+% $\begin{array}{l}
+% \typerule{T-Elvis}\\
+% \begin{array}{@{}c}
+% \Delta | \Gamma \vdash t_1 : \type{T}_1 \quad \quad
+% \Delta | \Gamma \vdash t_2 : \type{T}_2 \quad \quad
+% \Delta \vdash \type{T}_1 <: \type{T} \quad \quad
+% \Delta \vdash \type{T}_2 <: \type{T}
+% \\
+% \hline
+% \vspace*{-0.3cm}\\
+% \Delta | \Gamma \vdash t_1 \elvis{} t_2 : \type{T}
+% \end{array}
+% \end{array}$
+% \\[1em]
+% $\begin{array}{l}
+% \typerule{T-Method}\\
+% \begin{array}{@{}c}
+% \text{dom}(\Delta)=\ol{X} \quad \quad
+% \Delta' = \overline{\type{Y} : \bot .. \type{U}} \quad \quad
+% \Delta, \Delta' \vdash \ol{U}, \type{T}, \ol{T}\ \ok \quad \quad
+% \texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \set{\ldots} \\
+% \Delta, \Delta' | \overline{x:\type{T}}, \texttt{this} : \exptype{C}{\ol{X}} \vdash t:\type{S} \quad \quad
+% \Delta, \Delta' \vdash \type{S} <: \type{T} \quad \quad
+% \text{override}(\texttt{m}, \type{N}, \generics{\ol{Y \triangleleft U}}\ol{T} \to \type{T})
+% \\
+% \hline
+% \vspace*{-0.3cm}\\
+% \Delta \vdash \generics{\ol{Y \triangleleft U}} \type{T} \ \texttt{m}(\overline{\type{T} \ x}) = t \ \ok \ \texttt{in C}
+% \end{array}
+% \end{array}$
+% \\[1em]
+% $\begin{array}{l}
+% \typerule{T-Class}\\
+% \begin{array}{@{}c}
+% \Delta = \overline{\type{X} : \bot .. \type{U}} \quad \quad
+% \Delta \vdash \ol{U}, \ol{T} \ \ok \quad \quad
+% \Delta \vdash \type{N} \ \ok \quad \quad
+% \Delta \vdash \ol{M} \ \ok \texttt{ in C}
+% \\
+% \hline
+% \vspace*{-0.3cm}\\
+% \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M} } \ \ok
+% \end{array}
+% \end{array}$
+% \caption{T-Call and T-Field} \label{fig:tletexpr}
+% \end{figure}
diff --git a/tRules.tex b/tRules.tex
index 3e2e014..f9c6e18 100644
--- a/tRules.tex
+++ b/tRules.tex
@@ -61,6 +61,9 @@ class List {
as we consider them as data declarations which are given by the programmer.
% They are inferred in for example \cite{plue14_3b}
\item We add the elvis operator ($\elvis{}$) to the syntax to easily showcase applications involving wildcard types.
+This operator is used to emulate Java's \texttt{if-else} expression but without the condition clause.
+Our operator just returns one of the two given statements at random.
+The point is that the return type of the elvis operator has to be a supertype of its two subexpressions.
\item The \texttt{new} expression does not require generic parameters.
\item Every method has an unique name.
The calculus does not include method overriding for simplicity.
diff --git a/typeinference.tex b/typeinference.tex
new file mode 100644
index 0000000..66dcc9f
--- /dev/null
+++ b/typeinference.tex
@@ -0,0 +1,414 @@
+
+\section{Global Type Inference Algorithm}
+\label{sec:glob-type-infer}
+
+This section gives an overview of the global type inference algorithm
+with examples and identifies the challenges that we had to overcome in
+the design of the algorithm.
+
+\begin{figure}[h]
+\begin{minipage}{0.49\textwidth}
+\begin{lstlisting}[style=tfgj, caption=Valid Java program, label=lst:addExample]
+ List add(List l, A v)
+
+List super String> l = ...;
+add(l, "String");
+\end{lstlisting}
+\end{minipage}\hfill
+\begin{minipage}{0.49\textwidth}
+\begin{lstlisting}[style=tamedfj, caption=\TamedFJ{} representation, label=lst:addExampleLet]
+ List add(List l, A v)
+List super String> l = ...;
+let v:(*@$\tv{v}$@*) = l
+ in add(v, "String");
+\end{lstlisting}
+\end{minipage}\\
+\begin{minipage}{0.49\textwidth}
+\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:addExampleCons]
+(*@$\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}} \lessdot \tv{v}$@*)
+(*@$\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$@*)
+(*@$\type{String} \lessdot \wtv{a}$@*)
+\end{lstlisting}
+\end{minipage}\hfill
+\begin{minipage}{0.49\textwidth}
+\begin{lstlisting}[style=tamedfj, caption=Type solution, label=lst:addExampleSolution]
+ List add(List l, A v)
+List super String> l = ...;
+let l2:(*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l
+ in add(l2, "String");
+\end{lstlisting}
+\end{minipage}
+\end{figure}
+
+% \begin{description}
+% \item[input] \tifj{} program
+% \item[output] type solution
+% \item[postcondition] the type solution applied to the input must yield a valid \letfj{} program
+% \end{description}
+
+%Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
+Listings~\ref{lst:addExample}, \ref{lst:addExampleLet}, \ref{lst:addExampleCons}, and
+\ref{lst:addExampleSolution} showcase the global type inference algorithm step by step.
+Note that regular Java code snippets are displayed in a grey box, \TamedFJ{} programs are yellow
+and constraints have a red background.
+%This example is fully typed except for the method call \texttt{add} missing its type parameters.
+In the Java code in Listing~\ref{lst:addExample}, the type of variable
+\texttt{l} is an existential type so that it has to undergo a capture conversion
+before being passed to a method call.
+To this end we convert the program to A-Normal form (Listing~\ref{lst:addExampleLet}),
+which introduces a let statement defining a new variable \texttt{v}.
+The constraint generation step also assigns type placeholders to all variables missing a type annotation.
+%In this case the variable \texttt{v} gets the type placeholder $\tv{v}$ (also shown in listing \ref{lst:addExampleCons})
+%during the constraint generation step.
+In this case the algorithm puts the type
+placeholder $\tv{v}$ for the type of \texttt{v} before generating constraints (see Listing~\ref{lst:addExampleCons}).
+These constraints mirror the typing rules of the \TamedFJ{} calculus (section~\ref{sec:tifj}).
+% During the constraint generation step the type of the variable \texttt{v} is unknown
+% and given the type placeholder $\tv{v}$.
+The call to \texttt{add} generates the \emph{capture constraint} $\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$.
+This constraint ($\lessdotCC$) is a kind of subtype constraint, which additionally
+expresses that the left side of the constraint is subject to a capture conversion.
+Next, the unification algorithm \unify{} (section~\ref{sec:unify}) solves the constraints.
+Havin the constraints in listing \ref{lst:addExampleCons} as an input \unify{} changes the constraint
+$\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}} \lessdot \tv{v}$
+to $\tv{v} \doteq \wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$
+therby finding a type solution for $\tv{v}$.
+Afterwards every occurence of $\tv{v}$ in the constraint set is replaced by $\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$
+leaving us with the following constraints which are now subject to a capture conversion by the \unify{} algorithm:
+% Initially, no type is assigned to $\tv{v}$.
+% % During the course of \unify{} more and more types emerge.
+% As soon as a concrete type for $\tv{v}$ is appears during constraint
+% solving, \unify{} can conduct a capture conversion if needed.
+% %The constraints where this is possible are marked as capture constraints.
+% In this example, $\tv{v}$ will be set to
+% $\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$
+% leaving us with the following constraints:
+
+\begin{displaymath}
+\prftree[r]{Capture}{
+\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}, \, \type{String} \lessdotCC \wtv{a}
+}{
+\wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
+}
+\end{displaymath}
+
+%Capture Constraints $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ allow for a capture conversion,
+%which converts a constraint of the form $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ to $(\exptype{C}{\rwildcard{X}} \lessdot \type{T})$
+The constraint $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$
+allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
+The captured wildcard $\rwildcard{X}$ gets a fresh name \texttt{Y}, which is stored in the wildcard environment of the \unify{} algorithm.
+Substituting \texttt{Y} for $\wtv{a}$ yields the constraints almost
+solved: $\exptype{List}{\rwildcard{Y}} \lessdot
+\exptype{List}{\rwildcard{Y}}$, $\type{String} \lessdot
+\rwildcard{Y}$.
+The first constraint is obviously satisfied and $\type{String} \lessdot \rwildcard{Y}$ is satisfied
+because $\rwildcard{Y}$ has $\type{String}$ as lower bound.
+
+
+A correct Featherweight Java program including all type annotations and an explicit capture conversion via let statement is shown in Listing \ref{lst:addExampleSolution}.
+This program can be deduced from the solution of the \unify{} algorithm.% presented in Section~\ref{sec:unify}.
+In the body of the let statement the type $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$
+becomes $\exptype{List}{\rwildcard{X}}$ and the capture converted wildcard $\wildcard{X}{\type{Object}}{\type{String}}$ can be used as
+a type parameter of the call \texttt{add(v, "String")}.
+
+% The input to our type inference algorithm is a modified version of the calculus in \cite{WildcardsNeedWitnessProtection} (see chapter \ref{sec:tifj}).
+% First \fjtype{} (see section \ref{chapter:constraintGeneration}) generates constraints
+% and afterwards \unify{} (section \ref{sec:unify}) computes a solution for the given constraint set.
+% Constraints consist out of subtype constraints $(\type{T} \lessdot \type{T})$ and capture constraints $(\type{T} \lessdotCC \type{T})$.
+% \textit{Note:} a type $\type{T}$ can either be a named type, a type placeholder or a wildcard type placeholder.
+% A subtype constraint is satisfied if the left side is a subtype of the right side according to the rules in figure \ref{fig:subtyping}.
+% \textit{Example:} $\exptype{List}{\ntv{a}} \lessdot \exptype{List}{\type{String}}$ is fulfilled by replacing type placeholder $\ntv{a}$ with the type $\type{String}$.
+% Subtype constraints and type placeholders act the same as the ones used in \emph{Type Inference for Featherweight Generic Java} \cite{TIforFGJ}.
+% The novel capture constraints and wildcard placeholders are needed for method invocations involving wildcards.
+
+% The central piece of this type inference algorithm, the \unify{} process, is described with implication rules (chapter \ref{sec:unify}).
+% We try to keep the branching at a minimal amount to improve runtime behavior.
+% Also the transformation steps of the \unify{} algorithm are directly related to the subtyping rules of our calculus.
+% There are no informal parts in our \unify{} algorithm.
+% It solely consist out of transformation rules which are bound to simple checks.
+
+\subsection{Notes on Capture Constraints}
+Capture constraints must be stored in a multiset so that it is possible that two syntactically equal constraints remain in the same set.
+The equality relation on Capture constraints is not reflexive.
+
+Capture Constraints are bound to a variable.
+For example a let statement like \lstinline{let x = v in x.get()} will create the capture constraint
+$\tv{x} \lessdotCC_x \exptype{List}{\wtv{a}}$.
+This time we annotated the capture constraint with an $x$ to show its relation to the variable \texttt{x}.
+Let's do the same with the constraints generated by the \texttt{concat} method invocation in listing \ref{lst:faultyConcat},
+creating the constraints \ref{lst:sameConstraints}.
+
+\begin{figure}
+ \begin{minipage}[t]{0.49\textwidth}
+ \begin{lstlisting}[caption=Faulty Method Call,label=lst:faultyConcat,style=TamedFJ]{tamedfj}
+ List> v = ...;
+
+ let x = v in
+ let y = v in
+ concat(x, y) // Error!
+ \end{lstlisting}\end{minipage}
+ \hfill
+ \begin{minipage}[t]{0.49\textwidth}
+ \begin{lstlisting}[caption=Annotated constraints,mathescape=true,style=constraints,label=lst:sameConstraints]
+ $\tv{x} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{x}$
+ $\tv{y} \lessdotCC_\texttt{y} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{y}$
+ \end{lstlisting}
+ \end{minipage}
+\end{figure}
+
+
+During the \unify{} process it could happen that two syntactically equal capture constraints evolve,
+but they are not the same because they are each linked to a different let introduced variable.
+In this example this happens when we substitute $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\tv{x}$ and $\tv{y}$
+resulting in:
+%For example by substituting $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{x}]$ and $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{y}]$:
+\begin{displaymath}
+ \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_x \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_y \exptype{List}{\wtv{a}}
+\end{displaymath}
+Thanks to the original annotations we can still see that those are different constraints.
+After \unify{} uses the \rulename{Capture} rule on those constraints
+it gets obvious that this constraint set is unsolvable:
+\begin{displaymath}
+ \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}},
+\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}
+\end{displaymath}
+
+%In this paper we do not annotate capture constraint with their source let statement.
+This paper will not annotate capture constraints with variable names.
+Instead we consider every capture constraint as distinct to other capture constraints even when syntactically the same,
+because we know that each of them originates from a different let statement.
+\textit{Hint:} An implementation of this algorithm has to consider that seemingly equal capture constraints are actually not the same
+and has to allow doubles in the constraint set.
+
+% %We see the equality relation on Capture constraints is not reflexive.
+% A capture constraint is never equal to another capture constraint even when structurally the same
+% ($\type{T} \lessdotCC \type{S} \neq \type{T} \lessdotCC \type{S}$).
+% This is necessary to solve challenge \ref{challenge:1}.
+% A capture constraint is bound to a specific let statement.
+
+\textit{Note:}
+In the special case \lstinline{let x = v in concat(x,x)} the constraints would look like
+$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}},
+\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
+and we could actually delete one of them without loosing information.
+But this case will never occur in our algorithm, because the let
+statements for our input programs are generated by transformation to ANF (see \ref{sec:anfTransformation}).
+
+
+\subsection{Challenges}\label{challenges}
+%TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
+
+% Wildcards are not reflexive.
+% ( on the equals property ), every wildcard has to be capture converted when leaving its scope
+
+% do not substitute free type variables
+
+Global type inference for Featherweight Generic Java without wildcards
+has been considered elsewher \cite{TIforFGJ}.
+Adding wildcards to the calculus created new problems, which have not
+been recognized by existing work on type unification for Java with wildcards~\cite{plue09_1}.
+% what is the problem?
+% Java does invisible capture conversion steps
+Java's wildcard types are represented as existential types that have to be opened before they can be used.
+Opening can either be done implicitly
+(\cite{aModelForJavaWithWildcards}, \cite{javaTIisBroken}) or
+explicitly via a let statement (\cite{WildcardsNeedWitnessProtection}).
+For all variations it is vital to know the argument types with which a method is called.
+In the absence of type annotations,
+we do not know where an existential type will emerge and where a capture conversion is necessary.
+Rather, the type inference algorithm has to figure out the placement
+of existentials.
+We identified three main challenges related to Java wildcards and global type inference.
+\begin{enumerate}
+\item \label{challenge:1}
+One challenge is to design the algorithm in a way that it finds a
+correct solution for programs like the one shown in Listing~\ref{lst:addExample}
+and rejects programs like the one in Listing~\ref{lst:concatError}.
+The first one is a valid Java program,
+because the type \texttt{List super String>} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$
+which is used as the generic method parameter for the call to \texttt{add} as shown in Listing~\ref{lst:addExampleLet}.
+Because we know that the type \texttt{String} is a subtype of the free variable $\rwildcard{X}$,
+it is safe to pass \texttt{"String"} for the first parameter of the function.
+
+The second program shown in Listing~\ref{lst:concatError} is incorrect.
+The method call to \texttt{concat} with two wildcard lists is unsound.
+The element types of the lists may be unrelated, therefore the call to \texttt{concat} cannot succeed.
+The problem gets apparent if we try to write the \texttt{concat}
+method call in the \TamedFJ{} calculus
+(Listing~\ref{lst:concatTamedFJ}):
+\texttt{l1'} and \texttt{l2'} are two different lists inside the body of the let statements, namely
+$\exptype{List}{\rwildcard{X}}$ and $\exptype{List}{\rwildcard{Y}}$.
+For the method call \texttt{concat(x1, x2)} no replacement for the generic \texttt{A}
+exists to satisfy
+$\exptype{List}{\type{A}} <: \exptype{List}{\type{X}},
+\exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$.
+
+% \textbf{Solution:}
+% Capture Conversion during Unify.
+
+% \item
+% \unify{} transforms a constraint set into a correct type solution by
+% gradually assigning types to type placeholders during that process.
+% Solved constraints are removed and never considered again.
+% In the following example, \unify{} solves the constraint generated by the expression
+% \texttt{l.add(l.head())} first, which results in $\ntv{l} \lessdot \exptype{List}{\wtv{a}}$.
+% \begin{verbatim}
+% anyList() = new List() :? new List()
+
+% add(anyList(), anyList().head());
+% \end{verbatim}
+% The type for \texttt{l} can be an arbitrary list, but it has to be a invariant one.
+% Assigning a \texttt{List>} for \texttt{l} is unsound, because the type list hiding behind
+% \texttt{List>} could be a different one for the \texttt{add} call than the \texttt{head} method call.
+% An additional constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
+% is solved by removing the wildcard $\rwildcard{X}$ if possible.
+
+% This problem is solved by ANF transformation
+
+\item
+% This problem is solved by assuming everything is a wildcard and lateron erasing excessive wildcards
+% this is solved by having wildcards bound to a type. But this makes it necessary to remove wildcards lateron otherwise Unify would have to backtrack
+The program in Listing~\ref{shuffleExample} exhibits a challenge involving wildcards and subtyping.
+The method call \texttt{shuffle(l)} is incorrect, because \texttt{l} has type
+$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ representing a list of unknown lists.
+However, $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ is a subtype of
+$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ which represents a list of lists, all of the same type $\rwildcard{X}$,
+and can be passed safely to \texttt{shuffle}.
+This behavior can also be explained by looking at the types and their capture converted versions:
+\begin{center}
+\begin{tabular}{l | l | l}
+Java type & \TamedFJ{} representation & Capture Conversion \\
+\hline
+$\exptype{List}{\exptype{List}{\texttt{?}}}$ & $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ & $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ \\
+$\exptype{List2D}{\texttt{?}}$ & $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ & $\exptype{List2D}{\rwildcard{X}}$ \\
+%Supertype of $\exptype{List2D}{\texttt{?}}$ & $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ & $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ \\
+\end{tabular}
+\end{center}
+%The direct supertype of $\exptype{List2D}{\rwildcard{X}}$ is $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
+%One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}.
+%A wildcard in the Java syntax has no name and is bound to its enclosing type:
+%$\exptype{List}{\exptype{List}{\type{?}}}$ equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
+%During type checking \emph{intermediate types}
+%can emerge, which have no equivalent in the Java syntax.
+
+\begin{lstlisting}[style=java,label=shuffleExample,caption=Intermediate Types Example]
+class List extends Object {...}
+class List2D extends List> {...}
+
+ void shuffle(List> list) {...}
+
+List> l = ...;
+List2D> l2d = ...;
+
+shuffle(l); // Error
+shuffle(l2d); // Valid
+\end{lstlisting}
+% Java is using local type inference to allow method invocations which are not describable with regular Java types.
+% The \texttt{shuffle} method in this case is invoked with the type $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$
+% which is a subtype of $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
+% After capture conversion \texttt{l2d'} has the type $\exptype{List}{\exptype{List}{\rwildcard{X}}}$
+% and \texttt{shuffle} can be invoked with the type parameter $\rwildcard{X}$:
+% \begin{lstlisting}[style=TamedFJ]
+% let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in shuffle(l2d')
+% \end{lstlisting}
+
+% For the example shown in listing \ref{shuffleExample} the method call \texttt{shuffle(l2d)} creates the constraints:
+% \begin{constraintset}
+% \begin{center}
+% $
+% \begin{array}{l}
+% \wctype{\rwildcard{X}}{List2D}{\rwildcard{X}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
+% \\
+% \hline
+% \wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
+% \\
+% \hline
+% \textit{Capture Conversion:}\
+% \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\wtv{x}}}
+% \\
+% \hline
+% \textit{Solution:} \wtv{x} \doteq \rwildcard{X} \implies \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\rwildcard{X}}}
+% \end{array}
+% $
+% \end{center}
+% \end{constraintset}
+
+Given such a program the type inference algorithm has to allow the call \texttt{shuffle(l2d)} and
+decline the call to \texttt{shuffle(l)}.
+
+% The method call \texttt{shuffle(l)} is invalid however,
+% because \texttt{l} has the type
+% $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
+% There is no solution for the subtype constraint:
+% $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$
+
+\item \label{challenge3} \textbf{Free variables cannot leave their scope}:
+Let's assume we have a variable \texttt{ls} with type $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$
+%When calling the \texttt{id} function with an element of this list we have to apply capture conversion.
+and the following program:
+
+\noindent
+\begin{minipage}{0.62\textwidth}
+\begin{lstlisting}
+let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = ls.get(0) in id(x) : (*@$\ntv{z}$@*)
+\end{lstlisting}\end{minipage}
+ \hfill
+\begin{minipage}{0.36\textwidth}
+ \begin{lstlisting}[style=constraints]
+(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$@*),
+(*@$\exptype{List}{\wtv{x}} \lessdot \ntv{z},$@*)
+ \end{lstlisting}
+\end{minipage}
+% the variable z must not contain free variables (TODO)
+
+Take the Java program in listing \ref{lst:mapExample} for example.
+It uses map to apply a polymorphic method \texttt{id} to every element of a list
+$\expr{l} :
+\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$.
+
+How do we get the \unify{} algorithm to determine the correct type for the
+variable \expr{l2}?
+Although we do not specify constraint generation for language constructs like
+lambda expressions used in this example,
+we can imagine that the constraints have to look like in Listing~\ref{lst:mapExampleCons}.
+
+\begin{minipage}{0.45\textwidth}
+\begin{lstlisting}[caption=List Map Example,label=lst:mapExample]
+ List id(List l){ ... }
+List> ls;
+l2 = l.map(x -> id(x));
+\end{lstlisting}\end{minipage}
+\hfill
+\begin{minipage}{0.45\textwidth}
+\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:mapExampleCons]
+(*@$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}$@*)
+(*@$\exptype{List}{\wtv{x}} \lessdot \tv{z},$@*)
+(*@$\exptype{List}{\tv{z}} \lessdot \tv{l2}$@*)
+\end{lstlisting}
+\end{minipage}
+
+The constraints
+$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}},
+\exptype{List}{\wtv{x}} \lessdot \tv{z}$
+stem from the body of the lambda expression
+\texttt{id(x)}.
+\textit{For clarification:} This method call would be represented as the following expression in \letfj{}:
+\texttt{let x1 :$\wctype{\rwildcard{A}}{List}{\rwildcard{A}}$ = x in id(x) :$\tv{z}$}
+
+The T-Let rule prevents us from using free variables created by the method call to \expr{id}
+to be used in the return type $\tv{z}$.
+But this restriction has to be communicated to the \unify{} algorithm,
+which does not know about the origin and context of
+the constraints.
+If we naively substitute $\sigma(\tv{z}) = \exptype{List}{\rwildcard{A}}$
+the return type of the \texttt{map} function would be the type
+$\exptype{List}{\exptype{List}{\rwildcard{A}}}$, which would be unsound.
+The type of \expr{l2} is the same as the one of \expr{l}:
+$\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
+
+\textbf{Solution:}
+We solve this issue by distinguishing between wildcard placeholders
+and normal placeholders and introducing them as needed.
+$\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.
+
+\end{enumerate}
diff --git a/unify.tex b/unify.tex
index 386f644..b14c9d6 100644
--- a/unify.tex
+++ b/unify.tex
@@ -680,16 +680,13 @@ exists the wildcard $\rwildcard{X}$ has to be removed by setting both lower and
% }
% \end{lstlisting}
-Take the introduction example from listing \ref{lst:intro-example}.
-Constraints for the untyped \texttt{genList} method:
-\begin{constraintset}
-$\begin{array}{l}
-\exptype{List}{\ntv{x}} \lessdot {\ntv{r}}, \type{String} \lessdot {\ntv{x}},
-\exptype{List}{\ntv{y}} \lessdot {\ntv{r}}, \type{Integer} \lessdot {\ntv{y}}
-\end{array}$
-\end{constraintset}
-
+Let's have a look at the constraints generated by the introduction example in listing \ref{lst:intro-example-typeless}:
+\begin{lstlisting}[style=constraints]
+(*@$\exptype{List}{\ntv{x}} \lessdot {\ntv{r}}, \type{String} \lessdot {\ntv{x}}$@*),
+(*@$\exptype{List}{\ntv{y}} \lessdot {\ntv{r}}, \type{Integer} \lessdot {\ntv{y}}$@*)
+\end{lstlisting}
+\unify{} executes the following steps to generate a solved constraint set:
\begin{displaymath}
\prftree[r]{\rulename{Subst}}
{
@@ -786,55 +783,22 @@ The \texttt{concat} method takes two lists of the same generic type.
% Free variables are not allowed to leave their scope.
% This is ensured by type variables which are not allowed to be assigned type holding free variables.
-\subsection{Algorithm}
+% \subsection{Algorithm}
-With \texttt{C} being class names and \texttt{A} being wildcard names.
-The wildcard type $\wildcard{X}{U}{L}$ consist of an upper bound $\type{U}$, a lower bound $\type{L}$
-and a name $\mathtt{X}$.
+% With \texttt{C} being class names and \texttt{A} being wildcard names.
+% The wildcard type $\wildcard{X}{U}{L}$ consist of an upper bound $\type{U}$, a lower bound $\type{L}$
+% and a name $\mathtt{X}$.
-The \rulename{Tame} rule eliminates wildcards. %TODO
-This is done by setting the upper and lower bound to the same value.
+% The \rulename{Tame} rule eliminates wildcards. %TODO
+% This is done by setting the upper and lower bound to the same value.
-The \rulename{match} rule generates fresh wildcards $\overline{\wildcard{A}{\tv{u}}{\tv{l}}}$.
-Their upper and lower bounds are fresh type variables.
+% The \rulename{match} rule generates fresh wildcards $\overline{\wildcard{A}{\tv{u}}{\tv{l}}}$.
+% Their upper and lower bounds are fresh type variables.
-\unify{} is able to remove wildcards by assigning their upper and lower bounds the same type
-(Def: $\type{Object} = \wildcard{A}{Object}{Object}$ by definition \ref{def:equal}).
-This is used by the \rulename{Tame} rule.
+% \unify{} is able to remove wildcards by assigning their upper and lower bounds the same type
+% (Def: $\type{Object} = \wildcard{A}{Object}{Object}$ by definition \ref{def:equal}).
+% This is used by the \rulename{Tame} rule.
-\textbf{Helper functions:}
-\begin{description}
-\item[$\tph{}$] returns all type placeholders inside a given type.
-
-\textit{Example:} $\tph(\wctype{\wildcard{X}{\tv{a}}{\bot}}{Pair}{\wtv{b},\rwildcard{X}}) = \set{\tv{a}, \wtv{b}}$
-
-%\textbf{Wildcard renaming}\\
-\item[Wildcard renaming:]
-The \rulename{Reduce} rule separates wildcards from their environment.
-At this point each wildcard gets a new and unique name.
-To only rename the respective wildcards the reduce rule renames wildcards up to alpha conversion:
-($[\ol{C}/\ol{B}]$ in the \rulename{reduce} rule)
-\begin{align*}
- [\type{A}/\type{B}]\type{B} &= \type{A} \\
- [\type{A}/\type{B}]\type{C} &= \type{C} & \text{if}\ \type{B} \neq \type{C}\\
- [\type{A}/\type{B}]\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} &= \wcNtype{\overline{\wildcard{X}{[\type{A}/\type{B}]\type{U}}{[\type{A}/\type{B}]\type{L}}}}{[\type{A}/\type{B}]N} & \text{if}\ \type{B} \notin \overline{\rwildcard{X}} \\
- [\type{A}/\type{B}]\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} &= \wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} & \text{if}\ \type{B} \in \overline{\rwildcard{X}} \\
-\end{align*}
-\item[Free Variables:]
-The $\text{fv}$ function assumes every wildcard type variable to be a free variable aswell.
-% TODO: describe a function which determines free variables? or do an example?
-\begin{align*}
-\text{fv}(\rwildcard{A}) &= \set{ \rwildcard{A} } \\
-\text{fv}(\tv{a}) &= \emptyset \\
-%\text{fv}(\wtv{a}) &= \set{\wtv{a}} \\
-\text{fv}(\wctype{\Delta}{C}{\ol{T}}) &= \set{\text{fv}(\type{T}) \mid \type{T} \in \ol{T}} / \text{dom}(\Delta) \\
-\end{align*}
-
-\item[Fresh Wildcards:]
-$\text{fresh}\ \overline{\wildcard{A}{\tv{u}}{\tv{l}}}$ generates fresh wildcards.
-The new names $\ol{A}$ are fresh, aswell as the type variables $\ol{\tv{u}}$ and $\ol{\tv{l}}$,
-which are used for the upper and lower bounds.
-\end{description}
% \noindent
% \textbf{Example: (reduce-rule)}
% %The \ruleReduceWC{} resembles the \texttt{S-Exists} subtyping rule.
@@ -1219,7 +1183,7 @@ $\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \cap \Delta_{in}
\label{fig:step2-rules2}
\end{figure}
-Figure \ref{fig:step2-rules2} are special transformations aimed at free variables defined in the input environment $\Delta_{in}$.
+Figure \ref{fig:step2-rules} are special transformations aimed at free variables defined in the input environment $\Delta_{in}$.
Usually \rulename{Upper} takes care of $\rwildcard{X} \lessdot \tv{a}$ constraints,
but if $\rwildcard{X}$ is an element of $\Delta_{in}$ we can also treat it as a regular type.
This leaves us with the two possibilities \rulename{Subst-X} and \rulename{Gen-X} which is the same as \rulename{Upper}.
@@ -1317,11 +1281,9 @@ $
\label{fig:generation-rules}
\end{figure}
-\subsection{Explanations}
-
-%The type reduction is done by the rules in figure \ref{fig:reductionRules}
\subsection{Examples}
+
\textit{Example} of the type reduction rules in figure \ref{fig:reductionRules} with the input
$\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$
The first step is the \rulename{Capture} rule.
@@ -1462,12 +1424,12 @@ is called and $\tv{a}$ gets a type, then this type can be an existential type as
% ( is this complete? X,Y.Pair )
-\subsection{Implementation}
-%List this under implementation details
-Every constraint that is not in solved form and is not able to be processed by any of the rules accounts as a error constraint and renders the constraint set unsolvable
+% \subsection{Implementation}
+% %List this under implementation details
+% Every constraint that is not in solved form and is not able to be processed by any of the rules accounts as a error constraint and renders the constraint set unsolvable
-The new constraint generated by the adopt rule may be eliminated by the match rule.
-The adopt rule still needs to be applied only once per constraint.
+% The new constraint generated by the adopt rule may be eliminated by the match rule.
+% The adopt rule still needs to be applied only once per constraint.
% \textbf{Eliminating Wildcards}