examples.tex

Our unify algorithm processes one or two constraints at a time.
Lets look at some examples of different compositions of constraints
and how our unify algorithm will transform them.

\begin{enumerate}
\item $Eq = \set{a \lessdot \exptype{C}{\ol{X}}, a \lessdot b}$ \\
If this is an end configuration, the constraint set is solved.
We can now put any type for $b$, which is a sub or supertype of $\exptype{C}{\ol{X}}$.
The only exception is, when $b \in \ol{X}$.
In this case $\sigma(b) = \tt{Object}$ is always a correct unifier.
So there is atleast one possible solution.

\item $Eq = \set{a \lessdot \exptype{C}{\ol{X}}, a \lessdot b, b \lessdot c}$
It's the same as the example before.
Replacing $b$ and $c$ with \texttt{Object} is also a correct solution. 

\item $Eq = \set{a \lessdot \exptype{C}{\ol{X}}, a \lessdot b, b \lessdot \exptype{D}{\ol{Y}}}$
Here the adopt rule transforms this to:
$\set{a \lessdot \exptype{C}{\ol{X}}, a \lessdot b, b \lessdot \exptype{D}{\ol{Y}}, a \lessdot \exptype{D}{\ol{Y}}}$
and here it depends if $\exptype{C}{\ol{A}} <: \exptype{D}{\ol{B}}$ or $\exptype{D}{\ol{A}} <: \exptype{C}{\ol{B}}$.
Either the $a \lessdot \exptype{C}{\ol{X}}$ or $b \lessdot \exptype{D}{\ol{Y}}$ constraint
gets removed by the match rule.
This leads to $\set{a \lessdot \exptype{C}{\ol{X}}, a \lessdot b, b \lessdot \exptype{D}{\ol{Y}}}$.
If $\texttt{C} = \texttt{D}$ and $\ol{X} = \ol{Y}$ we have the following situation:
$\set{a \lessdot \exptype{C}{\ol{X}}, a \lessdot b, b \lessdot \exptype{D}{\ol{Y}}}$.
Otherwise the match rule gets applied again.

\item $Eq = \set{a \lessdot \exptype{C}{\ol{X}}, a \lessdot b, b \lessdot \exptype{C}{\ol{X}}}$
TODO

\end{enumerate}

\textbf{match-rule:}\\
The match-rule takes two constraints of the form $a \lessdot \exptype{C}{\ol{X}}, a \lessdot \exptype{D}{\ol{Y}}$
and checks which one of the two types \texttt{C} and \texttt{D} is a subtype of the other.
We only leave the constraint, which is more restrictive.
If \texttt{C} and \texttt{D} do not have a subtype relation, the match-rule won't apply.
This will lead to the constraint set never reaching solved form.
We cannot remove the $a \lessdot \exptype{D}{\ol{Y}}$ constraint without matching the
$\ol{Y}$ and $\ol{X}$.
We do this by generating the constraint $\exptype{C}{\ol{X}} \lessdot \exptype{D}{\ol{Y}}$.
This constraint will then be processed by the adapt and the reduce rule.

Example:
$Eq = \set{a \lessdot \exptype{C}{b,\tt{String}}, a \lessdot \exptype{D}{b,b}}$
with $\exptype{C}{A,B} <: \exptype{D}{B,B}$.
\begin{displaymath}
\prftree[r]{
    reduce2
        }{
    \prftree[r]{
        adapt
            }{
    \prftree[r]{
        match
            }{
    \set{a \lessdot \exptype{C}{b,\tt{String}}, a \lessdot \exptype{D}{b,b}}
    }{
    a \lessdot \exptype{C}{b,\tt{String}}, \exptype{C}{b,\tt{String}} \lessdot \exptype{D}{b,b}
    }
    }{
         a \lessdot \exptype{C}{b,\tt{String}}, \exptype{D}{\tt{String},\tt{String}} \doteq \exptype{D}{b,b}
    }}
    {
       a \lessdot \exptype{C}{b,\tt{String}}, b \doteq \tt{String}, b \doteq \tt{String}
        }
\end{displaymath}

\textbf{adopt-rule:}\\
\begin{displaymath}
    \prftree[r]{
        ?
    }{
\prftree[r]{
    reduce2
        }{
    \prftree[r]{
        match
            }{
    \prftree[r]{
        adopt
            }{
    \set{a \lessdot \exptype{C}{\tt{String}}, b \lessdot a, b \lessdot \exptype{C}{c}}
    }{
        \set{a \lessdot \exptype{C}{\tt{String}}, b \lessdot a, b \lessdot \exptype{C}{\tt{String}}, b \lessdot \exptype{C}{c}}
    }
    }{
        \set{a \lessdot \exptype{C}{\tt{String}}, b \lessdot a, b \lessdot \exptype{C}{\tt{String}}, \exptype{C}{\tt{String}} \lessdot \exptype{C}{c}}
    }}
    {
        \set{a \lessdot \exptype{C}{\tt{String}}, b \lessdot a, b \lessdot \exptype{C}{\tt{String}}, \tt{String} \doteq c}
    }}{
    ? \text{(solved form reached?)}
        }
