Ecoop2024_TIforWildFJ/tRules.tex

\section{Syntax and Typing}

The input syntax for our algorithm is shown in figure \ref{fig:syntax}
and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}.

Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
The input language is designed to showcase type inference involving existential types.
Method call rule T-Call is the most interesting part, because it emulates the behaviour of a Java method call,
where existential types are implicitly \textit{opened} and \textit{closed}.

%The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}.
%and is solely used for examples.
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}.

%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.

\begin{figure}
$
\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} & ::= & \generics{\ol{X \triangleleft T}} \type{T} \ \texttt{m}(\overline{\type{T}\ x}) = t \\
\text{Terms} & t & ::= & x \\
& & \ \ | & \texttt{new} \ \exptype{C}{\ol{T}}(\overline{t})\\
& & \ \ | & t.f\\
& & \ \ | & t.\generics{\ol{T}}\texttt{m}(\overline{t})\\
& & \ \ | & t \elvis{} t\\
\text{Variable contexts} & \Gamma & ::= & \overline{x:\type{T}}\\
\hline
\end{array}
$
\caption{Input Syntax}\label{fig:syntax}
\end{figure}

% Each class type has a set of wildcard types $\overline{\Delta}$ attached to it.
% The type $\wctype{\overline{\Delta}}{C}{\ol{T}}$ defines a set of wildcards $\overline{\Delta}$,
% which can be used inside the type parameters $\ol{T}$.

\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}(\wctype{\ol{\wildcard{X}{U}{L}}}{C}{\ol{S}}) = \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 \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] % TODO: we need subtyping for FJ without let statements. Problem is \Delta \vdash T witnessed. The \Delta here contains all the let statements beforehand.
% TODO: maybe do a rule which adds let statements at any place! Goal: a program which Unify calculates a type for is also correct under our type laws and can be converted to LefFJ
% motivation: do not use normal types as intermediate types. Keep a Pair<X,X> as that and not convert to X,Y.Pair<X,Y>
% it is possible because the parameters of the method are normal types. we can start capture converting them
% is it possible to say there exists any \Delta which makes the method body possible?
$\begin{array}{l}
    \typerule{T-Call}\\
    \begin{array}{@{}c}
        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\type{T}} \ \ok \quad \quad
        \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 \mid \Delta_G \quad \quad
        \Delta | \Gamma \vdash \ol{e} : \ol{T} \mid \overline{\Delta_G} \quad \quad
        \Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
        \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
        \\
        \overline{\Delta_G}, \Delta_G, \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} \mid \Delta', \overline{\Delta}
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
    \typerule{T-Call}\\
    \begin{array}{@{}c}
        \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 \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
        \\
        \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}} \quad \quad
        \Delta \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T} \mid \overline{\Delta}
    \end{array}
\end{array}$
% \Delta is not allowed to have wildcards depending on eachother. X^Y, Y^T for example
\\[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-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'} \quad \quad
        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok 
        \\
        \Delta | \Gamma \vdash \ol{e} : \ol{T} \quad \quad
        \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}} \quad \quad 
        \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
        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta | \Gamma \vdash \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}$
\end{center}
\caption{Expression Typing}\label{fig:expressionTyping}
\end{figure}

\begin{figure}
\begin{center}
    $\begin{array}{l}
        \typerule{T-Method}\\
% TODO: do a rule that forbids variables in Delta which are not introduced by a capture conversion
        \begin{array}{@{}c}
            \exptype{C}{\ol{X}} \to \ol{T} \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad
            \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \quad \quad
            \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \\
            \text{dom}(\triangle) = \ol{X} \quad \quad
            %\texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \ \{ \ldots \} \\
            \mathtt{\Pi} | \triangle, \triangle', \overline{\triangle} | \ol{x : T}, \texttt{this} : \exptype{C}{\ol{X}} \vdash \texttt{e} : \type{S} \mid \overline{\Delta} \quad \quad 
            \triangle \vdash \type{S} <: \type{T}
            \\
            \hline
        \vspace*{-0.3cm}\\
            \mathtt{\Pi} | \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-Method}\\
    \begin{array}{@{}c}
        \exptype{C}{\ol{X}} \to \ol{T} \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad
        \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \quad \quad
        \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \\
        \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}) = \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{ \exptype{C}{\ol{X}}.\texttt{m} : \ol{T}_\texttt{m} \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M}} \\
        \mathtt{\Pi}'' = \mathtt{\Pi} \cup \set{ \exptype{C}{\ol{X}}.\texttt{m} :
            \generics{\ol{X \triangleleft \type{N}}, \ol{Y \triangleleft P}}\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
        \mathtt{\Pi}' | \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{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}$
\end{figure}