189 lines
7.8 KiB
TeX
189 lines
7.8 KiB
TeX
\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} |