567 lines
21 KiB
TeX
567 lines
21 KiB
TeX
\section{Syntax and Typing}\label{sec:tifj}
|
|
|
|
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 calculus is a subset of the calculus defined by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection}
|
|
with the exception that type annotations are optional in our calculus.
|
|
|
|
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}.
|
|
|
|
Example: %TODO
|
|
\begin{verbatim}
|
|
class List<A> {
|
|
A head;
|
|
List<A> tail;
|
|
|
|
add(v) = new List(v, this);
|
|
}
|
|
\end{verbatim}
|
|
|
|
%The rules depicted here are type inference rules. It is not possible to derive a distinct typing from a given input program.
|
|
|
|
%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.
|
|
|
|
The syntax forces every expression to undergo a capture conversion before it can be used as a method argument.
|
|
Even variables have to be catched by a let statement first.
|
|
This behaviour emulates Java's implicit capture conversion.
|
|
|
|
\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} & ::= & \texttt{m}(\overline{\expr{x}}) \set{ \texttt{return}\ t;} \\
|
|
\text{Terms} & t & ::= & \expr{x} \\
|
|
& & \ \ | & \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}_c}) \\
|
|
& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \expr{x}_c.f \\
|
|
& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \expr{x}_c.\texttt{m}(\overline{\expr{x}_c}) \\
|
|
& & \ \ | & t \elvis{} t \\
|
|
\text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
|
|
\hline
|
|
\end{array}
|
|
$
|
|
\caption{\TamedFJ{} Syntax}\label{fig:syntax}
|
|
\end{figure}
|
|
|
|
% \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} & ::= & \texttt{m}(\overline{\expr{x}}) = t \\
|
|
% \text{Values} & v & ::= & \expr{x} \\
|
|
% \text{Terms} & t & ::= & v \\
|
|
% & & \ \ | & \texttt{let} \ \expr{x} = \texttt{new} \ \type{C}(\overline{v}) \ \texttt{in} \ t \\
|
|
% & & \ \ | & \texttt{let} \ \expr{x} = v.f \ \texttt{in} \ t \\
|
|
% & & \ \ | & \texttt{let} \ \expr{x} = v.\texttt{m}(\overline{v}) \ \texttt{in} \ t \\
|
|
% & & \ \ | & \texttt{let} \ \expr{x} = v \elvis{} v \ \texttt{in} \ t \\
|
|
% \text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
|
|
% \hline
|
|
% \end{array}
|
|
% $
|
|
% \caption{Input Syntax}\label{fig:syntax}
|
|
% \end{figure}
|
|
|
|
% \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} & ::= & \texttt{m}(\overline{\expr{x}}) = t \\
|
|
% \text{Terms} & t & ::= & \expr{x} \\
|
|
% & & \ \ | & \texttt{let} \ \expr{x} = t \ \texttt{in} \ t \\
|
|
% & & \ \ | & \expr{x}.f \\
|
|
% & & \ \ | & \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
|
|
% & & \ \ | & t \elvis{} t \\
|
|
% \text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
|
|
% \hline
|
|
% \end{array}
|
|
% $
|
|
% \caption{Input Syntax}\label{fig:syntax}
|
|
% \end{figure}
|
|
|
|
|
|
% \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} & ::= & \texttt{m}(\overline{x}) = t \\
|
|
% \text{Terms} & t & ::= & x \\
|
|
% & & \ \ | & \texttt{new} \ \type{C}(\overline{t})\\
|
|
% & & \ \ | & t.f\\
|
|
% & & \ \ | & 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}
|
|
|
|
\subsection{ANF transformation}\label{sec:anfTransformation}
|
|
\newcommand{\anf}[1]{\ensuremath{\tau}(#1)}
|
|
%https://en.wikipedia.org/wiki/A-normal_form)
|
|
Featherweight Java's syntax involves no \texttt{let} statement
|
|
and terms can be nested freely.
|
|
This is similar to Java's syntax.
|
|
To convert it to \TamedFJ{} additional let statements have to be added.
|
|
This is done by a \textit{A-Normal Form} \cite{aNormalForm} transformation shown in figure \ref{fig:anfTransformation}.
|
|
The input of this transformation is a Featherweight Java program in the syntax given \ref{fig:inputSyntax}
|
|
and the output is a \TamedFJ{} program.
|
|
|
|
\textit{Example:}\\
|
|
\noindent
|
|
\begin{minipage}{0.45\textwidth}
|
|
\begin{lstlisting}[style=fgj,caption=Featherweight Java]
|
|
m(l, v){
|
|
return l.add(v);
|
|
}
|
|
\end{lstlisting}
|
|
\end{minipage}%
|
|
\hfill
|
|
\begin{minipage}{0.5\textwidth}
|
|
\begin{lstlisting}[style=tfgj,caption=\TamedFJ{} representation]
|
|
m(l, v) =
|
|
let x1 = l in
|
|
let x2 = v in x1.add(x2)
|
|
\end{lstlisting}
|
|
\end{minipage}
|
|
|
|
|
|
% $
|
|
% \begin{array}{|lrcl|l}
|
|
% \hline
|
|
% & & & \textbf{Featherweight Java Terms}\\
|
|
% \text{Terms} & t & ::=
|
|
% & \expr{x}
|
|
% \\
|
|
% & & \ \ |
|
|
% & \texttt{new} \ \type{C}(\overline{t})
|
|
% \\
|
|
% & & \ \ |
|
|
% & t.f
|
|
% \\
|
|
% & & \ \ |
|
|
% & t.\texttt{m}(\overline{t})
|
|
% \\
|
|
% & & \ \ |
|
|
% & t \elvis{} t\\
|
|
% %
|
|
% \hline
|
|
% \end{array}
|
|
% $
|
|
|
|
\begin{figure}
|
|
\begin{center}
|
|
$\begin{array}{lrcl}
|
|
%\text{ANF}
|
|
& \anf{\expr{x}} & = & \expr{x} \\
|
|
& \anf{\texttt{new} \ \type{C}(\overline{t})} & = & \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}}) \\
|
|
& \anf{t.f} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \expr{x}.f \\
|
|
& \anf{t.\texttt{m}(\overline{t})} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
|
|
& \anf{t_1 \elvis{} t_2} & = & \anf{t_1} \elvis{} \anf{t_2}
|
|
\end{array}$
|
|
\end{center}
|
|
\caption{ANF Transformation}\label{fig:anfTransformation}
|
|
\end{figure}
|
|
|
|
% $
|
|
% \begin{array}{lrcl|l}
|
|
% \hline
|
|
% & & & \textbf{Featherweight Java} & \textbf{A-Normal form} \\
|
|
% \text{Terms} & t & ::=
|
|
% & \expr{x}
|
|
% & \expr{x}
|
|
% \\
|
|
% & & \ \ |
|
|
% & \texttt{new} \ \type{C}(\overline{t})
|
|
% & \texttt{let}\ \overline{x} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{x})
|
|
% \\
|
|
% & & \ \ |
|
|
% & t.f
|
|
% & \texttt{let}\ x = t \ \texttt{in}\ x.f
|
|
% \\
|
|
% & & \ \ |
|
|
% & t.\texttt{m}(\overline{t})
|
|
% & \texttt{let}\ x_1 = t \ \texttt{in}\ \texttt{let}\ \overline{x} = \overline{t} \ \texttt{in}\ x_1.\texttt{m}(\overline{x})
|
|
% \\
|
|
% & & \ \ |
|
|
% & t \elvis{} t
|
|
% & t \elvis{} t\\
|
|
% %
|
|
% \hline
|
|
% \end{array}
|
|
% $
|
|
|
|
|
|
% 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}(\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}
|
|
(\type{T'},\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{ \texttt{m} : (\exptype{C}{\ol{X}}, \ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M}} \\
|
|
\mathtt{\Pi}'' = \mathtt{\Pi} \cup \set{ \texttt{m} :
|
|
\generics{\ol{X \triangleleft \type{N}}, \ol{Y \triangleleft P}}(\exptype{C}{\ol{X}},\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}$
|
|
\caption{Field access}
|
|
\end{figure} |