\end{displaymath}


\textbf{circle:}\\
\begin{displaymath}
    \prftree[r]{
        \ldots
    }{
\prftree[r]{
    match
        }{
    \prftree[r]{
        adopt
            }{
    \prftree[r]{
        adopt
            }{
\set{a \lessdot \exptype{C}{x}, b \lessdot a, a \lessdot b}
}{
    \set{a \lessdot \exptype{C}{x}, b \lessdot a, b \lessdot \exptype{C}{x}, a \lessdot b}
}
}{
    \set{a \lessdot \exptype{C}{x}, b \lessdot a, b \lessdot \exptype{C}{x}, a \lessdot b, a \lessdot \exptype{C}{x}}
}}
{
    \set{a \lessdot \exptype{C}{x}, b \lessdot a, b \lessdot \exptype{C}{x}, \exptype{C}{x} \lessdot \exptype{C}{x}, a \lessdot b, \exptype{C}{x} \lessdot \exptype{C}{x}}
}}{
 \ldots
        }
\end{displaymath}

\textbf{longer circle:}\\
\begin{displaymath}
    \prftree[r]{
        adopt, adopt
}{
\set{a \lessdot \exptype{C}{x}, b \lessdot a, c \lessdot b, c \lessdot a}
}{
\set{a \lessdot \exptype{C}{x}, b \lessdot a,
c \lessdot b, c \lessdot a, b \lessdot \exptype{C}{x}, c \lessdot \exptype{C}{x}}
}
\end{displaymath}

\textbf{longer circle 2:}\\
\begin{displaymath}
    \prftree[r]{
        match, reduce2
    }{
\prftree[r]{
    adopt
        }{
    \prftree[r]{
        match, reduce2
            }{
    \prftree[r]{
        adopt, adopt
}{
\set{a \lessdot \exptype{C}{x}, b \lessdot a, c \lessdot b, c \lessdot a, b \lessdot \exptype{C}{String}}
}{
\set{a \lessdot \exptype{C}{x}, b \lessdot a,
c \lessdot b, c \lessdot a, b \lessdot \exptype{C}{x}, b \lessdot \exptype{C}{\tt{String}}, c \lessdot \exptype{C}{\tt{String}}}
}
}{
    \set{a \lessdot \exptype{C}{x}, b \lessdot a,
    c \lessdot b, c \lessdot a, b \lessdot \exptype{C}{x}, c \lessdot \exptype{C}{\tt{String}}, x \doteq \tt{String}}    
}}
{
    \set{a \lessdot \exptype{C}{x}, b \lessdot a,
    c \lessdot b, c \lessdot a, b \lessdot \exptype{C}{x}, c \lessdot \exptype{C}{\tt{String}}, c \lessdot \exptype{C}{x}, x \doteq \tt{String}}   
}}{
    \set{a \lessdot \exptype{C}{x}, b \lessdot a,
    c \lessdot b, c \lessdot a, b \lessdot \exptype{C}{x}, c \lessdot \exptype{C}{x}, x \doteq \tt{String}}   
        }
\end{displaymath}


\textbf{Example 1}\\
The algorithm is able to infer the types of multiple classes under specific circumstances.
The individual classes must be given to him after one another.
This comes with the restriction, that the first class is correct on its own and does not use any other class.
The second class that gets compiled can use the first class and so on.

The following example shows how the algorithm infers and compiles multiple classes iteratively.
The class \texttt{Class1} is infered first.
It has only one method which is the identity function,
to which our algorithm allocates the type $\exptype{}{A}\ A \to A$.
The next class \texttt{Class2} is now able to use this generic method.
The blue colored types are inferred in the next iteration of our algorithm.

\begin{table}
\caption{Two classes as input. \texttt{Class1} is infered first (shown in {\color{red}red})}
\begin{tabular}{cc}
\begin{lstlisting}
class Class1 extends Object {
  Class1() { super(); }
  id(a){
    return a;
  }
}
class Class2 extends Class1 {
  Class2() { 
    super(); 
  }
  example(){
    return new Class1().id(this);
  }
}
\end{lstlisting}
&
\begin{lstlisting}
class Class1 extends Object {
  Class1() { super(); }
  (*@ \textcolor{red}{<A> A} @*) id((*@ \textcolor{red}{A} @*) a){
    return a;
  }
}
class Class2 extends Class1 {
  Class2() { 
    super(); 
  }
  (*@ \textcolor{blue}{Class1}@*) example(){
    return this.(*@\textcolor{blue}{<Class1>}@*)id(this);
  }
}
\end{lstlisting}
\end{tabular}
\end{table}

