diff --git a/TIforWildFJ.tex b/TIforWildFJ.tex index 9f0bbad..013974d 100644 --- a/TIforWildFJ.tex +++ b/TIforWildFJ.tex @@ -100,9 +100,33 @@ TODO: Abstract \input{introduction} +%We could do a translation from Java to \wildFJ explaining implicit capture conversion + +\section{Soundness of Typing} + + +We show soundness with the type rules statet in \cite{WildcardsNeedWitnessProtection}. +A correct \FGJGT{} program can be converted to a correct \wildFJ{} program. + +\begin{figure} +$\begin{array}{rcl} + | \texttt{x} | + & = & \texttt{x} \\ + | \texttt{let} \ \texttt{x} : \type{T} = \texttt{e},\, \ol{x} : \ol{T} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x}) | + & = & |\texttt{e}|.\texttt{m}(\ol{|e|}) \\ + | \texttt{let} \ \texttt{x} : \type{T} = \texttt{e}\ \texttt{in}\ \texttt{x}.\texttt{f} | + & = & |\texttt{e}|.\texttt{f} \\ + | \texttt{e} \elvis{} \texttt{e} | + & = & |\texttt{e}| \elvis{} |\texttt{e}| \\ +\end{array}$ +\caption{Erasure} \label{fig:erasure} +\end{figure} + + + %\input{tRules} -%\input{tiRules} +\input{tiRules} \input{constraints} diff --git a/constraints.tex b/constraints.tex index 39d31d9..c1dccd3 100644 --- a/constraints.tex +++ b/constraints.tex @@ -113,7 +113,7 @@ Wildcard types are not used during the constraint generation step and have no in \orCons\set{ \set{ & \tv{r} \lessdot \exptype{C}{\ol{\wtv{a}}} , - [\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} , \ol{\tv{a}} \lessdot [\overline{\tv{a}}/\ol{X}]\ol{N} + [\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} , \ol{\wtv{a}} \lessdot [\overline{\wtv{a}}/\ol{X}]\ol{N} } \\ & \quad \mid \mv{T}\ \mv{f} \in \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots} , \, \overline{\wtv{a}} \text{ fresh} @@ -178,7 +178,7 @@ The ones to already typed methods and calls to untyped methods. \overline{\wtv{b}} \lessdot \ol{N'} \} \end{array}\\ & \ |\ - (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T}) \in + (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N'}}\overline{\type{T}} \to \type{T}) \in {\mtypeEnvironment} , \, \overline{\wtv{a}} \text{ fresh}, \, \overline{\wtv{b}} \text{ fresh} } \end{array}\\ diff --git a/prolog.tex b/prolog.tex index 0d26766..a4759ab 100755 --- a/prolog.tex +++ b/prolog.tex @@ -26,6 +26,7 @@ \newcommand{\olsub}{\textrm{$<:$}\ } \newcommand{\sub}\olsub%{\mbox{$<$}} +\newcommand{\ok}{\text{ok}} \newcommand{\set}[1]{\{ #1 \} } diff --git a/soundness.tex b/soundness.tex index db731b3..935ae20 100644 --- a/soundness.tex +++ b/soundness.tex @@ -1,5 +1,7 @@ \section{Soundness} +\newcommand{\CC}{\text{CC}} + \begin{theorem}\label{testenv-theorem} Type inference produces a correctly typed program. \begin{description} @@ -11,6 +13,31 @@ Type inference produces a correctly typed program. \end{description} \end{theorem} +\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$ + , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdot \type{T'} } }$ + and $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$ + and $\vdash \ol{L} : \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] $\Delta \vdash \texttt{e} : \sigma(\tv{a})$ + \end{description} +\end{lemma} +\textit{Proof:} +By structural induction over the expression $\texttt{e}$. +\begin{description} + \item[$\texttt{e}.\texttt{f}$] Given $\Delta \vdash \texttt{e} : \sigma(\tv{r})$ by assumption. + $\Delta', \Delta|\Gamma \vdash \CC{}(\sigma(\tv{r})) <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise. + Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$. + %TODO: Proof this: The reason is that r is not flagged with a ? and we only add free variables here, that are in \Delta + Then $\text{fv}(\wcNtype{\Delta'}{N}) \subseteq \text{dom}(\Delta)$ + and therefore $\text{fv}(\type{N}) \subseteq \text{dom}(\Delta, \Delta')$. + This implies $\Delta, \Delta' \vdash \type{U}_i <: \type{S}$, because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$. + \item[$\texttt{e}.\texttt{m}(\ol{e})$] Given +\end{description} + % %This lemma can be used to proof Normalize rule! % \begin{lemma}\label{lemma:wildcardReplacement} % Wildcards with the same upper and lower bound can be replaced by their bounds without breaking subtype relations. @@ -45,19 +72,29 @@ Type inference produces a correctly typed program. \begin{lemma} The \unify{} algorithm only produces correct output for constraints not containing free variables. - \begin{description} \item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdot \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$ \item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$ \item[Then] there exists a $\Delta'$ with: $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$ -and $\Delta, \Delta' \vdash \overline{\text{CC}(\sigma(\type{S'})) <: \sigma(\type{T'})}$ +and $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T'})}$ % and $\sigma(\type{T'}) = \sigma(\type{T'})$. -The function $\text{CC}$ is given as $\text{CC}(\wcNtype{\Delta}{N}) = \type{N}$ +The function $\CC{}$ is given as $\CC{}(\wcNtype{\Delta}{N}) = \type{N}$ \end{description} \end{lemma} +% \begin{lemma} % a lemma where we distinguis between free variable on the left or the right side of a constraint (not needed anymore) +% The \unify{} algorithm only produces correct output for constraints not containing free variables. +% \begin{description} +% \item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \wcNtype{\Delta'}{N} \lessdot \type{T'} } \cup \overline{ \type{S'} \lessdot \wcNtype{\Delta'}{N'} })$ +% \item[and] $fv(\overline{ \type{S} }) = \emptyset, fv(\overline{ \type{T} }) = \emptyset, fv(\overline{ \type{T'} }) = \emptyset, fv(\overline{ \type{S'} }) = \emptyset$ +% \item[Then] $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$ +% and $\Delta, \Delta' \vdash \overline{\sigma(\type{N}) <: \sigma(\type{T'})}, \overline{\sigma(\type{S'}) <: \sigma(\type{N'})}$ +% %TODO: Rephrase (\Delta' is used three times!) +% %The function $\CC{}$ is given as $\CC{}(\wcNtype{\Delta}{N}) = \type{N}$ +% \end{description} +% \end{lemma} \textit{Proof:} %(we are going backwards over the algorithm) %first we have to determine the \Delta'' -> it's only the wildcards which are free in N @@ -96,8 +133,18 @@ $\Delta \vdash \sigma(C') \implies \Delta \vdash \sigma(C)$ %\item[Capture, Reduce] are always applied together. We have to destinct between two cases: \item[Capture] If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists. -If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$ we have to show $\Delta' \vdash \text{CC}(\sigma(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}})) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$, -which holds by assumption with $\Delta'$ chosen in a way that $\text{fv}(\exptype{C}{\ol{S}}) \subseteq \Delta'$. The variables $\ol{C}$ in $\ol{S}$ can be renamed to $\ol{B}$, because $\ol{C}$ are fresh. +If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$ the preposition holds because +$\Delta, \Delta' \vdash [\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} <: \wctype{\Delta}{C}{\ol{T}}$ $\implies$ +$\Delta' \Delta \vdash \text{CC}(\sigma(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}})) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$ + +%we have to show $\Delta' \vdash \text{CC}(\sigma(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}})) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$, +%which holds by assumption with $\Delta'$ chosen in a way that $\text{fv}(\exptype{C}{\ol{S}}) \subseteq \Delta'$. The variables $\ol{C}$ in $\ol{S}$ can be renamed to $\ol{B}$, because $\ol{C}$ are fresh. + +% If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$ +% we have to show $\set{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}, \Delta \vdash \sigma(\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$, +% which holds by assumption with $\Delta'$ chosen in a way that $\text{fv}(\exptype{C}{\ol{S}}) \subseteq \Delta'$. +% The variables $\ol{C}$ in $\ol{S}$ can be renamed to $\ol{B}$, because $\ol{C}$ are fresh. + %If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$ we have to show $\Delta \vdash \sigma(\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$. %$\Delta \vdash \sigma([\ol{C}/\ol{B}]\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$ holds by assumption and %the variables $\ol{B}$ in $\ol{S}$ can be renamed to $\ol{C}$, because $\ol{C} \notin \ol{S}$ ($\ol{C}$ are fresh). @@ -106,9 +153,19 @@ which holds by assumption with $\Delta'$ chosen in a way that $\text{fv}(\exptyp %We are doing a capture conversion. If $\type{T}$ does not contain free variables, this does not affect the subtype relation. \item[Reduce] %Assumption and S-Exists. -If $\text{fv}(\exptype{C}{\ol{S}}) = \emptyset$ the preposition holds by Assumption and S-Exists. -If $\text{fv}(\exptype{C}{\ol{S}}) \neq \emptyset$ there exists a $\Delta'$ with -$\Delta' \vdash \text{CC}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$. +% Three different cases of the constraint $\exptype{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$: +% \begin{description} +% \item[$\text{fv}(\exptype{C}{\ol{S}}) = \emptyset, \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$:] +% the preposition holds by Assumption and S-Exists. +% \item[$\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$:] +% then $\text{fv}(\exptype{C}{\ol{S}}) \subseteq \Delta'$ with $\Delta' = \overline{\wildcard{A}{\type{U}}{\type{L}}}$ +% \item[$\text{fv}(\exptype{C}{\ol{S}}) = \emptyset$] $\Delta' = \emptyset$ +% \end{description} +% List <. Y.List, free variables are either in +If $\text{fv}(\exptype{C}{\ol{S}}) = \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists. +Otherwise +$\Delta' \vdash \CC{}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$ +holds with any $\Delta'$ so that $(\text{fv}(\exptype{C}{\ol{S}}) \cup \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) ) \subseteq \text{dom}(\Delta') $. \item[Match] Assumption, S-Trans \item[Trim] Assumption and S-Exists \item[Remove] $C$ is not changed @@ -183,18 +240,3 @@ $\sigma(\wildcardEnv) = \sigma([\type{T}/\tv{a}]\wildcardEnv)$ %Proof by Lemma 5 \emph{Type substitution preserves subtyping} from \cite{WildcardsNeedWitnessProtection}. Same as Subst \end{description} - -\subsection{Type Inference Soundness} -The type solution is a correct one in respect to the type rules. - -Problem: -The capture conversion and let statements. -Constraint a <. b => CC(X.C) <: C -Why is X the only type used - -$\type{T} \lessdot \type{S}$: -If the left part of the constraint has no free variables the solution $\sigma(\type{T})$ will have neither. -This means that all used type variables on both sides are bound in the global environment or the environment of the left side -%X.C <: C -%C = C (both sides must be the same) -%the left side has no free variables! \ No newline at end of file diff --git a/tiRules.tex b/tiRules.tex new file mode 100644 index 0000000..9ef32d5 --- /dev/null +++ b/tiRules.tex @@ -0,0 +1,208 @@ +\section{Typeless FJ} + +\subsection{Syntax} +We use the TameFJ syntax for the most part (\ref{fig:syntax-tamingfj}). + +\begin{figure}[tp] + \begin{align*} + \mv N &::= \exptype{C}{\ol{W}}\\ + \mv T &::= \mv X \mid \wctype{\ol{W}}{C}{\ol{W}}\\ + \mv W &::= \mv T \mid \wildcard{Z}{T}{T}\\ + \mv L &::= \mathtt{class} \ \exptype{C}{\ol{X} \triangleleft \ol{T}} \triangleleft \ \mv N\ \{ \ol{T} \ \ol{f}; \,\mv K \, \ol{M} \} \\ + \mv K &::= \mv C(\ol{f})\ \{\mathtt{super}(\ol{f}); \ \mathtt{this}.\ol{f}=\ol{f};\} \\ + \mv M &::= \mathtt{m}(\ol{x})\ = \mv e \\ + \mv e &::= \mv x \mid \mv e.\mv f \mid + \mv e.\mathtt{m}(\ol{e}) \mid \mathtt{new}\ \mathtt{C}(\ol{e}) + \mid \mv e \elvis{} \mv e + \end{align*} + \caption{Syntax of TameFJ + Type Inference} + \label{fig:syntax-tamingfj} + \end{figure} + +\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} \ No newline at end of file