\section{\TamedFJ{}}\label{sec:tifj} %LetFJ -> Output language! %TamedFJ -> ANF transformed input langauge %Input language only described here. It is standard Featherweight Java % we use the transformation to proof soundness. this could also be moved to the end. % the constraint generation step assumes every method argument to be encapsulated in a let statement. This is the way Java is doing capture conversion The input to our algorithm is a typeless version of Featherweight Java. The syntax is shown in figure \ref{fig:syntax} and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}. Method parameters and return types are optional. We still require type annotations for fields and generic class parameters. This is a design choice by us, as we consider them as data declarations which are given by the programmer. % They are inferred in for example \cite{plue14_3b} Note the \texttt{new} expression not requiring generic parameters, which are also inferred by our algorithm. The method call naturally has type inferred generic parameters aswell. We add the elvis operator ($\elvis{}$) to the syntax mainly to showcase applications involving wildcard types. The syntax is described in figure \ref{fig:syntax} with optional type annotations highlighted in yellow. It is possible to exclude all optional types. \TamedFJ{} is a subset of the calculus defined by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection}. %The language is designed to showcase type inference involving existential types. The idea is for our type inference algorithm to calculate all missing types and output a fully and correctly typed \TamedFJ{} program, which by default is also a correct Featherweight Java program (see chapter \ref{sec:soundness}). \noindent \textit{Notes:} \begin{itemize} \item The calculus does not include method overriding for simplicity reasons. Type inference for that is described in \cite{TIforFGJ} and can be added to this algorithm accordingly. Our algorithm is designed for extensibility with the final goal of full support for Java. \unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}. Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}. %\textit{Note:} \item The typing rules for expressions shown in figure \ref{fig:expressionTyping} refrain from restricting polymorphic recursion. Type inference for polymorphic recursion is undecidable \cite{wells1999typability} and when proofing completeness like in \cite{TIforFGJ} the calculus needs to be restricted in that regard. Our algorithm is not complete (see discussion in chapter \ref{sec:completeness}) and without the respective proof we can keep the \TamedFJ{} calculus as simple as possible and as close to it's Featherweight Java correspondent \cite{WildcardsNeedWitnessProtection} as possible. Our soundness proof works either way. \end{itemize} %Additional features like overriding methods and method overloading can be added by copying the respective parts from there. %Additional features can be easily added by generating the respective constraints (Plümicke hier zitieren) % The type system in \cite{WildcardsNeedWitnessProtection} allows a method to \textit{override} an existing method declaration in one of its super classes, % but only by a method with the exact same type. % The type system presented here does not allow the \textit{overriding} of methods. % Our type inference algorithm consumes the input classes in succession and could only do a type check instead of type inference % on overriding methods, because their type is already determined. % Allowing overriding therefore has no implication on our type inference algorithm. % The output is a valid Featherweight Java program. % We use the syntax of the version introduced in \cite{WildcardsNeedWitnessProtection} % calling it \letfj{} for that it is a Featherweight Java variant including \texttt{let} statements. \newcommand{\highlight}[1]{\begingroup\fboxsep=0pt\colorbox{yellow}{$\displaystyle #1$}\endgroup} \begin{figure} \par\noindent\rule{\textwidth}{0.4pt} \center $ \begin{array}{lrcl} %\hline \text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\ \text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\ \text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\ \text{Type variable contexts} & \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\ \text{Class declarations} & D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\ \text{Method declarations} & \texttt{M} & ::= & \highlight{\generics{\overline{\type{X} \triangleleft \type{N}}}}\ \highlight{\type{T}}\ \texttt{m}(\overline{\highlight{\type{T}}\ \expr{x}}) \{ \texttt{return} \ \expr{e}; \} \\ \text{Terms} & \expr{e} & ::= & \expr{x} \\ & & \ \ | & \texttt{new} \ \type{C}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\ & & \ \ | & \expr{e}.f\\ & & \ \ | & \expr{e}.\texttt{m}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\ & & \ \ | & \texttt{let}\ \expr{x} \highlight{: \wcNtype{\Delta}{N}} = \expr{e} \ \texttt{in} \ \expr{e}\\ & & \ \ | & \expr{e} \elvis{} \expr{e}\\ \text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\ %\hline \end{array} $ \par\noindent\rule{\textwidth}{0.4pt} \caption{Input Syntax with optional type annotations}\label{fig:syntax} \end{figure} \begin{figure}[tp] \begin{center} $\begin{array}{l} \typerule{S-Refl}\\ \begin{array}{@{}c} \Delta \vdash \type{T} <: \type{T} \end{array} \end{array}$ $\begin{array}{l} \typerule{S-Trans}\\ \begin{array}{@{}c} \Delta \vdash \type{S} <: \type{T}' \quad \quad \Delta \vdash \type{T}' <: \type{T} \\ \hline \vspace*{-0.3cm}\\ \Delta \vdash \type{S} <: \type{T} \end{array} \end{array}$ $\begin{array}{l} \typerule{S-Upper}\\ \begin{array}{@{}c} \wildcard{X}{U}{L} \in \Delta \\ \vspace*{-0.9em}\\ \hline \vspace*{-0.9em}\\ \Delta \vdash \type{X} <: \type{U} \end{array} \end{array}$ $\begin{array}{l} \typerule{S-Lower}\\ \begin{array}{@{}c} \wildcard{X}{U}{L} \in \Delta \\ \vspace*{-0.9em}\\ \hline \vspace*{-0.9em}\\ \Delta \vdash \type{L} <: \type{X} \end{array} \end{array}$ \\[1em] $\begin{array}{l} \typerule{S-Extends}\\ \begin{array}{@{}c} \texttt{class}\ \exptype{C}{\overline{\type{X} \triangleleft \type{U}}} \triangleleft \type{N} \ \{ \ldots \} \\ \ol{X} \cap \text{dom}(\Delta) = \emptyset \\ \hline \vspace*{-0.3cm}\\ \Delta \vdash \wctype{\Delta'}{C}{\ol{T}} <: \wcNtype{\Delta'}{[\ol{T}/\ol{X}]\type{N}} \end{array} \end{array}$ $\begin{array}{l} \typerule{S-Exists}\\ \begin{array}{@{}c} \Delta', \Delta \vdash [\ol{T}/\ol{\type{X}}]\ol{L} <: \ol{T} \quad \quad \Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\ \text{fv}(\ol{T}) \subseteq \text{dom}(\Delta, \Delta') \quad \text{dom}(\Delta') \cap \text{fv}(\wcNtype{\ol{\wildcard{X}{U}{L}}}{N}) = \emptyset \\ \hline \vspace*{-0.3cm}\\ \Delta \vdash \wcNtype{\Delta'}{[\ol{T}/\ol{X}]\type{N}} <: \wcNtype{\ol{\wildcard{X}{U}{L}}}{N} \end{array} \end{array}$ \end{center} \caption{Subtyping}\label{fig:subtyping} \end{figure} \begin{figure}[tp] \begin{center} $\begin{array}{l} \typerule{WF-Bot}\\ \begin{array}{@{}c} \Delta \vdash \bot \ \ok \end{array} \end{array}$ $\begin{array}{l} \typerule{WF-Top}\\ \begin{array}{@{}c} \Delta \vdash \ol{L}, \ol{U} \ \ok \\ \hline \vspace*{-0.3cm}\\ \Delta \vdash \overline{\wildcard{W}{U}{L}}.\texttt{Object} \end{array} \end{array}$ $\begin{array}{l} \typerule{WF-Var}\\ \begin{array}{@{}c} \wildcard{W}{U}{L} \in \Delta \quad \quad \Delta \vdash \ol{L}, \ol{U} \ \ok \\ \hline \vspace*{-0.3cm}\\ \Delta \vdash \wildcard{W}{U}{L} \ \ok \end{array} \end{array}$ \\[1em] $\begin{array}{l} \typerule{WF-Class}\\ \begin{array}{@{}c} \Delta' = \ol{\wildcard{W}{U}{L}} \quad \quad \Delta, \Delta' \vdash \ol{T}, \ol{L}, \ol{U} \ \ok \quad \quad \Delta, \Delta' \vdash \ol{L} <: \ol{U} \\ \Delta, \Delta' \vdash \ol{T} <: [\ol{T}/\ol{X}] \ol{U'} \quad \quad \texttt{class}\ \exptype{C}{\ol{X \triangleleft U'}} \triangleleft \type{N} \ \{ \ldots \} \\ \hline \vspace*{-0.3cm}\\ \Delta \vdash \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}} \ \ok \end{array} \end{array}$ \end{center} \caption{Well-formedness}\label{fig:well-formedness} \end{figure} \begin{figure}[tp] \begin{center} $\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}$ \hfill $\begin{array}{l} \typerule{T-Field}\\ \begin{array}{@{}c} \Delta | \Gamma \vdash \expr{v} : \type{T} \quad \quad \Delta \vdash \type{T} <: \wcNtype{}{N} \quad \quad \textit{fields}(\type{N}) = \ol{U\ f} \\ \hline \vspace*{-0.3cm}\\ \Delta | \Gamma \vdash \expr{v}.\texttt{f}_i : \type{U}_i \end{array} \end{array}$ \\[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-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-New}\\ \begin{array}{@{}c} \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} \ \ok \quad \quad \Delta \vdash \overline{\type{S}} <: \overline{\type{U}} \\ \Delta | \Gamma \vdash \overline{\expr{v} : \type{S}} \quad \quad \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \\ \hline \vspace*{-0.3cm}\\ \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{v}) : \exptype{C}{\ol{T}} \end{array} \end{array}$ \hfill % $\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'}} \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}, \ol{e} : \ol{T} \quad \quad % \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}} % \\ % \Delta \vdash \type{T}, \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-Call}\\ \begin{array}{@{}c} \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad \Delta \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\ \Delta \vdash \ol{S} \ \ok \quad \quad \Delta | \Gamma \vdash \expr{v}, \ol{v} : \ol{T} \quad \quad \Delta \vdash \ol{T} <: [\ol{S}/\ol{X}]\ol{U} \\ \hline \vspace*{-0.3cm}\\ \Delta | \Gamma \vdash \expr{v}.\texttt{m}(\ol{v}) : \type{T} \end{array} \end{array}$ \\[1em] $\begin{array}{l} \typerule{T-Let}\\ \begin{array}{@{}c} \Delta | \Gamma \vdash \expr{t}_1 : \type{T}_1 \quad \quad \Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N} \\ \Delta, \Delta' | \Gamma, \expr{x} : \wcNtype{}{N} \vdash \expr{t}_2 : \type{T}_2 \quad \quad \Delta, \Delta' \vdash \type{T}_2 <: \type{T} \quad \quad \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad \Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok \\ \hline \vspace*{-0.3cm}\\ \Delta | \Gamma \vdash \texttt{let}\ \expr{x} = \expr{t}_1 \ \texttt{in} \ \expr{t}_2 : \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}$ \end{center} \caption{Expression Typing}\label{fig:expressionTyping} \end{figure} \begin{figure} \begin{center} $\begin{array}{l} \typerule{T-Method}\\ \begin{array}{@{}c} \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\ldots} \quad \quad \generics{\ol{Y \triangleleft \type{N}}}(\exptype{C}{\ol{X}},\ol{T}) \to \type{T} \in \mathtt{\Pi}(\texttt{m}) \quad \quad \triangle' = \overline{\type{Y} : \bot .. \type{P}} \\ \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \quad \quad \text{dom}(\triangle) = \ol{X} \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} \\ \hline \vspace*{-0.3cm}\\ \mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) \set{ \texttt{return}\ \texttt{e}; } \ \ok \ \text{in C} \end{array} \end{array}$ \\[1em] $\begin{array}{l} \typerule{T-Class}\\ \begin{array}{@{}c} %\forall \texttt{m} \in \ol{M} : \mathtt{\Pi}(\texttt{m}) = \generics{\ol{X \triangleleft \type{N}}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \\ \triangle = \overline{\type{X} : \bot .. \type{U}} \quad \quad \triangle \vdash \ol{U}, \ol{T}, \type{N} \ \ok \quad \quad \mathtt{\Pi}' | \triangle \vdash \ol{M} \ \ok \text{ in C} \\ \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] \hfill $\begin{array}{l} \typerule{T-Program}\\ \begin{array}{@{}c} \mathtt{\Pi} = \overline{\texttt{m} : \generics{\ol{X \triangleleft \type{N}}}\ol{T} \to \type{T}} \\ \hline \vspace*{-0.3cm}\\ \overline{D : \mathtt{\Pi}} \end{array} \end{array}$ \end{center} \caption{Class and Method Typing rules}\label{fig:typing} \end{figure} \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}$ \caption{Field access} \end{figure}