From 15c49c3cfc5f0a8445e0ac9b080baec5fd5fe6f4 Mon Sep 17 00:00:00 2001 From: regnat Date: Mon, 22 May 2017 16:24:42 +0200 Subject: [PATCH] Define the "oracle" type-system --- common/header.tex | 1 + main.tex | 7 +- soundness/intro.tex | 14 ++++ soundness/main.tex | 152 ------------------------------------------- soundness/oracle.tex | 63 ++++++++++++++++++ 5 files changed, 84 insertions(+), 153 deletions(-) create mode 100644 soundness/intro.tex delete mode 100644 soundness/main.tex create mode 100644 soundness/oracle.tex diff --git a/common/header.tex b/common/header.tex index 312320d..c252b4a 100644 --- a/common/header.tex +++ b/common/header.tex @@ -109,6 +109,7 @@ \newcommand{\tinfer}{\vdash^\Uparrow} \newcommand{\tcheck}{\vdash^\Downarrow} \newcommand{\tIC}{\vdash^\delta} +\newcommand{\toracle}{\vdash^\Updownarrow} \newcommand{\onerec}{\{ \textbf{..} \}} \DeclareCollectionInstance{plainmath}{xfrac}{mathdefault}{math} {% diff --git a/main.tex b/main.tex index a592bc3..3ad394e 100644 --- a/main.tex +++ b/main.tex @@ -47,7 +47,12 @@ We also present a compilation from nix to nix-light. \input{nix-light/typing/bidir.tex} \section{Soundness of the type-system} -\input{soundness/main} +\input{soundness/intro} + +\subsection{The oracle type-system} +\input{soundness/oracle} + +\subsection{Soundness of the oracle type-system} \section{Compilation} diff --git a/soundness/intro.tex b/soundness/intro.tex new file mode 100644 index 0000000..b22a9d9 --- /dev/null +++ b/soundness/intro.tex @@ -0,0 +1,14 @@ +The \emph{subject reduction} property does not hold for our type system. +Indeed, the checking part makes uses of annotations which are lost during +reduction, and designing a reduction system which keeps those annotations would +be non-trivial at all and would require the reduction system to be deeply +dependant on the structure of the types, which we want to avoid. +But we can imagine an extension of our type-system that would be able to guess +the type of any expression, and would just have to check it (some kind of +``oracle'' type-system). + +In this section, we present such a type-system, and proove that subject +reduction and progress both hold for it. +As both the ``infer'' and ``check'' type-systems are restrictions of the oracle +type-system (\emph{i.e.} every term well-typed in one of those is well-typed in +the oracle), we get as corollary the soundness of those. diff --git a/soundness/main.tex b/soundness/main.tex deleted file mode 100644 index 4b754c1..0000000 --- a/soundness/main.tex +++ /dev/null @@ -1,152 +0,0 @@ -We have the two classical results of \emph{Subject reduction} and -\emph{Progress} which entail type soundess for the non-gradual part of the -language. -Note that because we defined two typing judgements, both result will be stated -twice. - -We first prove the following lemmas: - -\begin{lemma}\label{lemma:inferCheck} - Let $e$ be an expression, $\Γ$ a typing environment and $\τ$ and $\τ'$ two - (possibly gradual) types with $\τ \subtypeG \τ'$. - If $\Γ \tinfer e : \τ$ then $\Γ \tcheck e : \τ'$. -\end{lemma} - -\begin{proof} - \todo{} -\end{proof} - -\begin{lemma}[Substitution]\label{lemma:substitution} - Let $e$ and $e'$ be expressions, $x$ be a variable, $\τ$ and $\τ'$ two types, - $\Γ$ a typing environment and $\delta$ be $\Uparrow$ or $\Downarrow$. - - If $\Γ; x : \τ' \tIC e : \τ$ and $\Γ \tinfer e' : \τ'$ then $\Γ \tIC - \subst{x}{e'}{e} : \τ$ -\end{lemma} - -\begin{proof} - By induction on the typing derivation of $\Γ; x : \τ' \tIC e : \τ$. We - replace every Ivar rule introducing $\Γ ; x : \τ' \tinfer x : \τ'$ by a - derivation of $\Γ \tinfer e' : \τ'$, and every Cvar rule introducing $\Γ ; x - : \τ' \tcheck x : \τ''$ (with $ \τ' \subtypeG \τ'')$ by a derivation of $\Γ - \tcheck e' : \τ''$ (which exists because of Lemma~\ref{lemma:inferCheck}). - - This builds a new derivation of $\Γ \tinfer \subst{x}{e'}{e} : \τ$. -\end{proof} - -\begin{theorem}[Subject reduction $\Uparrow$]\label{thm:subj-reduction-infer} - For any pair $e, e'$ of terms (of nix-light), if $\Γ \tinfer e : t$ and $e - \rightarrow e'$, then $\Γ \tinfer e' : t$. -\end{theorem} - -\begin{proof} - We consider an expression $e$ such that $\Γ \tinfer e : t$. - We prove by induction on the derivation of $\Γ \tinfer e : t$ that $\forall - e', (e \rightarrow e') \Rightarrow (\Γ \tinfer e' : t)$. - - Let's consider the various possibilities for the last rule of the derivation - $\Γ \tinfer e : t$. - - \begin{description} - \item[IVar,IConst,IAbs,ICons] The expression $e$ is a value and can't be - reduced, so the property holds. - \item[IApp] - $\inferrule{% - \Γ \tinfer e_1 : t_1 \\ \Γ \tinfer e_2 : t_2 \\ - t_1 \subtypeG \zero \rightarrow \one \\ - t_2 \subtypeG \dom(t_1) - }{% - \Γ \tinfer e_1~e_2 : t_1 \circ t_2 - }$ - - The expression $e$ has then the form $e_1~e_2$ with $\Γ \tinfer e_1 - : t_1$ and $\Γ \tinfer e_2 : t_2$ (and $t = t_1 \circ t_2$). - It can be reduced in three different ways (depending of the form of $e_1$ - and $e_2$): - \begin{itemize} - \item If $e_1$ is a value $\λ r. e_0$, then the only possible reduction - is by applying the $\beta$-reduction rule, so the only choice for - $e'$ is $\subst{x}{e_2}{e_0}$ (where $x = \var(r)$). - - Moreover, a case analysis on the different typing rules shows that - the last rule of the derivation of $\Γ \tinfer \λ r . e_0 : t_1$ can - only be the Iabs rule: - \[ - \inferrule{% - x:t_x \vdash r:t_x \\ \Γ; x:t_x \tinfer e_0:s - }{% - \Γ \tinfer \λ r.e_0 : t_x \rightarrow s - } - \] - So $t_1$ has the form $t_x \rightarrow s$. This means that $t_2$ is a - subtype of $t_x = \dom(t_x \rightarrow s)$ and that $t'$ is equal to - $s = (t_x \rightarrow s) \circ t_2$. - - Moreover, as $\Γ; x:t_x \tinfer e_0:s$ and $\Γ \tinfer e_2 : t_2$ - with $t_2 \subtypeG t_x$, the Lemma~\ref{lemma:substitution} allows - us to conclude that $\Γ \tinfer e' : t'$. - \item If $e_1$ is a value $\λ p.e_0$ (with $p$ not in the form $x$ or - $x:t$), and $e_2$ is a value, then we can use the same reasoning. - \item In the other cases, we can reduce either $e_1$, either $e_2$. - - If we reduce $e_1$ to $e'_1$, we get a new expression $e' = - e'_1~e_2$, and $e'_1$ satisfies $\Γ \tinfer e'_1 : t_1$ (by induction - hypothesis). By re-applying the Iapp rule, we get $\Γ \tinfer - e'_1~e_2 : t$, thus $\Γ \tinfer e' : t$. - - The same holds if we reduce $e_2$. - - \end{itemize} - \item[Let] - $\inferrule{% - \Γ; x_1 : \any \tinfer e_1 : t_1\\ - \Γ ; x_1 : t_1 \tinfer e_2 : t - }{% - \Γ \tinfer \text{let } e_1 = x_1 \text{ in } e_2 : t - }$ - - The expression $e$ has the form ``let $e_1 = x_1$ in $e_2$''. - It reduces (and may only reduce to) $e' = \subst{x_1}{e_1}{e_2}$. - By applying the substitiution lemma, we can deduce that $e'$ has type - $t$. - \item[LetAnnot] - The subject reduction property do not hold for the \textbf{LetAnnot} - case for now.~\todo{Make this hold} - \item[ITcase] - $\inferrule{% - \Γ \tinfer e_0 : t_0 \\ - t_0 \not\subtype s \Rightarrow \Γ; x : t_0 \wedge \lnot s \tinfer e_2 : t_2 \\ - t_0 \not\subtype \lnot s \Rightarrow \Γ; x : t_0 \wedge s \tinfer e_1 : t_1 \\ - }{% - \Γ \tinfer (x = e_0 \in s) ? e_1 : e_2 : t_1 \vee t_2 - }$ - - If $e_0$ is not a value, then the only possible reduction for $e$ is to - reduce it to an expression $e'_0$ which will have a type $t'_0 \subtype - t_0$ under the context $\Γ$ (by induction hypothesis). - By re-applying the \textbf{ITcase} rule, we obtain a new type $t'$ for - the expression $(x = e'_0 \in s) ? e_1 : e_2$, which is a subtype of - $t$. - - If $e_0$ is a value $v$, then the only possible reductions are if - $\tinfer v : s$ or $\tinfer v : \lnot s$\todo{Current typing rules - do not allow asserting that this is always true, which will b a deal - broker for Progress, see~\cite{Fri08} for a way to enforce this}. - - Assume the first one. The expression $e$ then reduces to - $\subst{x}{v}{e_1}$, and (by application of the substitution Lemma), we - know that $\Γ \tinfer \subst{x}{v}{e_1} : t_1$. As $t_1 \subtype t$ - (because $t = t_1 \vee t_2$), we get the expected result. - - By symmetry, this also holds if $\tinfer v : \lnot s$. - \end{description} -\end{proof} - -\begin{theorem}[Subject reduction $\Downarrow$]\label{thm:subj-reduction-check} - For any pair $e, e'$ of terms (of nix-light), if $\Γ \tcheck e : t$ and $e - \rightarrow e'$, then $\Γ \tcheck e' : t$. -\end{theorem} - -\begin{proof} - The proof is similar to the one of~\autoref{thm:subj-reduction-infer}. -\end{proof} diff --git a/soundness/oracle.tex b/soundness/oracle.tex new file mode 100644 index 0000000..5b574ae --- /dev/null +++ b/soundness/oracle.tex @@ -0,0 +1,63 @@ +The type-system is defined in~\autoref{fig::oracle-type-system}. + +\begin{figure} + \begin{mathpar} + \and\inferrule{ \Γ(x) \subtype t }{\Γ; \toracle x:t}(OVar) + + \and\inferrule{ \Bt(c) \subtype t }{\Γ \toracle c:t}(OConst) + + \and\inferrule{% + \Γ \toracle e_2 : s \\ + \Γ \toracle e_1 : s \rightarrow t + }{% + \Γ \toracle e_1~e_2 : t + } + (OApp) + + \and\inferrule{% + t \subtype \zero \rightarrow \one \\ + \forall s_1 \rightarrow s_2 \in \A(t), \\ + \Γ' \dashv p:s_1 \\ \Γ;\Γ' \toracle e : s_2 + }{% + \Γ \toracle \λ p.e : t + }(OAbs) + + \and + \inferrule{% + \forall i \in \discrete{1}{n}, + \Γ; x_1 : t_i \toracle e_i : t_i \\ + \Γ; x_1 : t_1 \toracle e : t + }{% + \Gamma \toracle \text{let } x_1 = e_1 \text{ in } e : t + } + (OLet) + + \and + \inferrule{% + \forall i \in \discrete{1}{n}, + \Γ; x_1 : t_1; \ldots; x_n : t_n \toracle e_i : t_i \\ + \Γ; x_1 : t_1; \cdots; x_n : t_n \toracle e : t + }{% + \Gamma \toracle \text{let } x_1 : t_1 = e_1; \ldots{}; x_n : t_n = e_n + \text{ in } e : t + } + (OLetAnnot) + + \and\inferrule{% + \Γ \toracle e : t \\ + t \not\subtype t \Rightarrow \Γ; x : t \wedge \lnot t \toracle e_2 : s \\ + t \not\subtype \lnot t \Rightarrow \Γ; x : t \wedge t \toracle e_1 : s \\ + }{% + \Γ \toracle (x = e \in t) ? e_1 : e_2 : s + }(OTcase) + + \and\inferrule{% + \Γ \toracle e_1 : t_1 \\ \Γ \toracle e_2 : t_2 \\ + t_2 \subtype \cons(\any, \any) \\ + \cons(t_1, t_2) \subtype t + }{% + \Γ \toracle \cons(e_1, e_2) : t + }(OCons) + \end{mathpar} + \caption{The oracle type-system}\label{fig::oracle-type-system} +\end{figure}