Add to Soundness. Start Wellformed lemma, add T-Rules
This commit is contained in:
Andreas Stadelmeier
parent
14ebe4c360
commit
d4c43c04a7
@ -124,7 +124,7 @@ $\begin{array}{rcl}
|
||||
|
||||
|
||||
|
||||
%\input{tRules}
|
||||
\input{tRules}
|
||||
|
||||
\input{tiRules}
|
||||
|
||||
|
||||
@ -26,7 +26,7 @@
|
||||
\newcommand{\olsub}{\textrm{$<:$}\ }
|
||||
|
||||
\newcommand{\sub}\olsub%{\mbox{$<$}}
|
||||
\newcommand{\ok}{\text{ok}}
|
||||
\newcommand{\ok}{\texttt{ok}}
|
||||
|
||||
\newcommand{\set}[1]{\{ #1 \} }
|
||||
|
||||
|
||||
@ -20,24 +20,52 @@ Type inference produces a correctly typed program.
|
||||
, 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{}$
|
||||
and $\Gamma \subseteq \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})$
|
||||
%and $\Delta \vdash \sigma(\type{S}), \sigma(\type{T})\ \ok$
|
||||
\item[then] $\Delta|\Gamma \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.
|
||||
\item[$\texttt{e}.\texttt{f}$] $\Delta|\Gamma \vdash \texttt{e} : \sigma(\tv{r})$ by assumption.
|
||||
$\Delta', \Delta\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}$.
|
||||
This implies $\Delta, \Delta' \vdash \type{U}_i <: \type{S}$,
|
||||
because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$
|
||||
and $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$.
|
||||
|
||||
% Set $\sigma(\tv{r}) = \type{T} = \wcNtype{\Delta'}{N}$.
|
||||
% Then $\Delta | \Gamma \vdash e : \type{T}$ by assumption. $\Delta \vdash \type{T} <: \wcNtype{\Delta'}{N}$ by S-Refl.
|
||||
% $\textit{fields}(\type{N}) = \overline{\type{U}\ f}$ by definition.
|
||||
% $\Delta, \Delta' \vdash \type{U}_i <: \type{S}$ by premise.
|
||||
|
||||
$\Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok$ %TODO
|
||||
|
||||
\item[$\texttt{e}.\texttt{m}(\ol{e})$] Given
|
||||
\end{description}
|
||||
|
||||
\begin{lemma}
|
||||
\begin{description}
|
||||
\item[If] $(\sigma, \Delta) = \unify{}( C )$
|
||||
\item[Then] $\forall x \in \set{\type{S} \mid \type{S} \in C, \text{fv}(\type{S}) = \emptyset }: \text{fv}(\sigma(\type{S})) \subseteq \text{dom}(\Delta)$
|
||||
\end{description}
|
||||
\end{lemma}
|
||||
\textit{Proof:} by induction over the \unify{} algorithm.
|
||||
A unifier $\sigma(\tv{a}) = \type{T}$, where the type variable $\tv{a}$ is not flagged as a wildcard will always hold
|
||||
$\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
|
||||
%TODO: Unify subst rule does not fail when there are free type variables on the right side
|
||||
|
||||
\begin{lemma}
|
||||
\unify{} only produces well-formed type substitutions.
|
||||
% Could this be done via the GenSigma rule? just check if substitutions are well-formed?
|
||||
\end{lemma}
|
||||
|
||||
% %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.
|
||||
|
||||
266
tRules.tex
Normal file
266
tRules.tex
Normal file
@ -0,0 +1,266 @@
|
||||
\section{Syntax}
|
||||
$
|
||||
\begin{array}{lrcl}
|
||||
\hline
|
||||
\text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{W}} \\
|
||||
\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} & ::= & \generics{\ol{X \triangleleft T}} \type{T} \ \texttt{m}(\overline{\type{T}\ x}) = t \\
|
||||
\text{Terms} & t & ::= & x \\
|
||||
& & \ \ | & \texttt{new} \ \exptype{C}{\ol{T}}(\overline{t})\\
|
||||
& & \ \ | & t.f\\
|
||||
& & \ \ | & t.\generics{\ol{T}}\texttt{m}(\overline{t})\\
|
||||
& & \ \ | & t \elvis{} t\\
|
||||
\text{Variable contexts} & \Gamma & ::= & \overline{x:\type{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}$.
|
||||
It is important that each wildcard declaration $\wildcard{X}{T}{L}$ is unique.
|
||||
|
||||
|
||||
\section{Type rules}
|
||||
|
||||
\begin{figure}[tp]
|
||||
$\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 \exptype{D}{\ol{S}} \ \{ \ldots \} \\
|
||||
\ol{X} \cap \text{dom}(\Delta) = \emptyset
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\Delta \vdash \wctype{\Delta'}{C}{\ol{T}} <: \wctype{\Delta'}{D}{[\ol{T}/\ol{X}]\ol{S}}
|
||||
\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 \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}}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\caption{Subtyping}\label{fig:subtyping}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}[tp]
|
||||
$\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}
|
||||
\Delta \vdash \ol{L}, \ol{U} \ \ok
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\Delta \vdash \wildcard{W}{U}{L} \ \ok
|
||||
\end{array}
|
||||
\end{array}$
|
||||
$\begin{array}{l}
|
||||
\typerule{WF-Class}\\
|
||||
\begin{array}{@{}c}
|
||||
\Delta \vdash \ol{T}, \ol{L}, \ol{U} \ \ok \quad \quad
|
||||
\Delta \vdash \ol{L} <: \ol{U} \\
|
||||
\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}$
|
||||
\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}.
|
||||
|
||||
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{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}
|
||||
|
||||
|
||||
@ -491,6 +491,10 @@ $\wctype{\ol{\rwildcard{A}}}{C}{\ol{\rwildcard{A}}}$.
|
||||
Apply the rules depicted in the figures \ref{fig:normalizing-rules}, \ref{fig:reduce-rules} and \ref{fig:wildcard-rules} exhaustively.
|
||||
Starting with the \rulename{circle} rule. Afterwards the other rules in figure \ref{fig:normalizing-rules}.
|
||||
|
||||
If we find an illicit constraint assigning a type containing free variables to a type placeholder not flagged as a wildcard placeholder the algorithm fails.
|
||||
|
||||
$\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \neq \emptyset$ $\implies$ fail!
|
||||
|
||||
The first step of the algorithm is able to remove wildcards.
|
||||
Removing a wildcard works by setting its lower and upper bound to be equal.
|
||||
(Def: $\type{Object} = \wildcard{A}{Object}{Object}$).
|
||||
|
||||
Loading…
Reference in New Issue
Block a user