[Git][monnier/typer][report/itd] 4 commits: - - Typer

17 Oct 2018


      Stefan pushed to branch report/itd at Stefan / Typer
Commits:
e3610e71 by Stefan Monnier at 2018-10-16T22:38:26Z
-
- - - - -
4352b262 by Stefan Monnier at 2018-10-17T03:01:10Z
-
- - - - -
1b81f9ff by Stefan Monnier at 2018-10-17T03:01:11Z
Merge branch &#39;report/itd&#39; of gitlab.com:/monnier/typer into report/itd
- - - - -
af536d42 by Stefan Monnier at 2018-10-17T05:07:57Z
-
- - - - -
1 changed file:
- paper.tex
Changes:
=====================================
paper.tex
=====================================
@@ -63,6 +63,7 @@
 \newcommand \id[1] {\textsl{#1}}
 \newcommand \kw[1] {\textsf{#1}}
 \newcommand \Subst[3] {#1[#2/#3]}
+\newcommand \Comment[1] {}
\newcommand \FIXME[1] {\fbox{\parbox{\columnwidth}{{\color{red}{¡FIXME!}} #1}}}
@@ -242,7 +243,46 @@ The contributions of this article are:
\section{Background}
-In this section, we briefly present the two problems our design aims to address.
+\newcommand \Tind[3] {\kw{Ind}(#1:#2)\langle#3\rangle}
+\newcommand \Tcon[2] {\kw{Con}(#1,#2)}
+\newcommand \TIcase[4] {{<}#1{>}\kw{Case}~#2%% :#3
+  ~\kw{of}~\langle#4\rangle}
+\newcommand \Tfix[3] {\kw{Fix}_{#1}~#2:#3~=~}
+
+In this section, we briefly present the two problems our design aims
+to address.  A common way to add inductive types to a language is to extend
+it as follows (mostly taken from~\citet{Gimenez94}):
+\begin{displaymath}
+  \begin{array}{lc@{;;}c@{;;}l}
+    \textsl{(index)} & i &\in& \mathbb{N} \
+    \textsl{(term)} & e,b,c,\tau &::=&
+        ... ~\MAlign{
+      |~ \Tind{x}{\tau}{\vec c} \
+      |~ \Tcon{i}{e} \
+      |~ \TIcase{\tau_r}{e}{\tau_e}{\vec b} \
+      |~ \Tfix{i}{x}{\tau}{e}
+    } \
+  \end{array}
+\end{displaymath}
+Where $\Tind{x}{\tau}{\vec c}$ is the type constructor where ${\vec c}$ holds
+the type of each possible constructor, $\Tcon{i}{e}$ is the value constructor
+for the $i^{th}$ constructor of the inductive type $e$, \kw{Case} is the
+eliminator and \kw{Fix} allows the definition of functions that perform
+structural recursion on those inductive data types.
+The $\Tind{x}{\tau}{\vec c}$ constructor is neat combination of recursive type,
+sum type, tuple type, and indexed type families.
+
+The main shortcoming of that presentation, for our use, is that \kw{Case} is
+the only eliminator and is a large construct whose naive run-time complexity
+is proportional to the number of fields of $e$.  While it is often perfectly
+adequate, it is impractical when selecting a single field from a large
+tuple, such as a tuple holding all the functions exported from a module.
+For this reason, we want to introduce tuples separately from
+inductive types.
+
+To do that, we will deconstruct inductive types into their constituting
+elements: recursive types, sum types, tuple types, and indexed
+type families.
\subsection{Native tuples}
@@ -349,11 +389,11 @@ it practical to provide this feature even if it is not used very often.
 \begin{figure}
   \begin{displaymath}
     \begin{array}{lc@{;;}c@{;;}l}
-      \textit{(var)} & x,y,t &\in& \mathcal{V} \
-      \textit{(level)} & \ell &\in& \mathbb{N} \
-      \textit{(ctxt)} & \Gamma,\Delta &::=& \EmptyCtx ~|~ \Gamma,x:\tau \
-      \textit{(sort)} & s &::=& \Type \ell \
-      \textit{(term)} & e,\tau &::=& s ~|~ x ~|~ \Tlam x \tau e ~|~ \Tapp{e_1}{e_2}
+      \textsl{(var)} & x,y,t &\in& \mathcal{V} \
+      \textsl{(level)} & \ell &\in& \mathbb{N} \
+      \textsl{(ctxt)} & \Gamma,\Delta &::=& \EmptyCtx ~|~ \Gamma,x:\tau \
+      \textsl{(sort)} & s &::=& \Type \ell \
+      \textsl{(term)} & e,\tau &::=& s ~|~ x ~|~ \Tlam x \tau e ~|~ \Tapp{e_1}{e_2}
       ~|~ \Tarw x {\tau_1} {\tau_2}
     \end{array}
   \end{displaymath}
@@ -411,240 +451,251 @@ Figure~\ref{fig:ccw} shows our base language \CCw{} as a pure type system
 à la ECC~\cite{Luo89}.
While inductive types have non-trivial interactions with impredicativity,
-they are largely orthogonal to our work, so contrary to most other
-presentations, we did not include an impredicative universe at the bottom in
-order to keep the presentation simpler.
-
-\newpage
-\section{Dependent pairs}
-
-\newcommand \TPair[2] {\Sigma#1:#2.}
-\newcommand \Tpair[2] {\langle#1,#2\rangle}
-
-\begin{figure}
-  \begin{mathpar}
-    \Infer[P-form]
-          {\Jtyper {\tau_1}{\Type {\ell_1}} \
-           \Jtyper[\Gamma,x:\tau_1]{\tau_2}{\Type {\ell_2}}}
-          {\Jtyper{\TPair x {\tau_1}{\tau_2}}{\Type {(\Tmax{\ell_1}{\ell_2})}}}
-
-    \Infer[P-intro]
-          {\Jtyper{e_1}{\tau_1} \
-           \Jtyper{e_2}{\tau_2[e_1/x]}}
-          {\Jtyper{\Tpair{e_1}{e_2}}{\TPair x {\tau_1}{\tau_2}}}
-
-    \Infer[P-proj$_1$]
-          {\Jtyper{e}{\TPair x {\tau_1}{\tau_2}}}
-          {\Jtyper{\Tproj e 1}{\tau_1}}
-
-    \Infer[P-proj$_2$]
-          {\Jtyper{e}{\TPair x {\tau_1}{\tau_2}}}
-          {\Jtyper{\Tproj e 2}{\tau_2[\Tproj e 1/x]}}
-\end{mathpar}
-  \caption{Dependent pairs}
-  \label{fig:pairs}
-\end{figure}
-
-Fig.~\ref{fig:pairs} shows the usual typing rules for dependent pairs.
-
-\FIXME{Does this interact with impredicativity?}
-\FIXME{Can we use the impredicative encoding and avoid adding it to
-       the language!  I think not!}
-
-\newpage
-\section{Tagged sums}
-
-\newcommand \TSum[1] {#1~{+}~}
-\newcommand \TSinj[1][\Ttagvar] {\kw{inj}_{#1}}
-\newcommand \TScase[5] {\kw{case}~#1~|~\TSinj[1]{#2}\Rightarrow#3~|~\TSinj[2]{#4}\Rightarrow#5}
-
-\begin{figure}
-  \begin{mathpar}
-    \Infer[S-form]
-          {\Jtyper {\tau_1} {\Type {\ell_1}} \
-           \Jtyper {\tau_2} {\Type {\ell_2}}}
-          {\Jtyper {\TSum{\tau_1}{\tau_2}}
-           {\Type{(\Tmax{\ell_1}{\ell_2})}}}
-    \
-
-    \Infer[S-intro$_1$]
-          {\Jtyper e {\tau_1}}
-          {\Jtyper {\TSinj[1] e} {\TSum{\tau_1}{\tau_2}}}
-
-    \Infer[S-intro$_2$]
-          {\Jtyper e {\tau_2}}
-          {\Jtyper {\TSinj[2] e} {\TSum{\tau_1}{\tau_2}}}
-
-    \Infer[S-elim]
-          {\Jtyper e {\TSum{\tau_1}{\tau_2}} \
-           \Jtyper[\Gamma,x_1:\tau_1]{e_1}\tau \
-           \Jtyper[\Gamma,x_2:\tau_2]{e_2}\tau}
-          {\Jtyper {\TScase e{x_1}{e_1}{x_2}{e_2}} \tau}
-  \end{mathpar}
-  \caption{Tagged sums}
-  \label{fig:sums}
-\end{figure}
+those interactions are largely orthogonal to our work, so contrary to most
+other presentations, we did not include an impredicative universe at the
+bottom: our calculus is fully predicative, which simplifies several parts of
+the presentation.
+
+We will use this same base calculus for both the reference calculus of
+inductive constructions as well as our calculus of united constructions
+which we present in the next few sections in the form of a collection of
+extensions.
+
+\Comment{
+  \newpage
+  \section{Dependent pairs}
+
+  \newcommand \TPair[2] {\Sigma#1:#2.}
+  \newcommand \Tpair[2] {\langle#1,#2\rangle}
+
+  \begin{figure}
+    \begin{mathpar}
+      \Infer[P-form]
+            {\Jtyper {\tau_1}{\Type {\ell_1}} \
+             \Jtyper[\Gamma,x:\tau_1]{\tau_2}{\Type {\ell_2}}}
+            {\Jtyper{\TPair x {\tau_1}{\tau_2}}{\Type {(\Tmax{\ell_1}{\ell_2})}}}
+
+      \Infer[P-intro]
+            {\Jtyper{e_1}{\tau_1} \
+             \Jtyper{e_2}{\tau_2[e_1/x]}}
+            {\Jtyper{\Tpair{e_1}{e_2}}{\TPair x {\tau_1}{\tau_2}}}
+
+      \Infer[P-proj$_1$]
+            {\Jtyper{e}{\TPair x {\tau_1}{\tau_2}}}
+            {\Jtyper{\Tproj e 1}{\tau_1}}
+
+      \Infer[P-proj$_2$]
+            {\Jtyper{e}{\TPair x {\tau_1}{\tau_2}}}
+            {\Jtyper{\Tproj e 2}{\tau_2[\Tproj e 1/x]}}
+    \end{mathpar}
+    \caption{Dependent pairs}
+    \label{fig:pairs}
+  \end{figure}
+
+  Fig.~\ref{fig:pairs} shows the usual typing rules for dependent pairs.
+
+  \FIXME{Does this interact with impredicativity?}
+  \FIXME{Can we use the impredicative encoding and avoid adding it to
+         the language!  I think not!}
+}
-Fig.~\ref{fig:sums} shows the usual typing rules for tagged sums.
+\Comment{
+  \newpage
+  \section{Tagged sums}
+
+  \newcommand \TSum[1] {#1~{+}~}
+  \newcommand \TSinj[1][\Ttagvar] {\kw{inj}_{#1}}
+  \newcommand \TScase[5] {\kw{case}~#1~|~\TSinj[1]{#2}\Rightarrow#3~|~\TSinj[2]{#4}\Rightarrow#5}
+
+  \begin{figure}
+    \begin{mathpar}
+      \Infer[S-form]
+            {\Jtyper {\tau_1} {\Type {\ell_1}} \
+             \Jtyper {\tau_2} {\Type {\ell_2}}}
+            {\Jtyper {\TSum{\tau_1}{\tau_2}}
+             {\Type{(\Tmax{\ell_1}{\ell_2})}}}
+      \
+
+      \Infer[S-intro$_1$]
+            {\Jtyper e {\tau_1}}
+            {\Jtyper {\TSinj[1] e} {\TSum{\tau_1}{\tau_2}}}
+
+      \Infer[S-intro$_2$]
+            {\Jtyper e {\tau_2}}
+            {\Jtyper {\TSinj[2] e} {\TSum{\tau_1}{\tau_2}}}
+
+      \Infer[S-elim]
+            {\Jtyper e {\TSum{\tau_1}{\tau_2}} \
+             \Jtyper[\Gamma,x_1:\tau_1]{e_1}\tau \
+             \Jtyper[\Gamma,x_2:\tau_2]{e_2}\tau}
+            {\Jtyper {\TScase e{x_1}{e_1}{x_2}{e_2}} \tau}
+    \end{mathpar}
+    \caption{Tagged sums}
+    \label{fig:sums}
+  \end{figure}
+
+  Fig.~\ref{fig:sums} shows the usual typing rules for tagged sums.
+}
-\newpage
+%% \newpage
 \section{Tuples}
-\newcommand \Tuple[2][\Ttagvar] {\kw{Tuple}~{#1}~#2}
-\newcommand \tuple[2][\Ttagvar] {\kw{tuple}_{#1}^{#2}}
+\newcommand \Tuple[2][\Ttagvar] {\kw{Tuple}_{#1}~#2}
+\newcommand \tuple[2][\Ttagvar] {\kw{tuple}_{#1}~{#2}~}
 \newcommand \TLabel {\id{Label}}
-\newcommand \Tsel {\pi}
+%% \newcommand \Tsel {\pi}
\begin{figure}
-  \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}
+  %% \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}_\ell~\tau~f) = \tau \
+  %%     \id{Tnth}~x~(s~n)~i~(\id{Tcons}_\ell~\tau~f) = \
+  %%     ;;;;
+  %%     \id{Tnth}~x~n~(s~i)~(f~(\id{nth}~i~x))
+  %%   }
+  %% \end{displaymath}
\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 \tau}}
-          {\Jtyper{\Tproj e i}{\tau_i[{\Tproj e 0,..,\Tproj e {i!-!1}}/x_0,..,x_{i!-!1}]}}
+    \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-field]
+          {|\vec e| = 0}
+          {\Jtyper {\vec e} {\EmptyCtx}}
+
+    \Infer%% [TC-field]
+          {\Jtyper {\vec e} {\Delta} \
+           \Jtyper {e_i} {\tau_i[{\vec e}/\Delta]}}
+          {\Jtyper {\vec e, e_i} {\Delta, x:\tau_i}}
+
+    \Infer{\Jtyper {\vec e} {\Delta}}
+          {\Jtyper {\tuple \Delta {\vec e}} {\Tuple \Delta}}
+
+    \Infer%% [T-proj]
+        {\Jtyper{e}{\Tuple \Delta} \
+         \Delta = x_0:\tau_0,..,x_n:\tau_n \
+         n \ge i}
+        {\Jtyper{\Tproj e i}{\tau_i[{\Tproj e 0,..,\Tproj e {i!-!1}}/x_0,..,x_{i!-!1}]}}
   \end{mathpar}
   \caption{Tuples}
   \label{fig:tuples}
 \end{figure}
-Fig.~\ref{fig:tuples} shows the typing rules for tagged tuples.
-
-\newpage
-\section{Tagged terms}
-
-\newcommand \TTag[1][\Ttagvar] {\kw{Tag}_{#1}~}
-\newcommand \Ttag[1][\Ttagvar] {\kw{tag}_{#1}}
-\newcommand \Tuntag {\kw{untag}~}
+At its core, our solution to our design problem is very simple: instead of
+using ``plain'' tuples on one side and tagged sums on the other, as is done
+in SML, we associate the tags (which we call \emph{labels}) with the tuples,
+so that our sums can be reduced to mere (non-disjoint) union types.
+The extra cost of adding a label to every tuple is very minor; more
+specifically in many cases those labels can be stored at no extra cost
+within the metadata needed for memory management purposes.
-\begin{figure}
-
-  \begin{displaymath}
-    \begin{array}{lc@{;;}c@{;;}l}
-      \textit{(label)} & l &\in& \mathcal{L} \
-      \textit{(term)} & e,\tau &::=&
-          ... ~\MAlign{
-        |~ \TTag{\tau}
-        ~|~ \Ttag e
-        ~|~ \Tuntag{e}
-      } \
-    \end{array}
-  \end{displaymath}
+Our language's syntax is extended as follows:
+\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}_\ell & \id{Types}_\ell; \
+  %%   \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}_\ell & \Tsarw{\id{Types}_\ell}{\Type {\ell}}; \
+  %%   \id{Vnil}_\ell & \id{Values}_\ell~{\id{Tnil}_\ell}; \
+  %%   \id{Vcons}_\ell &
+  %%       \MAlign{
+  %%         \Tarw{x}{\tau}{\Tsarw{\id{Values}_\ell~{(f~x)}}{}} \
+  %%         ;; \id{Values}_\ell~{(\id{Tcons}~\tau~f)};
+  %%       } \medskip \
+  %%   \Tuple[]{} & \TLabel \to \id{Types}_\ell \to \Type \ell; \
+  %% \end{array}
+  \begin{array}{lc@{;;}c@{;;}l}
+    \textsl{(label)} & l &\in& \mathcal{L} \
+    \textsl{(term)} & e,\tau &::=&
+        ... ~|~ \Tuple \Delta ~|~ \tuple \Delta {\vec e} ~|~ \Tproj e i
+  \end{array}
+\end{displaymath}
+Where $\Tuple \Delta$ is the type constructor for tuples with label $l$ where $\Delta$
+is the list of (possibly dependent) field types, $\tuple \Delta {\vec e}$ is the
+constructor of actual tuple values, and $\Tproj e i$ is the destructor which
+extracts the value of a given field.  Figure~\ref{fig:tuples} shows the
+typing rules for our labeled tuples.  Reduction rules of the languages are
+extended with the obvious congruence rules as well as the following
+primitive reduction:
+\begin{displaymath}
+  (\tuple \Delta {\vec e}).i ;;\leadsto;; e_i
+\end{displaymath}
-  \begin{mathpar}
-    \Infer%% [N-form]
+The form of our tuple constructor $\tuple \Delta {\vec e}$ was chosen to be
+``saturated'' in the sense that all elements of the tuple have to be
+provided, rather than allowing uses such as $\tuple \Delta$ and letting elements
+be provided in a curried fashion.  This was done for two reasons: first, it
+makes the construct directly correspond to the actual allocation and
+initialization of the heap object, so any extra closures needed for curried
+use have to be made explicit in the code; second it preserves the property
+that any value of arrow type has to be of the form $\lambda x:\tau.e$.
+
+
+\Comment{
+  %% \newpage
+  \section{Tagged terms}
+
+  \newcommand \TTag[1][\Ttagvar] {\kw{Tag}_{#1}~}
+  \newcommand \Ttag[1][\Ttagvar] {\kw{tag}_{#1}}
+  \newcommand \Tuntag {\kw{untag}~}
+
+  \begin{figure}
+
+    \begin{displaymath}
+      \begin{array}{lc@{;;}c@{;;}l}
+        \textsl{(label)} & l &\in& \mathcal{L} \
+        \textsl{(term)} & e,\tau &::=&
+            ... ~\MAlign{
+          |~ \TTag{\tau}
+          ~|~ \Ttag e
+          ~|~ \Tuntag{e}
+        } \
+      \end{array}
+    \end{displaymath}
+
+    \begin{mathpar}
+      \Infer%% [N-form]
           {\Jtyper \tau {\Type \ell}}
           {\Jtyper {\TTag \tau} {\Type \ell}}
-    \Infer%% [N-intro]
+      \Infer%% [N-intro]
           {\Jtyper e \tau}
           {\Jtyper {\Ttag e} {\TTag \tau}}
-    \Infer%% [N-elim]
+      \Infer%% [N-elim]
           {\Jtyper {\Ttag e} {\TTag \tau}}
           {\Jtyper {\Tuntag e} \tau}
-  \end{mathpar}
-  \caption{Tagged terms}
-  \label{fig:tagged-terms}
-\end{figure}
-
-Fig.~\ref{fig:tagged-terms} shows the typing rules for tagged terms.
-
-\newpage
-\section{Equality}
+    \end{mathpar}
+    \caption{Tagged terms}
+    \label{fig:tagged-terms}
+  \end{figure}
-\begin{figure}
-  \begin{displaymath}
-    \begin{array}{l@{;:;}l}
-      \id{Eq} & \Tarw{t}{\Type{}}{\Tarw {x,y} t {\Type{0}}}; \
-      \id{refl} & \Tarw{t}{\Type{}}{\Tarw{x}{t}{\id{Eq}~t~x~x}}; \
-      J & \MAlign{
-        \Tarw{t}{\Type{}}{\Tarw {x,y} t {\Tarw u {\Type{}} {\Tarw
-                              f {\Tsarw t u} {}}}} \
-        \Tsarw{\id{Eq}~t~x~y}{\Tsarw{f~x}{f~y}}
-        ;}
-    \end{array}
-  \end{displaymath}
-
-  \begin{mathpar}
-    \Jstep {J~_~_~_~_~_~(\id{refl}~_~_)~x}x
-  \end{mathpar}
-  %% With impredicativity we could define it as:\hfill\mbox{}
-  %% \begin{displaymath}
-  %%   \begin{array}{l}
-  %%     \id{Eq}~t~x~y = \Tarw u {\Type{}} {\Tarw
-  %%       f {\Tsarw t u} {\Tsarw{f~x}{f~y}}}; \
-  %%     \id{refl}~t~x~=\Tlam u {\Type{}} {\Tlam f {(\Tsarw t u)} {\Tlam v {(f~x)} v}};
-  %%   \end{array}
-  %% \end{displaymath}
-  \caption{Equality type}
-  \label{fig:equality}
-\end{figure}
+  Fig.~\ref{fig:tagged-terms} shows the typing rules for tagged terms.
+}
-\newpage
+%% \newpage
 \section{Unions}
\newcommand \TUnion[1] {#1~\cup~}
 \newcommand \TUnionSmart[1] {#1~\cup'~}
 \newcommand \TUweaken[1] {\id{Sub.weaken}~#1~}
-\newcommand \TUcase[6] {\kw{case}~#1~|~#2~#3~P_{#3}~\Rightarrow #4~|~#5~P_{#5}~\Rightarrow #6}
+\newcommand \TUcase[6] {\kw{switch}~#1~|~#2~#3~P_{#3}~\Rightarrow #4~|~#5~P_{#5}~\Rightarrow #6}
\newcommand \JSplit[3] {#2 \Longleftarrow #1~/\Ttagvar \Longrightarrow #3}
 \newcommand \JOrder[3] {#1;\stackrel\Ttagvar\Longrightarrow;\TUnion{#2}{#3}}
@@ -653,41 +704,14 @@ Fig.~\ref{fig:tagged-terms} shows the typing rules for tagged terms.
\begin{figure}
-  \begin{displaymath}
-    \begin{array}{lc@{;;}c@{;;}l}
-      \textit{(term)} & e,\tau &::=&
-          ... ~\MAlign{
-        |~ \TUnion{\tau_1}{\tau_2} \
-        !FIXME!
-      } \
-    \end{array}
-  \end{displaymath}
-
-  \begin{displaymath}
-    \begin{array}{l@{;:;}l}
-      %% \multicolumn 1 l {_{\subseteq}_ \hfill :} &
-      _{\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};\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
-          \Jsubtype{\TUnion{\tau_1}{\tau_2}}{\tau_3} \
-      \id{Sub.weaken} & \Jsubtype{\tau_1}{\tau_2} \to \tau_1 \to \tau_2 \
-      %%
-    \end{array}
-  \end{displaymath}
-
   \begin{mathpar}
     %% FIXME: Make it return the \Jsubtype proofs!
-    \Infer[U-order1]{ }{\JOrder{\TTag{\tau}}{\TTag{\tau}}{\bot}}
+    \Infer%% [U-order1]
+          { }{\JOrder{\Tuple{\Delta}}{\Tuple{\Delta}}{\bot}}
-    \Infer[U-order2]
+    \Infer%% [U-order2]
           {\Ttagvar' \neq \Ttagvar}
-          {\JOrder{\TTag[\Ttagvar']{\tau}}{\bot}{\TTag{\tau}}}
+          {\JOrder{\Tuple[\Ttagvar']{\Delta}}{\bot}{\Tuple[\Ttagvar']{\Delta}}}
\Infer[U-order-union]
           {\JOrder{\tau_1}{\tau_{\Ttagvar{}1}}{\tau_{d1}} \
@@ -708,9 +732,9 @@ Fig.~\ref{fig:tagged-terms} shows the typing rules for tagged terms.
   \begin{mathpar}
     \Infer[U-elim]
           {\Jtyper e {\tau_u} \
-           \JOrder {\tau_u} {\TTag{\tau_\Ttagvar}} {\tau_d} \
+           \JOrder {\tau_u} {\tau_\Ttagvar} {\tau_d} \
            %% FIXME: Args to TUweaken!
-           \Jtyper[\Gamma,x:{{\TTag{\tau_\Ttagvar}}},P_x:(e \equiv \TUweaken{?}{x})]
+           \Jtyper[\Gamma,x:{{\tau_\Ttagvar}},P_x:(e \equiv \TUweaken{?}{x})]
                   {e_\Ttagvar} \tau \
            \Jtyper[\Gamma,y:{\tau_d},P_y:(e \equiv \TUweaken{?}{y})] {e_d} \tau}
           {\Jtyper {\TUcase e {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d}} \tau}
@@ -720,6 +744,58 @@ Fig.~\ref{fig:tagged-terms} shows the typing rules for tagged terms.
   \label{fig:unions}
 \end{figure}
+Since our tuples carry labels, our sum types do not need to carry any labels
+and we can hence use union types for them.  We do not need to extend the
+syntax of our language for that, instead we add the following axioms to the
+initial environment:
+%%
+\begin{displaymath}
+  \begin{array}{l@{;:;}l}
+    %% \multicolumn 1 l {_{\subseteq}_ \hfill :} &
+    _\cup_ & \Type{\ell_1}\to\Type{\ell_2}\to\Type{\Tmax{\ell_1}{\ell_2}} \
+    _{\subseteq}_ & \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};\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
+        \Jsubtype{\TUnion{\tau_1}{\tau_2}}{\tau_3} \
+    \id{Sub.weaken} & \Jsubtype{\tau_1}{\tau_2} \to \tau_1 \to \tau_2 \
+    %%
+  \end{array}
+\end{displaymath}
+These declarations define the new union $\cup$ type as well as a new subtype
+type $\subseteq$.  Then come four constructors that allow constructing proofs of
+subtyping between union types, and finally the \id{Sub.weaken} operation
+which should be read as a form of casting from a subtype to a supertype.
+
+Note that we are cheating a bit here: not only those declarations use
+a shorthand notation eliding some arguments that can be inferred, but they
+rely on some form of universe polymorphism, so they should be read
+a declaration schemas, which need to be freshly instantiated for each use.
+
+After casting our subtypes to their supertype, we need some way to recover
+the lost information.  For that we introduce the following new syntax:
+%%
+\begin{displaymath}
+  \begin{array}{lc@{;;}c@{;;}l}
+    \textsl{(term)} & e,\tau &::=&
+        ... ~\MAlign{
+      |~ {\MAlign{\TUcase {e \} {\Ttagvar}{x}{e_\Ttagvar \}{y}{e_d}}}
+    }
+  \end{array}
+\end{displaymath}
+It is a switch statement, intended to have an run-time complexity comparable
+to that of a C \kw{switch} in the sense that it only checks the labels and
+jumps to a particular branch but does not perform any further extraction
+of data.  Our \kw{switch} statement tests a single label before
+falling through to a default branch, but it can be trivially chained in
+order to select between several possible labels, of course.
+
+%% FIXME: reduction rules?  Especially for the `weaken` thingy!
+
 Fig.~\ref{fig:unions} shows our typing rules for unions.  Our unions are
 unusual in that the subterms that make up the type cannot be arbitrary
 types, to make sure we can apply \kw{case} to them.
@@ -735,8 +811,8 @@ types, to make sure we can apply \kw{case} to them.
 \begin{figure}
   \begin{displaymath}
     \begin{array}{lc@{;;}c@{;;}l}
-      \textit{(index)} & i &\in& \mathbb{N} \
-      \textit{(term)} & e,b,c,\tau &::=&
+      \textsl{(index)} & i &\in& \mathbb{N} \
+      \textsl{(term)} & e,b,c,\tau &::=&
           ... ~\MAlign{
         |~ \Tmu[i]{x}{\tau}{e}
         ~|~ \Tmu{x}{\tau}{e} \
@@ -775,6 +851,37 @@ types, to make sure we can apply \kw{case} to them.
   \label{fig:recurse}
 \end{figure}
+\newpage
+\section{Equality}
+
+\begin{figure}
+  \begin{displaymath}
+    \begin{array}{l@{;:;}l}
+      \id{Eq} & \Tarw{t}{\Type{}}{\Tarw {x,y} t {\Type{0}}}; \
+      \id{refl} & \Tarw{t}{\Type{}}{\Tarw{x}{t}{\id{Eq}~t~x~x}}; \
+      J & \MAlign{
+        \Tarw{t}{\Type{}}{\Tarw {x,y} t {\Tarw u {\Type{}} {\Tarw
+                              f {\Tsarw t u} {}}}} \
+        \Tsarw{\id{Eq}~t~x~y}{\Tsarw{f~x}{f~y}}
+        ;}
+    \end{array}
+  \end{displaymath}
+
+  \begin{mathpar}
+    \Jstep {J~_~_~_~_~_~(\id{refl}~_~_)~x}x
+  \end{mathpar}
+  %% With impredicativity we could define it as:\hfill\mbox{}
+  %% \begin{displaymath}
+  %%   \begin{array}{l}
+  %%     \id{Eq}~t~x~y = \Tarw u {\Type{}} {\Tarw
+  %%       f {\Tsarw t u} {\Tsarw{f~x}{f~y}}}; \
+  %%     \id{refl}~t~x~=\Tlam u {\Type{}} {\Tlam f {(\Tsarw t u)} {\Tlam v {(f~x)} v}};
+  %%   \end{array}
+  %% \end{displaymath}
+  \caption{Equality type}
+  \label{fig:equality}
+\end{figure}
+
 \section{Erasure}
The intention of our calculus is for \kw{weaken} to have no run time cost.
@@ -791,11 +898,11 @@ which is sound and complete.
\subsection{Inductive types}
-\newcommand \Tind[3] {\kw{Ind}(#1:#2)\langle#3\rangle}
-\newcommand \Tcon[2] {\kw{Con}(#1,#2)}
-\newcommand \TIcase[4] {{<}#1{>}\kw{Case}~#2%% :#3
-  ~\kw{of}~\langle#4\rangle}
-\newcommand \Tfix[3] {\kw{Fix}_{#1}~#2:#3~=~}
+%% \newcommand \Tind[3] {\kw{Ind}(#1:#2)\langle#3\rangle}
+%% \newcommand \Tcon[2] {\kw{Con}(#1,#2)}
+%% \newcommand \TIcase[4] {{<}#1{>}\kw{Case}~#2%% :#3
+%%   ~\kw{of}~\langle#4\rangle}
+%% \newcommand \Tfix[3] {\kw{Fix}_{#1}~#2:#3~=~}
\newcommand \JIcon[2][\nu;x] {#1 \vdash #2;;\kw{con}}
 \newcommand \JIpos[2][\nu] {#1 \vdash #2;;\kw{pos}}
@@ -999,8 +1106,8 @@ follows:
 %%
 \begin{displaymath}
   \begin{array}{lc@{;;}c@{;;}l}
-    \textit{(index)} & i &\in& \mathbb{N} \
-    \textit{(term)} & e,b,c,\tau &::=&
+    \textsl{(index)} & i &\in& \mathbb{N} \
+    \textsl{(term)} & e,b,c,\tau &::=&
         ... ~\MAlign{
       |~ \Tind{x}{\tau}{\vec c} \
       |~ \Tcon{i}{e} \
View it on GitLab: https://gitlab.com/monnier/typer/compare/9cc261534bdaa2f33731768f755283f35a3...
-- 
View it on GitLab: https://gitlab.com/monnier/typer/compare/9cc261534bdaa2f33731768f755283f35a3...
You're receiving this email because of your account on gitlab.com.



    