Define the "oracle" type-system

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}
 {%

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}
 

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.

soundness/main.tex

@@ -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}

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}