Fix errrors in TYPE. Fix Unify soundness proof. start TYPE Soundness proof. Add elimination/transformation WildFJ <-> WildFJ-GT
This commit is contained in:
Andreas Stadelmeier
parent
18dd2325a6
commit
14ebe4c360
@ -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}
|
||||
|
||||
|
||||
@ -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}\\
|
||||
|
||||
@ -26,6 +26,7 @@
|
||||
\newcommand{\olsub}{\textrm{$<:$}\ }
|
||||
|
||||
\newcommand{\sub}\olsub%{\mbox{$<$}}
|
||||
\newcommand{\ok}{\text{ok}}
|
||||
|
||||
\newcommand{\set}[1]{\{ #1 \} }
|
||||
|
||||
|
||||
@ -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<X> <. Y.List<Y>, 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<X>) <: C<X>
|
||||
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<X> <: C<X>
|
||||
%C<X> = C<X> (both sides must be the same)
|
||||
%the left side has no free variables!
|
||||
208
tiRules.tex
Normal file
208
tiRules.tex
Normal file
@ -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}
|
||||
Loading…
Reference in New Issue
Block a user