[Git][monnier/typer][report/itd] - - Typer

10 Oct 2018


      Stefan pushed to branch report/itd at Stefan / Typer
Commits:
40e74549 by Stefan Monnier at 2018-10-10T20:15:50Z
-
- - - - -
1 changed file:
- paper.tex
Changes:
=====================================
paper.tex
=====================================
@@ -72,8 +72,6 @@
 \newcommand \Jtyper[2][\Gamma] {#1 \vdash #2~:~}
 \newcommand \Type[1] {\kw{Type}_{#1}}
 \newcommand \Ttagvar {l}
-\newcommand \Tuple[2][\Ttagvar] {\kw{Tuple}_{#1}(#2)}
-\newcommand \tuple[2][\Ttagvar] {\kw{tuple}_{#1}^{#2}}
 \newcommand \Tarw[2] {(#1:#2)\to}
 \newcommand \Tmarw[2] {\overrightarrow{(#1:#2)}\to}
 \newcommand \Tsarw[1] {#1\to}
@@ -239,8 +237,8 @@ The contributions of this article are:
 \item A kind of case-analysis construct where the default branch also gets
   refined type information witnessing in an efficient way precise
   information about the branches already tested.
-\item A proof of equivalence of this language with the Calculus of Inductive
-  Constructions, showing it enjoys the same meta-theoretic properties.
+\item A proof of equivalence of this language with (a predicative version
+  of) the Calculus of Inductive Constructions.
 \end{itemize}
\section{Background}
@@ -492,31 +490,75 @@ Fig.~\ref{fig:sums} shows the usual typing rules for tagged sums.
 \newpage
 \section{Tuples}
-\newcommand \Tcons[2]{#1 \to #2}
+\newcommand \Tuple[2][\Ttagvar] {\kw{Tuple}~{#1}~#2}
+\newcommand \tuple[2][\Ttagvar] {\kw{tuple}_{#1}^{#2}}
+\newcommand \TLabel {\id{Label}}
+\newcommand \Tsel {\pi}
\begin{figure}
-  \begin{mathpar}
-    \Infer[T-base]{ }{\Jtyper {\Tuple \EmptyCtx}{\Type 0}}
-
-    \Infer[T-field]
-          {\Jtyper {\Tuple \Delta}{\Type {\ell_1}} \
-           \Jtyper[\Gamma,\Delta] \tau {\Type {\ell_2}}}
-          {\Jtyper {\Tuple {\Delta,x:\tau}}{\Type {(\Tmax{\ell_1}{\ell_2})}}}
-
-    \Infer[TC-base] { }{\Jtyper \EmptyCtx \EmptyCtx}
-
-    \Infer[TC-field]
-          {\Jtyper {\vec e} {\Delta} \
-           \Jtyper e {\tau_i[{\vec e}/\Delta]}}
-          {\Jtyper {\vec e, e_i} {\Delta, x:\tau_i}}
+  \begin{displaymath}
+    \begin{array}{l@{;:;}l}
+      \TLabel & \Type 0; \
+      %% `Tcons Int Tnil : Types 0` comparable to `cons Int nil : list Type₀`
+      %% `list Int : Type₀` and `list Type₀ : Type₁` so `Types 0 : Type₁`!
+      \id{Types}~\ell & \Type {\ell+1}; \
+      \id{Tnil} & \id{Types}~0; \
+      \id{Tcons} &
+          \MAlign{\Tarw{t}{\Type{\ell_1}}
+                  {\Tsarw{(\Tsarw{t}{\id{Types}~{\ell_2}})}
+                    {}} \
+                  ;;\id{Types}~{(\Tmax{\ell_1}{\ell_2});}} \medskip \
+      \id{Values} & \Tsarw{\id{Types}~\ell}{\Type {\ell}}; \
+      \id{Vnil} & \id{Values}~{\id{Tnil}}; \
+      \id{Vcons} &
+          \MAlign{
+            \Tarw{x}{\tau}{\Tsarw{\id{Values}~{(f~x)}}{}} \
+            ;; \id{Values}~{(\id{Tcons}~\tau~f)};
+          } \medskip \
+      \Tuple[]{} & \TLabel \to \id{Types}~\ell \to \Type \ell; \
+    \end{array}
+  \end{displaymath}
+  
+  \begin{displaymath}
+    %% FIXME: `Tnth` isn't be a function since it's only defined if
+    %% the index is within bounds!
+    \MAlign{
+      %% FIXME: Mutual recursion, yuck!
+      \id{nth} : (n:\id{Nat})\to(x:\tau:\id{Types}~\ell)\to\id{Tnth}~x~n~0~\tau \
+      \id{Tnth}~x~0~i~(\id{Tcons}~\tau~f) = \tau \
+      \id{Tnth}~x~(s~n)~i~(\id{Tcons}~\tau~f) = \
+      ;;;;
+      \id{Tnth}~x~n~(s~i)~(f~(\id{nth}~i~x))
+    }
+  \end{displaymath}
-    \Infer[T-intro]
-          {\Jtyper{\Tuple \Delta}{\Type \ell} \
-           \Jtyper{\vec e}{\Delta}}
-          {\Jtyper{\tuple \Delta (\vec e)} {\Tuple \Delta}}
+  \begin{mathpar}
+    %% \Infer[T-base]{ }{\Jtyper {\Tuple \EmptyCtx}{\Type 0}}
+    %%
+    %% \Infer[T-field]
+    %%       {\Jtyper {\Tuple \Delta}{\Type {\ell_1}} \
+    %%        \Jtyper[\Gamma,\Delta] \tau {\Type {\ell_2}}}
+    %%       {\Jtyper {\Tuple {\Delta,x:\tau}}{\Type {(\Tmax{\ell_1}{\ell_2})}}}
+    %%
+    %% \Infer[TC-base] { }{\Jtyper \EmptyCtx {\id{Tup.Tnil}}}
+
+    %% \Infer[TC-field]
+    %%       {\Jtyper {\vec e} {\Delta} \
+    %%        \Jtyper e {\tau_i[{\vec e}/\Delta]}}
+    %%       {\Jtyper {\vec e, e_i} {\Delta, x:\tau_i}}
+    %% \Infer[TC-field]
+    %%       {\Jtyper {\vec e} {\Delta} \
+    %%        \Jtyper e {\tau_i[{\vec e}/\Delta]}}
+    %%       {\Jtyper {e, \vec e} {\id{Tup.Tcons}~\tau~f}}
+
+    \Infer{\Jtyper{\Ttagvar}{\TLabel} \
+           \Jtyper{\tau}{\id{Types}~\ell} \
+           \Jtyper{\id{Vcons}~e_0~(..(\id{Vcons}~e_n~\id{Vnil})..)}
+           {\id{Values}~\tau}}
+          {\Jtyper{\tuple~\tau~\vec e} {\Tuple \tau}}
\Infer[T-proj]
-          {\Jtyper{e}{\Tuple {x_0:\tau_0,..,x_i:\tau_i,\Delta}}}
+          {\Jtyper{e}{\Tuple \tau}}
           {\Jtyper{\Tproj e i}{\tau_i[{\Tproj e 0,..,\Tproj e {i!-!1}}/x_0,..,x_{i!-!1}]}}
   \end{mathpar}
   \caption{Tuples}
@@ -624,12 +666,12 @@ Fig.~\ref{fig:tagged-terms} shows the typing rules for tagged terms.
   \begin{displaymath}
     \begin{array}{l@{;:;}l}
       %% \multicolumn 1 l {_{\subseteq}_ \hfill :} &
-      _{\subseteq}_ & \Type{\ell_1}\to\Type{\ell_2}\to\Type{\ell_1 \sqcup \ell_2} \
-      _\cup_ & \Type{\ell_1}\to\Type{\ell_2}\to\Type{\ell_1 \sqcup \ell_2} \medskip \
-      \id{Sub.refl} & \Jsubtype \tau \tau \
-      \id{Sub.left} &
+      _{\subseteq}_ & \Type{\ell_1}\to\Type{\ell_2}\to\Type{\Tmax{\ell_1}{\ell_2}} \
+      _\cup_ & \Type{\ell_1}\to\Type{\ell_2}\to\Type{\Tmax{\ell_1}{\ell_2}} \medskip \
+      \id{Sub.refl};\tau & \Jsubtype \tau \tau \
+      \id{Sub.left};\tau_3 &
           \Jsubtype{\tau_1}{\tau_2} \to \Jsubtype{\tau_1}{\TUnion{\tau_2}{\tau_3}} \
-      \id{Sub.right} &
+      \id{Sub.right};\tau_3 &
           \Jsubtype{\tau_1}{\tau_2} \to \Jsubtype{\tau_1}{\TUnion{\tau_3}{\tau_2}} \
       \id{Sub.both} &
           \Jsubtype{\tau_1}{\tau_3} \to \Jsubtype{\tau_2}{\tau_3} \to
@@ -1046,6 +1088,8 @@ $\Ftocic \bot = \bot$.
 \subsection{CIC to CUC}
\newcommand \TIeither[2] {\id{Either}~#1~#2}
+\newcommand \TIPair {\Sigma}
+\newcommand \TIpair {\id{dcons}}
\begin{figure}
   \begin{displaymath}
@@ -1056,8 +1100,14 @@ $\Ftocic \bot = \bot$.
       \Ftocuc {\Tarw{x}{\tau_1}{\tau_2}} & \Tarw{x}{\Ftocuc {\tau_1}}{\Ftocuc {\tau_2}} \
       \Ftocuc {\TUnion{\tau_1}{\tau_2}} & \TIeither{\Ftocuc {\tau_1}}{\Ftocuc {\tau_2}} \
       \Ftocuc {\Jsubtype{\tau_1}{\tau_2}} & \Tsarw{\Ftocuc {\tau_1}}{\Ftocuc {\tau_2}} \
-      \Ftocuc {\id{Sub.refl}{e}} & \Tapp{\Ftocuc {P}}{\Ftocuc {e}} \
+      %% \Ftocuc {\id{Sub.refl}{e}} &  \
       \Ftocuc {\TUweaken{P}{e}} & \Tapp{\Ftocuc {P}}{\Ftocuc {e}} \
+      \Ftocuc {\id{Tup.Types}~\ell} & \Type~\ell \
+      \Ftocuc {\id{Tup.Tnil}} & \id{True} \
+      \Ftocuc {\id{Tup.Tcons}} & \TIPair \
+      \Ftocuc {\id{Tup.Values}} & \Tlam{x}{\Type \ell}{x} \
+      \Ftocuc {\id{Tup.Vnil}} & I \
+      \Ftocuc {\id{Tup.Vcons}} & \TIpair \
     \end{array}
   \end{displaymath}
   Inductive types get turned into tuples, tags, explicit equality proofs,
View it on GitLab: https://gitlab.com/monnier/typer/commit/40e745495eace8f3ec3ef4dc31d5ec90b77f...
-- 
View it on GitLab: https://gitlab.com/monnier/typer/commit/40e745495eace8f3ec3ef4dc31d5ec90b77f...
You're receiving this email because of your account on gitlab.com.



    