stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add well-formedness description

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-01-04 01:33:36 +01:00
parent d4c43c04a7
commit 3a499d2e6d
3 changed files with 43 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
soundness.tex
View File

@ -46,6 +46,7 @@ By structural induction over the expression $\texttt{e}$.
% $\Delta, \Delta' \vdash \type{U}_i <: \type{S}$ by premise.
$\Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok$ %TODO
%Easy, because unify only generates substitutions for normal type placeholders which are OK
\item[$\texttt{e}.\texttt{m}(\ol{e})$] Given
\end{description}
@ -59,11 +60,17 @@ By structural induction over the expression $\texttt{e}$.
\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
%UNIFY fails when there are free variables on the right side of a a =. T constraint
\begin{lemma}
\unify{} only produces well-formed type substitutions.
% Could this be done via the GenSigma rule? just check if substitutions are well-formed?
% L <. U
% not possible because well-formedness depends on the input, which is not checked (should we check it? is that possible?)
%only type variables have to be OK
% TODO: Problem: how to proof \ol{S} ok for T-Call.
% a <. List<x?> --> here the type substituted for x? must be ok. Proof that by changing Unify to not return type insertions for this type and assume there is a correct substitution for x
\end{lemma}
% %This lemma can be used to proof Normalize rule!
@ -146,7 +153,7 @@ $\Delta \vdash \sigma(C') \implies \Delta \vdash \sigma(C)$
\begin{description}
\item[AddDelta] $C$ is not changed
\item[GenDelta] by definition, S-Var-Left, and S-Trans %The generated type variable is unique due to the solved form property. %and the solved form property (no $\tv{a}$ in $C$)
\item[GenSigma] by definition.
\item[GenSigma] by definition and S-Refl.
% holds for $\set{\tv{a} \doteq \type{G}}$ by definition.
% Holds for $C$ by assumption and because $\tv{a} \notin C$ by solved form definition ($[\type{G}/\tv{a}]C = C$).
\item[Ground] Assumption and S-Bot

22
tRules.tex
View File

@ -139,6 +139,28 @@ $\begin{array}{l}
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}}$.
%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"
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.

20
unify.tex
View File

@ -949,19 +949,23 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
\wildcardEnv \vdash [\type{B}/\tv{b}]C \implies \Delta \cup \set{\wildcard{B}{\type{N}}{\bot}}, \sigma \cup \set{\tv{b} \to \type{B}}
} \quad
\begin{array}{l}
\tph(\type{N}) = \emptyset, \text{fv}(\type{N}) = \emptyset \\
\rwildcard{B} \ \text{fresh}, \tv{b} \notin \text{dom}(\sigma)
\tph(\type{N}) = \emptyset, \text{fv}(\type{N}) \subseteq \Delta \\
\rwildcard{B} \ \text{fresh}, \tv{b} \notin \text{dom}(\sigma), \Delta \vdash \type{N} \ \ok
\end{array}
$
\\\\
\rulename{AddSigma}
\rulename{AddSigma} %This rule adds the substitutions for a? variables
& $
\deduction{
\wildcardEnv \vdash C \cup \set{\tv{a} \doteq \rwildcard{X}} \implies \Delta, \sigma
\wildcardEnv \vdash C \cup \set{\tv{a} \doteq \type{T}} \implies \Delta, \sigma
}{
\wildcardEnv \vdash C \cup \set{\tv{a} \doteq \rwildcard{X}} \implies \Delta, \sigma
\wildcardEnv \vdash C \cup \set{\tv{a} \doteq \type{T}} \implies \Delta, \sigma
\cup \set{\tv{a} \to \rwildcard{X}}
}
} \quad
\begin{array}{l}
\tph(\type{T}) = \emptyset \\
\tv{a} \notin \text{dom}(\sigma),\, \Delta \vdash \type{T} \ \ok
\end{array}
$
\\\\
\rulename{GenSigma}
@ -974,8 +978,8 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
\set{\tv{a} \to \type{T} }
} \quad
\begin{array}{l}
\tph(\type{T}) = \emptyset \\
\tv{a} \notin \text{dom}(\sigma)
\tph(\type{T}) = \emptyset \\ %,\, \text{fv}(\type{T}) \subseteq \Delta \\ % T ok implies that
\tv{a} \notin \text{dom}(\sigma),\, \Delta \vdash \type{T} \ \ok
\end{array}
$
\\\\