Ecoop2024_TIforWildFJ/tiRules.tex

208 lines
8.6 KiB
TeX

\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}