\section{Typeless FJ}

\subsection{Type System}

The type system is similar to the ones used in \emph{Wildcards need Witness Protection}.
Figure \ref{fig:subtyping} shows the subtyping relations.
A Wildcard consists out of a name and a upper and lower bound type.

During the constraint generation step each untyped method has a type of the form
$\exptype{C}{\ol{X}} \to \ol{T} \to \type{T}$.
The first parameter $\exptype{C}{\ol{X}}$ is the receiver type.
When using methods from a already typed class, the receiver type and the method parameters $\ol{T}$
can be used in a polymorphic fashion.
This is prohibited for local methods during the type inference step
to exclude polymorphic recursion.

Our language \TamedFJ{} requires fields to be typed.

%The \rulename{T-Field} and \rulename{T-Let} rules are merged into one:

\begin{figure}[tp]
$\begin{array}{l}
    \typerule{T-Var}\\
    \begin{array}{@{}c}
        \texttt{x} : \type{T} \in \Gamma
        \\
        \hline
    \vspace*{-0.3cm}\\
        \triangle | \Gamma \vdash \texttt{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}\\
        \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}}
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
    \typerule{T-Field}\\
    \begin{array}{@{}c}
        \mathtt{\Pi} | \triangle | \Gamma \vdash \texttt{t} : \wcNtype{\triangle'}{N} \quad \quad
        \textit{fields}(\ntype{N}) = \ol{U\ f}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \triangle | \Gamma \vdash \texttt{t}.\texttt{f}_i : [\ol{T}/\ol{X}]\type{U}_i
    \end{array}
\end{array}$ %TODO: can we use this simplified version?
\\[1em]
$\begin{array}{l}
    \typerule{T-Field}\\
    \begin{array}{@{}c}
        \Delta | \Gamma \vdash \texttt{e} : \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{e}.\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
        \generics{\ol{X \triangleleft U'}} \type{N} \to \ol{U} \to \type{U} \in \Pi(\texttt{m}) \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{e} : \type{T}_r \quad \quad
        \Delta | \Gamma \vdash \ol{e} : \ol{T} \quad \quad
        \Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
        \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
        \\
        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
        \Delta, \Delta', \overline{\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 \texttt{e}.\texttt{m}(\ol{e}) : \type{T}
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
    \typerule{T-Elvis}\\
    \begin{array}{@{}c}
        \triangle | \Gamma \vdash \texttt{t} : \type{T}_1 \quad \quad
        \triangle | \Gamma \vdash \texttt{t}_2 : \type{T}_2 \quad \quad
        \triangle \vdash \type{T}_1 <: \type{T} \quad \quad
        \triangle \vdash \type{T}_2 <: \type{T} \quad \quad
        \\
        \hline
    \vspace*{-0.3cm}\\
        \triangle | \Gamma \vdash \texttt{t}_1 \ \texttt{?:} \ \texttt{t}_2 : \type{T}
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
    \typerule{T-Method}\\
    \begin{array}{@{}c}
        \exptype{C}{\ol{X}} \to \ol{T} \to \type{T} \in \mathtt{\Pi}(\texttt{m})\\
        \text{dom}(\triangle) = \ol{X} \quad \quad
        \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \quad \quad
        \triangle, \triangle' \vdash \ol{U}, \type{T}, \ol{T} \ \ok \quad \quad
        \texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \ \{ \ldots \} \\
        \mathtt{\Pi} | \triangle, \triangle' | \ol{x : T}, \texttt{this} : \exptype{C}{\ol{X}} \vdash \texttt{e} : \type{S} \quad \quad 
        \triangle \vdash \type{S} <: \type{T} \quad \quad 
        \textit{override}(\texttt{m}, \type{N}, \generics{\overline{\type{Y} \triangleleft \type{U}}} \ol{T} \to \type{T})
        \\
        \hline
    \vspace*{-0.3cm}\\
        \triangle \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \text{ in C with } \generics{\ol{Y \triangleleft P}}
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
    \typerule{T-Class}\\
    \begin{array}{@{}c}
        \mathtt{\Pi}' = \mathtt{\Pi} \cup \set{ \texttt{m} \mapsto (\exptype{C}{\ol{X}} \to \ol{T}_\texttt{m} \to \type{T}_\texttt{m}) \mid \texttt{m} \in \ol{M}} \\
        \mathtt{\Pi}'' = \mathtt{\Pi} \cup \set{ \texttt{m} \mapsto
            \generics{\ol{X \triangleleft \type{N}}, \ol{Y \triangleleft P}}(\exptype{C}{\ol{X}} \to \ol{T}_\texttt{m} \to \type{T}_\texttt{m}) \mid \texttt{m} \in \ol{M} } \\
        \triangle = \overline{\type{X} : \bot .. \type{U}} \quad \quad
        \triangle \vdash \ol{U}, \ol{T}, \type{N} \ \ok \quad \quad
        \triangle \vdash \ol{M} \ \ok \text{ in C with} \ \generics{\ol{Y \triangleleft P}}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \}  : \mathtt{\Pi}''
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
    \typerule{T-Program}\\
    \begin{array}{@{}c}
        \emptyset \vdash \texttt{L}_1 : \mathtt{\Pi}_1 \quad \quad 
        \mathtt{\Pi}_1 \vdash \texttt{L}_2 : \mathtt{\Pi}_1 \quad \quad 
        \ldots \quad \quad 
        \mathtt{\Pi}_{n-1} \vdash \texttt{L}_n : \mathtt{\Pi}_n \quad \quad 
        \\
        \hline
    \vspace*{-0.3cm}\\
        \vdash \ol{L} : \mathtt{\Pi}_n
    \end{array}
\end{array}$

\end{figure}

Class names are unique, which makes every method reference $\type{C}.\texttt{m}$ unique.

The $\mathtt{\Pi}$ environment prevents polymorphic recursion.
Methods inside a class are only allowed to call each other in a non polymorphic fashion.

A method assumption ($\exptype{C}{\ol{X}} \to \ol{T} \to \type{T}$) consists out of a receiver type $\exptype{C}{\ol{X}}$,
a parameter list $\ol{T}$ and a return type $\type{T}$.

\begin{figure}
    $\text{fields}(\exptype{Object}{}) = \emptyset$
    \quad \quad
    $\begin{array}{l}
    \typerule{F-Class}\\
    \begin{array}{@{}c}
        \texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \set{\ol{S\ f}; \ol{M}} \quad \quad 
        \text{fields}([\ol{T}/\ol{X}]\type{N}) = \ol{U\ g}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \text{fields}(\exptype{C}{\ol{T}}) = \ol{U\ g}, [\ol{T}/\ol{X}]\ol{S\ f}
    \end{array}
\end{array}$
\end{figure}