Cleanup, rephrase introduction. Fix and Cleanup type rules. Remove override
This commit is contained in:
Andreas Stadelmeier
parent
6c716c5138
commit
26678767c2
@ -126,7 +126,7 @@ $\begin{array}{rcl}
|
||||
|
||||
\input{tRules}
|
||||
|
||||
\input{tiRules}
|
||||
%\input{tiRules}
|
||||
|
||||
\input{constraints}
|
||||
|
||||
|
||||
@ -1,14 +1,15 @@
|
||||
\section{Constraint generation}
|
||||
Our type inference algorithm is split into two parts.
|
||||
A constraint generation step \textbf{TYPE} and a \unify{} step.
|
||||
% Our type inference algorithm is split into two parts.
|
||||
% A constraint generation step \textbf{TYPE} and a \unify{} step.
|
||||
|
||||
Method names are not unique.
|
||||
It is possible to define the same method in multiple classes.
|
||||
The \TYPE{} algorithm accounts for that by generating Or-Constraints.
|
||||
This can lead to multiple possible solutions.
|
||||
% Method names are not unique.
|
||||
% It is possible to define the same method in multiple classes.
|
||||
% The \TYPE{} algorithm accounts for that by generating Or-Constraints.
|
||||
% This can lead to multiple possible solutions.
|
||||
|
||||
%\subsection{Well-Formedness}
|
||||
|
||||
The \fjtype{} algorithm assumes capture conversions for every method parameter.
|
||||
|
||||
%Why do we need a constraint generation step?
|
||||
%% The problem is NP-Hard
|
||||
|
||||
@ -17,11 +17,21 @@ In Java this is done implicitly by a process called capture conversion \cite{Jav
|
||||
The type system in \cite{WildcardsNeedWitnessProtection} makes this process explicit by using \texttt{let} statements.
|
||||
Our type inference algorithm will accept an input program without let statements and add them where necessary.
|
||||
|
||||
The input to the type inference algorithm is a Featherweight Java program without let statements (see figure \ref{fig:syntax}).
|
||||
The input to the type inference algorithm is a Featherweight Java program (example in figure \ref{fig:nested-list-example-typeless}) conforming to the syntax shown in figure \ref{fig:syntax}.
|
||||
Type inference adds \texttt{let} statements in a fashion similar to the Java capture conversion \cite{WildFJ}.
|
||||
We wrap every parameter of a method invocation in \texttt{let} statement unknowing if a capture conversion is necessary (see figure \ref{fig:nested-list-example-let}).
|
||||
The \fjtype{} algorithm calculates constraints based on this intermediate representation,
|
||||
which are then solved by the \unify{} algorithm
|
||||
resulting in a correctly typed program (see figure \ref{fig:nested-list-example-typed}).
|
||||
|
||||
We figured the \texttt{let} statements to be obsolete for our use case.
|
||||
Once the type inference algorithm found a correct type solution
|
||||
Once the type inference algorithm found a correct type solution they can be inferred by the given type annotations.
|
||||
|
||||
% 1. Constraint generation
|
||||
% 2. Insert typing
|
||||
|
||||
% # Showing soundness
|
||||
% Every program in our calculus can be converted to a WildcardsNeedWitnessProtection program
|
||||
|
||||
\begin{figure}[tp]
|
||||
\begin{subfigure}[t]{\linewidth}
|
||||
@ -48,6 +58,27 @@ class List<A> {
|
||||
List<A> add(A v) { ... }
|
||||
}
|
||||
|
||||
class Example {
|
||||
m(l, la, lb){
|
||||
return let r2 : (*@$\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$@*) = {
|
||||
let r1 : (*@$\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$@*) = l in {
|
||||
let p1 : (*@$\exptype{List}{\type{Integer}}$@*) = {
|
||||
let xa = la in xa.add(1)
|
||||
} in x1.add(p1)
|
||||
} in {
|
||||
let p2 = {
|
||||
let xb = lb in xb.add("str")
|
||||
} in x2.add(p2)
|
||||
};
|
||||
}
|
||||
}
|
||||
\end{lstlisting}
|
||||
|
||||
\begin{lstlisting}[style=tfgj]
|
||||
class List<A> {
|
||||
List<A> add(A v) { ... }
|
||||
}
|
||||
|
||||
class Example {
|
||||
m((*@$\exptype{List}{\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}}$@*) l, List<Integer> la, List<String> lb){
|
||||
return l
|
||||
@ -57,7 +88,7 @@ class Example {
|
||||
}
|
||||
\end{lstlisting}
|
||||
\caption{Featherweight Java Representation}
|
||||
\label{fig:nested-list-example-typed}
|
||||
\label{fig:nested-list-example-let}
|
||||
\end{subfigure}
|
||||
~
|
||||
\begin{subfigure}[t]{\linewidth}
|
||||
|
||||
@ -198,8 +198,8 @@
|
||||
\end{tcolorbox}
|
||||
}
|
||||
|
||||
\newcommand{\wcNtype}[2]{#1 .\ntype{#2}}
|
||||
\newcommand{\wctype}[3]{#1 .\exptype{#2}{#3}}
|
||||
\newcommand{\wcNtype}[2]{\exists #1 .\ntype{#2}}
|
||||
\newcommand{\wctype}[3]{\exists #1 .\exptype{#2}{#3}}
|
||||
\newcommand{\wtype}[1]{\mathit{#1}}
|
||||
\newcommand{\ntype}[1]{\mathtt{#1}}
|
||||
|
||||
|
||||
149
soundness.tex
149
soundness.tex
@ -420,3 +420,152 @@ $\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{Converting to Wild FJ}
|
||||
Figure \ref{fig:tletexpr} shows type rules for fields and method calls.
|
||||
They have been merged with let statements and simplified.
|
||||
|
||||
The let statements and the type $\wcNtype{\Delta'}{N}$, which the type inference algorithm can freely choose,
|
||||
are necessary for the soundness proof.
|
||||
|
||||
%TODO: Show that well-formed implies witnessed!
|
||||
We change the type rules to require the well-formedness instead of the witnessed property.
|
||||
See figure \ref{fig:well-formedness}.
|
||||
|
||||
Our well-formedness criteria is more restrictive than the ones used for \wildFJ{}.
|
||||
\cite{WildcardsNeedWitnessProtection} works with the two different judgements $\ok$ and \texttt{witnessed}.
|
||||
With \texttt{witnessed} being the stronger one.
|
||||
We rephrased the $\ok$ judgement to include \texttt{witnessed} aswell.
|
||||
$\type{T} \ \ok$ in this paper means $\type{T} \ \ok$ and $\type{T} \ \texttt{witnessed}$ in the sense of the \wildFJ{} type rules.
|
||||
Java's type system is complex enough as it is. Simplification, when possible, is always appreciated.
|
||||
Our $\ok$ rule may not be able to express every corner of the Java type system, but is sufficient to show soundness regarding type inference for a Java core calculus.
|
||||
|
||||
The \rulename{WF-Class} rule requires upper and lower bounds to be direct subtypes of each other $\type{L} <: \type{U}$.
|
||||
The type rules from \cite{WildcardsNeedWitnessProtection} use a witness type instead.
|
||||
Stating that a type is well formed (\texttt{witnessed}) if there exists atleast one simple type $\type{N}$ as a possible subtype:
|
||||
$\Delta \vdash \type{N} <: \wctype{\Delta'}{C}{\ol{T}}$.
|
||||
|
||||
A witness type is easy to find by replacing every wildcard $\ol{W}$ in $\wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$ by its upper bound:
|
||||
$\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} <: \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$.
|
||||
$\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} \ \texttt{witnessed}$ is given due to $\Delta \vdash \ol{T}, \ol{L}, \ol{U} \ \ok$
|
||||
and $\Delta \vdash \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}} \ \ok$.
|
||||
|
||||
\begin{figure}[tp]
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Var}\\
|
||||
\begin{array}{@{}c}
|
||||
x : \type{T} \in \Gamma
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\Delta | \Gamma \vdash 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}\\
|
||||
\Delta | \Gamma \vdash \letstmt{\ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}{\texttt{new} \ \exptype{C}{\ol{T}}(\overline{t})} : \type{T}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em]
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Field}\\
|
||||
\begin{array}{@{}c}
|
||||
\Delta | \Gamma \vdash \texttt{t} : \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{let}\ x : \wcNtype{\Delta'}{N} = \texttt{t} \ \texttt{in}\ x.\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
|
||||
\textit{mtype}(\texttt{m}, \type{N}) = \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \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{t}_r : \type{T}_r \quad \quad
|
||||
\Delta | \Gamma \vdash \ol{t} : \ol{T} \quad \quad
|
||||
\Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
|
||||
\Delta \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
|
||||
\\
|
||||
\Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
|
||||
\Delta, \Delta', \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 \letstmt{x : \wcNtype{\Delta'}{N} = t_r, \ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}
|
||||
{\texttt{x}.\generics{\ol{S}}\texttt{m}(\ol{x})} : \type{T}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em]
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Elvis}\\
|
||||
\begin{array}{@{}c}
|
||||
\Delta | \Gamma \vdash t_1 : \type{T}_1 \quad \quad
|
||||
\Delta | \Gamma \vdash t_2 : \type{T}_2 \quad \quad
|
||||
\Delta \vdash \type{T}_1 <: \type{T} \quad \quad
|
||||
\Delta \vdash \type{T}_2 <: \type{T}
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\Delta | \Gamma \vdash t_1 \elvis{} t_2 : \type{T}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em]
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Method}\\
|
||||
\begin{array}{@{}c}
|
||||
\text{dom}(\Delta)=\ol{X} \quad \quad
|
||||
\Delta' = \overline{\type{Y} : \bot .. \type{U}} \quad \quad
|
||||
\Delta, \Delta' \vdash \ol{U}, \type{T}, \ol{T}\ \ok \quad \quad
|
||||
\texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \set{\ldots} \\
|
||||
\Delta, \Delta' | \overline{x:\type{T}}, \texttt{this} : \exptype{C}{\ol{X}} \vdash t:\type{S} \quad \quad
|
||||
\Delta, \Delta' \vdash \type{S} <: \type{T} \quad \quad
|
||||
\text{override}(\texttt{m}, \type{N}, \generics{\ol{Y \triangleleft U}}\ol{T} \to \type{T})
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\Delta \vdash \generics{\ol{Y \triangleleft U}} \type{T} \ \texttt{m}(\overline{\type{T} \ x}) = t \ \ok \ \texttt{in C}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em]
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Class}\\
|
||||
\begin{array}{@{}c}
|
||||
\Delta = \overline{\type{X} : \bot .. \type{U}} \quad \quad
|
||||
\Delta \vdash \ol{U}, \ol{T} \ \ok \quad \quad
|
||||
\Delta \vdash \type{N} \ \ok \quad \quad
|
||||
\Delta \vdash \ol{M} \ \ok \texttt{ in C}
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M} } \ \ok
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\caption{T-Call and T-Field} \label{fig:tletexpr}
|
||||
\end{figure}
|
||||
|
||||
|
||||
213
tRules.tex
213
tRules.tex
@ -1,4 +1,15 @@
|
||||
\section{Syntax}
|
||||
\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}.
|
||||
|
||||
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}
|
||||
@ -21,13 +32,12 @@ $
|
||||
\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}$.
|
||||
|
||||
\section{Type rules}
|
||||
% 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}
|
||||
@ -74,7 +84,7 @@ $\begin{array}{l}
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\Delta \vdash \wctype{\Delta'}{C}{\ol{T}} <: \wctype{\Delta'}{D}{[\ol{T}/\ol{X}]\ol{S}}
|
||||
\Delta \vdash \wcNtype{\Delta'}{\type{N}} <: \wcNtype{\Delta'}{[\ol{T}/\ol{X}]\type{N}}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
$\begin{array}{l}
|
||||
@ -82,15 +92,16 @@ $\begin{array}{l}
|
||||
\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 \quad
|
||||
\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 \wctype{\Delta'}{C}{[\ol{T}/\ol{\type{X}}]\ol{S}} <:
|
||||
\wctype{\ol{\wildcard{X}{U}{L}}}{C}{\ol{S}}
|
||||
\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}
|
||||
|
||||
@ -141,69 +152,32 @@ $\begin{array}{l}
|
||||
\end{center}
|
||||
\caption{Well-formedness}\label{fig:well-formedness}
|
||||
\end{figure}
|
||||
%TODO: Proof that well-formed (ok) implies that a type is witnessed
|
||||
We change the type rules to require the well-formedness instead of the witnessed property.
|
||||
See figure \ref{fig:well-formedness}.
|
||||
|
||||
Our well-formedness criteria is more restrictive than the ones used for \wildFJ{}.
|
||||
\cite{WildcardsNeedWitnessProtection} works with the two different judgements $\ok$ and \texttt{witnessed}.
|
||||
With \texttt{witnessed} being the stronger one.
|
||||
We rephrased the $\ok$ judgement to include \texttt{witnessed} aswell.
|
||||
$\type{T} \ \ok$ in this paper means $\type{T} \ \ok$ and $\type{T} \ \texttt{witnessed}$ in the sense of the \wildFJ{} type rules.
|
||||
Java's type system is complex enough as it is. Simplification, when possible, is always appreciated.
|
||||
Our $\ok$ rule may not be able to express every corner of the Java type system, but is sufficient to show soundness regarding type inference for a Java core calculus.
|
||||
|
||||
The \rulename{WF-Class} rule requires upper and lower bounds to be direct subtypes of each other $\type{L} <: \type{U}$.
|
||||
The type rules from \cite{WildcardsNeedWitnessProtection} use a witness type instead.
|
||||
Stating that a type is well formed (\texttt{witnessed}) if there exists atleast one simple type $\type{N}$ as a possible subtype:
|
||||
$\Delta \vdash \type{N} <: \wctype{\Delta'}{C}{\ol{T}}$.
|
||||
|
||||
A witness type is easy to find by replacing every wildcard $\ol{W}$ in $\wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$ by its upper bound:
|
||||
$\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} <: \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$.
|
||||
$\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} \ \texttt{witnessed}$ is given due to $\Delta \vdash \ol{T}, \ol{L}, \ol{U} \ \ok$
|
||||
and $\Delta \vdash \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}} \ \ok$.
|
||||
|
||||
%Not necessary!
|
||||
% Additionally we do not allow nested wildcards. %TODO: Unify cannot create them (or does it?) What is when the input contains them
|
||||
|
||||
% The \unify{} algorithm is not capable of generating types like $\wctype{\rwildcard{X}, \wildcard{Y}{\bot}{\rwildcard{X}}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$.
|
||||
% %But they could be created in intermidiate types (\ol{S}) in method calls by capture conversion:
|
||||
% class WList<A> extends List<List<? extends A>>
|
||||
% m(List<X> l) % TODO
|
||||
% m(X.Wlist<X>) % S = Y^X.List<Y>
|
||||
|
||||
% X.WList<X> <. List<x?>
|
||||
% X.List<Y^X.List<Y>> <. List<x?>
|
||||
% x =. Y^X.List<Y>
|
||||
|
||||
% %TODO: do we need \Delta' \Delta \vdash T, L ,U ok ? or is \Delta \vdashh ... sufficient?
|
||||
% %<A> m(List<? extends A> l)
|
||||
% %This is important because it means different things maybe for the proof of our OK being more restrictive than "witnessed"
|
||||
|
||||
% % where can nested wildcards occur?
|
||||
% WBox<X> extends Box<Box<? extends X>>
|
||||
% WBox<?> => Y.WBox<Y> <: Y.Box<X^Y.Box<X>>
|
||||
|
||||
% Everything else regarding subtyping stays the same as in \cite{WildcardsNeedWitnessProtection}.
|
||||
% \begin{lemma}
|
||||
% If $\Delta \vdash $
|
||||
% \end{lemma}
|
||||
|
||||
Figure \ref{fig:tletexpr} shows type rules for fields and method calls.
|
||||
They have been merged with let statements and simplified.
|
||||
|
||||
The let statements and the type $\wcNtype{\Delta'}{N}$, which the type inference algorithm can freely choose,
|
||||
are necessary for the soundness proof.
|
||||
|
||||
\begin{figure}[tp]
|
||||
\begin{center}
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Var}\\
|
||||
\begin{array}{@{}c}
|
||||
x : \type{T} \in \Gamma
|
||||
\texttt{x} : \type{T} \in \Gamma
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\Delta | \Gamma \vdash x : \type{T}
|
||||
\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]
|
||||
@ -221,23 +195,7 @@ $\begin{array}{l}
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\Delta | \Gamma \vdash \letstmt{\ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}{\texttt{new} \ \exptype{C}{\ol{T}}(\overline{t})} : \type{T}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em]
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Field}\\
|
||||
\begin{array}{@{}c}
|
||||
\Delta | \Gamma \vdash \texttt{t} : \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{let}\ x : \wcNtype{\Delta'}{N} = \texttt{t} \ \texttt{in}\ x.\texttt{f}_i : \type{S}
|
||||
\triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em]
|
||||
@ -245,72 +203,109 @@ $\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
|
||||
\textit{mtype}(\texttt{m}, \type{N}) = \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{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{t}_r : \type{T}_r \quad \quad
|
||||
\Delta | \Gamma \vdash \ol{t} : \ol{T} \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} <: \ol{\wcNtype{\Delta}{N}}
|
||||
\Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
|
||||
\\
|
||||
\Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
|
||||
\Delta, \Delta', \Delta'' \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \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 \letstmt{x : \wcNtype{\Delta'}{N} = t_r, \ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}
|
||||
{\texttt{x}.\generics{\ol{S}}\texttt{m}(\ol{x})} : \type{T}
|
||||
\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}
|
||||
\Delta | \Gamma \vdash t_1 : \type{T}_1 \quad \quad
|
||||
\Delta | \Gamma \vdash t_2 : \type{T}_2 \quad \quad
|
||||
\Delta \vdash \type{T}_1 <: \type{T} \quad \quad
|
||||
\Delta \vdash \type{T}_2 <: \type{T}
|
||||
\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}\\
|
||||
\Delta | \Gamma \vdash t_1 \elvis{} t_2 : \type{T}
|
||||
\triangle | \Gamma \vdash \texttt{t}_1 \ \texttt{?:} \ \texttt{t}_2 : \type{T}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\\[1em]
|
||||
\end{center}
|
||||
\caption{Expression Typing}\label{fig:expressionTyping}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}
|
||||
\begin{center}
|
||||
$\begin{array}{l}
|
||||
\typerule{T-Method}\\
|
||||
\begin{array}{@{}c}
|
||||
\text{dom}(\Delta)=\ol{X} \quad \quad
|
||||
\Delta' = \overline{\type{Y} : \bot .. \type{U}} \quad \quad
|
||||
\Delta, \Delta' \vdash \ol{U}, \type{T}, \ol{T}\ \ok \quad \quad
|
||||
\texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \set{\ldots} \\
|
||||
\Delta, \Delta' | \overline{x:\type{T}}, \texttt{this} : \exptype{C}{\ol{X}} \vdash t:\type{S} \quad \quad
|
||||
\Delta, \Delta' \vdash \type{S} <: \type{T} \quad \quad
|
||||
\text{override}(\texttt{m}, \type{N}, \generics{\ol{Y \triangleleft U}}\ol{T} \to \type{T})
|
||||
\exptype{C}{\ol{X}} \to \ol{T} \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad
|
||||
%\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 \\
|
||||
%\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}\\
|
||||
\Delta \vdash \generics{\ol{Y \triangleleft U}} \type{T} \ \texttt{m}(\overline{\type{T} \ x}) = t \ \ok \ \texttt{in C}
|
||||
\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}
|
||||
\Delta = \overline{\type{X} : \bot .. \type{U}} \quad \quad
|
||||
\Delta \vdash \ol{U}, \ol{T} \ \ok \quad \quad
|
||||
\Delta \vdash \type{N} \ \ok \quad \quad
|
||||
\Delta \vdash \ol{M} \ \ok \texttt{ in 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} \set{\overline{\type{T}\ f}; \ol{M} } \ \ok
|
||||
\texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \} : \mathtt{\Pi}''
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\caption{T-Call and T-Field} \label{fig:tletexpr}
|
||||
\\[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}
|
||||
19
tiRules.tex
19
tiRules.tex
@ -1,24 +1,5 @@
|
||||
\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}.
|
||||
|
||||
Loading…
Reference in New Issue
Block a user