\textbf{Example 2}\\
When compiling a class like the following
we have to first split this class into two classes.
The \texttt{TwoMethods} class can be first split into the classes \texttt{Class1}
and \texttt{Class2} and after being processed by the type inference algorithm it can be assembled back together again.
This leads to a principal typing.
When using our type inference algorithm on the class \texttt{TwoMethods} alone
it would give the method \texttt{id} the type $\texttt{TwoMethods} \to \texttt{TwoMethods}$,
which is not the desired principal type.
\begin{lstlisting}
class TwoMethods extends Object {
  TwoMethods() { super(); }
  id(a){
    return a;
  }
  example(){
    return this.id(this);
  }
}
\end{lstlisting}

\textbf{Example 3}\\
%TODO: Ein Beispiel für die Unify-adapt Regel
FGJ allows subtype relations like the following:
\begin{lstlisting}
class Map<A,B> extends Object {
  Map<A,B>() { super(); }
}
class SpecialMap<A,B,C> extends Map<A,C> {
  SpecialMap<A,B,C>() { super(); }
}
\end{lstlisting}

If for example we have a method \texttt{method} like this:
\begin{lstlisting}
<X> void method(Map<X, String> map){
  ...
}
\end{lstlisting}
and call it:
\begin{lstlisting}
method(new SpecialMap<Object,Integer,String>());
\end{lstlisting}

Then the constraint $\exptype{SpecialMap}{Object,Integer,String} \lessdot \exptype{Map}{X,String}$
is generated by the \textbf{FJTYPE} algorithm.
This constraint will be processed by the \texttt{adapt} rule of the \unify{} algorithm.
Remember that $(\exptype{SpecialMap}{A,B,C} \olsub \exptype{Map}{A,C}) \in S_\leq$.
\begin{align*}
  Eq& \cup \exptype{SpecialMap}{Object,Integer,String} \lessdot \exptype{Map}{X,String} \\
  \cline{1-2} 
  Eq& \cup \set{\exptype{Map}{[ Object / A ][ Integer / B ][ String / C ](A,C)}
  \doteq \exptype{Map}{X,Integer}} \\
  \cline{1-2} 
  Eq& \cup \set{\exptype{Map}{Object,String}
  \doteq \exptype{C}{X, Integer}}
%Eq \cup \set{\theta_1 \doteq \lambda'_1 \ldo \theta_n \doteq \lambda'_n}
\end{align*}

After the \texttt{adapt} rule got applied we can already see that a correct unificator for this constraint would be
$\sigma(X) = \texttt{Object}$.

\textbf{Example 4 (Multiple type solutions):}
\begin{lstlisting}
class List<A> extends Object {
  List<A> add(A p){...}
}
class C1 extends Object {
  m1(ls){
    return ls.add(this);
  }
}
class C2 extends Object {
  m2(){
    return new C1().m1(new List<C1>());
  }
}
\end{lstlisting}
When compiling the class \texttt{C1} there are two possible method typings for \texttt{m1}.
One of it would 
\begin{lstlisting}
class List<A> extends Object {
  List<A> add(A p){...}
}
class C1 extends Object {
  List<Object> m1((*@\color{red}List<Object>@*) ls){
    return ls.add(this);
  }
}
class C2 extends Object {
  m2(){
    return new C1().m1((*@\color{red}new List<C1>()@*));
  }
}
\end{lstlisting}
\texttt{List<Object>} would be a correct type for the parameter \texttt{ls}.
The call \texttt{ls.add(this)} still works because the type of \texttt{this} is a subtype of \texttt{Object}.
But then the method \texttt{m2} will be incorrect when compiling the class \texttt{C2}.
Our algorithm has to backtrack to the class \texttt{C1} and use the other possible typing.
The following would be the correct solution with \texttt{List<C1>} as the type for \texttt{ls}.
\begin{lstlisting}
class List<A> extends Object {
  List<A> add(A p){...}
}
class C1 extends Object {
  List<C1> m1((*@\color{green}List<C1>@*) ls){
    return ls.add(this);
  }
}
class C2 extends Object {
  List<C1> m2(){
    return new C1().m1((*@\color{green}new List<C1>()@*));
  }
}
\end{lstlisting}

\textbf{Example 5} (for global type inference)
\begin{lstlisting}

\end{lstlisting}