From 3a499d2e6ddfc585c4f6b233aa057438c087908a Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Thu, 4 Jan 2024 01:33:36 +0100 Subject: [PATCH] Add well-formedness description --- soundness.tex | 11 +++++++++-- tRules.tex | 22 ++++++++++++++++++++++ unify.tex | 20 ++++++++++++-------- 3 files changed, 43 insertions(+), 10 deletions(-) diff --git a/soundness.tex b/soundness.tex index 60bbd60..3a5ae1f 100644 --- a/soundness.tex +++ b/soundness.tex @@ -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 --> 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 diff --git a/tRules.tex b/tRules.tex index acdc5ed..43870d8 100644 --- a/tRules.tex +++ b/tRules.tex @@ -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? +% m(List 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. diff --git a/unify.tex b/unify.tex index 885aaa0..110803b 100644 --- a/unify.tex +++ b/unify.tex @@ -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} $ \\\\