Stefan pushed to branch report/itd at Stefan / Typer

Commits: 656f7ed7 by Stefan Monnier at 2018-11-07T22:02:41Z -

- - - - -

2 changed files:

- GNUmakefile - paper.tex

Changes:

===================================== GNUmakefile ===================================== @@ -8,5 +8,4 @@ ${LOCALREFS}: ${PAPER}.aux ${GLOBALREFS}.bib @sed 's|^\bibdata{.*}|\bibdata{${GLOBALREFS}}|' <${PAPER}.aux >${PAPER}.tmp.aux bibexport -o $@ ${PAPER}.tmp.aux @rm -f ${PAPER}.tmp.aux $@-save-[1-9]* - - + bibtex ${PAPER}

===================================== paper.tex ===================================== @@ -1,4 +1,4 @@ -\documentclass[sigplan,10pt,review]{llncs} +\documentclass[sigplan,10pt,orivec,review]{llncs} %% \settopmatter{printfolios=true,printccs=false,printacmref=false} %% For double-blind review submission, w/ CCS and ACM Reference %% \documentclass[acmsmall,review,anonymous]{acmart} @@ -54,7 +54,9 @@ \usepackage{parskip} \usepackage{fancybox} %For \ovalbox

+\DeclareUnicodeCharacter{03B1}{\ensuremath{\alpha}} \DeclareUnicodeCharacter{2203}{\ensuremath{\exists}} +\DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}}

%% The doc says `vcenter` should work, but I get an error :-( %% \newcommand \Infer[1][] [\inferrule*[vcenter,right=#1]] @@ -85,6 +87,9 @@ \newcommand \Tproj[1] {#1.} \newcommand \Tmax[1] {#1~\sqcup~}

+%% Apparently llncs redefines \vec to use bold instead of an arrow! +%% \renewcommand \vec \overrightarrow + \newcommand \Tif[2] {\kw{if}~#1~\kw{then}~#2~\kw{else}~}

\newcommand \Jcuc[2][\Gamma] {#1 \vdash_U #2 :} @@ -569,6 +574,7 @@ reduction rule for CUC resp.~CIC.

\newcommand \Tuple[2][\Ttagvar] {\kw{Tuple}_{#1}~#2} \newcommand \tuple[2][\Ttagvar] {\kw{tuple}_{#1}~{#2}~} +%% \newcommand \tuple[3][\Ttagvar] {{ #3 : #2 }_{#1}} \newcommand \TLabel {\id{Label}} %% \newcommand \Tsel {\pi}

@@ -667,14 +673,16 @@ primitive reduction:

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: most -importantly, 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$. This second point turned out to be unimportant: not only we do not -make use of this property, but later parts of our system break it anyway. +provided, rather than providing a tuple constructor which only takes the $\Delta$ +argument and then receives the tuple elements in a curried fashion, as is +done for example in CIC's inductive constructors and in Haskell's datatype +constructors. This was done for two reasons: most importantly, 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$. This second point turned +out to be unimportant: not only we do not make use of this property, but +later parts of our system break it anyway.

\Comment{ @@ -747,7 +755,7 @@ environment: \id{Eq} is the type constructor for this new equality type; \id{refl} is the corresponding value constructor, and $J$ its eliminator which encodes the Leibniz equality. In the rest of this article instead of writing -$\id{Eq}~\tau~x~y$ we will write $x \equiv y$ since $\tau$ can always be inferred +$\id{Eq}~\tau~x~y$ we will often write $x \equiv y$ since $\tau$ can always be inferred from context.

Note that we are cheating a bit in those declarations: @@ -769,63 +777,86 @@ we could not define, we can now define also all the other single-constructor inductive types by adding appropriate fields holding proofs of the needed type equalities.

+For example, in a language with indexed inductive types, we can define the +traditional length-indexed list type as follows: +\begin{verbatim} + type NList (α : Type) : Nat -> Type + | nil : NList α 0 + | cons : α -> NList α l -> NList α (S l); +\end{verbatim} +In the absence of indexed inductive types this can be easily replaced by the +following definition which uses explicit equality witnesses instead of +indices: +\begin{verbatim} + type NList (α : Type) (l : Nat) : Type + | nil : (l ≡ 0) -> NList α l + | cons : α -> NList α l' -> (l ≡ S l') -> NList α l; +\end{verbatim} +The absence of indexed types also has the benefit that case analysis does +not need to make special allowances to support \emph{type refinement}: +the explicit equality witnesses can be used to get the same effect. + +%% \newpage +\subsection{Unions} + \newcommand \TUnion[1] {#1~\cup~} \newcommand \TUnionSmart[1] {#1~\cup'~} -\newcommand \TUweaken[2] {\kw{weaken}~#1{\subseteq}#2~} +%% Note: The first arg is not needed for type-checking, but it is +%% needed for the reduction rules (so a cast from \tau to \tau can be dropped). +\newcommand \TUcast[2] {\kw{cast}~#1{\subseteq}#2~} \newcommand \TUcase[8][\tau_r] { - \langle#1\rangle\kw{switch}~#2:#3~|~#4~#5~P_{#5}~\Rightarrow #6~|~#7~P_{#7}~\Rightarrow #8} + \kw{switch}~#2~|~#4~#5~P_{#5}~\Rightarrow #6~|~#7~P_{#7}~\Rightarrow #8}

\newcommand \JSplit[3] {#2 \Longleftarrow #1~/\Ttagvar \Longrightarrow #3} \newcommand \JOrder[3] {#1;\stackrel\Ttagvar\Longrightarrow;\TUnion{#2}{#3}}

\newcommand \Jsubtype [1] {#1~\subseteq~}

-\begin{figure} +\begin{figure}[bt] \begin{mathpar} \Infer{\Jcuc {\tau_1}{\Type{\ell_1}} \ \Jcuc {\tau_1}{\Type{\ell_1}}} {\Jcuc {\TUnion{\tau_1}{\tau_2}}{\Type{\Tmax{\ell_1}{\ell_2}}}}

- \Infer{\Jcuc {\tau_1}{s_1} \ - \Jcuc {\tau_2}{s_2} \ - \Jcuc {e}{\tau_1} \ - \Jsubtype {\tau_1}{\tau_2}} - {\Jcuc {\TUweaken{\tau_1}{\tau_2}e}{\tau_2}} + \Infer{%% \Jcuc {\tau_1}{s_1} \ + \Jcuc {\tau}{s} \ + \Jcuc {e}{\tau_e} \ + \Jsubtype {\tau_e}{\tau}} + {\Jcuc {\TUcast{\tau_e}{\tau}e}{\tau}}

- \Infer{\JOrder {\tau_e} {\tau_\Ttagvar} {\tau_d} \ + \Infer{\Jcuc e {\tau_e} \ + \JOrder {\tau_e} {\tau_\Ttagvar} {\tau_d} \ {\tau_\Ttagvar} \not= \bot \ {\tau_d} \not= \bot \\ - \Jcuc {\tau_e}{s} \ - \Jcuc {\tau_r}{s} \ - \Jcuc e {\tau_e} \\ + %% \Jcuc {\tau_e}{s} \ + %% \Jcuc {\tau_r}{s} \ %% \tau_e = \TUnion{_}{_} \\ - \Jcuc[\Gamma,x:{{\tau_\Ttagvar}},P_x:(e \equiv \TUweaken{\tau_l}{\tau_e}{x})] + \Jcuc[\Gamma,x:{{\tau_\Ttagvar}},P_x:(e \equiv \TUcast{\tau_l}{\tau_e}{x})] {e_\Ttagvar} {\tau_r} \ - \Jcuc[\Gamma,y:{\tau_d},P_y:(e \equiv \TUweaken{\tau_d}{\tau_e}{y})] + \Jcuc[\Gamma,y:{\tau_d},P_y:(e \equiv \TUcast{\tau_d}{\tau_e}{y})] {e_d} {\tau_r}} {\Jcuc {\TUcase e {\tau_e} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d}} {\tau_r}} \end{mathpar} - %% \caption{Typing rules for union types} - %% \label{fig:unions} - %% \end{figure} + \caption{Typing rules for union types} + \label{fig:unions} +\end{figure}

+\begin{figure}[bt] %% \begin{figure} \begin{mathpar} \ovalbox{\ensuremath{ - \begin{array}[b]{l|l} + \begin{array}[b]{l@{~}|@{~}l} \JOrder{\tau}{\tau_{\Ttagvar}}{\tau_{d}} & - \text{split $\tau$ according to $l$} \ + \text{Split $\tau$ according to $l$} \ \TUnionSmart{\tau_1}{\tau_2} & - \text{like $\cup$ but eliminating $\bot$} \ - \Jsubtype{\tau_1}{\tau_2} & \text{ $\tau_1$ is a subtype of $\tau_2$} + \text{Like $\cup$ but eliminating $\bot$} \ + \Jsubtype{\tau_1}{\tau_2} & \text{$\tau_1$ is a subtype of $\tau_2$} \end{array} - }} \vspace{-15pt} \hfill \\ + }} %% \vspace{-15pt} + \hfill %% \\ \Infer%% [U-order1] - { }{\JOrder{\Tuple{\Delta}}{\Tuple{\Delta}}{\bot}} - - \Infer%% [U-order2] - {\Ttagvar' \neq \Ttagvar} - {\JOrder{\Tuple[\Ttagvar']{\Delta}}{\bot}{\Tuple[\Ttagvar']{\Delta}}} + { }{\JOrder{\Tuple{\Delta}}{\Tuple{\Delta}}{\bot}} + \hfill

\Infer%% [U-order-union] {\JOrder{\tau_1}{\tau_{\Ttagvar{}1}}{\tau_{d1}} \ @@ -833,6 +864,10 @@ type equalities. {\JOrder{\TUnion{\tau_1}{\tau_2}} {(\TUnionSmart{\tau_{\Ttagvar{}1}}{\tau_{\Ttagvar{}2}})} {(\TUnionSmart{\tau_{d1}}{\tau_{d2}})}} + + \Infer%% [U-order2] + {\Ttagvar' \neq \Ttagvar} + {\JOrder{\Tuple[\Ttagvar']{\Delta}}{\bot}{\Tuple[\Ttagvar']{\Delta}}} \end{mathpar}

\begin{mathpar} @@ -855,35 +890,38 @@ type equalities. \Infer{\Jsubtype {\tau_1}{\tau_3} \ {\Jsubtype {\tau_2}{\tau_3}}} {\Jsubtype {\TUnion{\tau_1}{\tau_2}}{\tau_3}} \end{mathpar} - - \caption{Typing rules for union types} - \label{fig:unions} + + \caption{Auxiliary rules for union types} + \label{fig:unions-aux} \end{figure}

-\begin{figure*} +\begin{figure*}[bt] \begin{mathpar} %% \begin{array}{r@{;;\leadsto;;}l} - \JUstep{\TUweaken{_}{\tau_2}{(\TUweaken{\tau_1}{_}e)}} - {\TUweaken{\tau_1}{\tau_2}e} + \JUstep{\TUcast{_}{\tau_2}{(\TUcast{\tau_1}{_}e)}} + {\TUcast{\tau_1}{\tau_2}e}

- \JUstep{\TUweaken{\tau}{\tau}e}{e} + \JUstep{\TUcast{\tau}{\tau}e}{e}

- \Infer{\JOrder {\tau_e}{\tau_l}{\tau_d} } + \Infer{e = \TUcast {\tau}{\tau_e} e' \ + e' = {\tuple \Delta {\vec e}} \ + \JOrder {\tau_e}{\tau_l}{\tau_d}} {\JUstep{ - \TUcase {(\TUweaken {\tau}{_} {(\tuple \Delta {\vec e})})} {\tau_e} + \TUcase {e} {\tau_e} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} }{ - \Subst{e_\Ttagvar}{\id{refl},(\TUweaken {\tau}{\tau_l} {(\tuple \Delta - {\vec e})})}{P_x,x} + \Subst{e_\Ttagvar}{\id{refl}~{\tau_e}~e, \TUcast {\tau}{\tau_l} e'}{P_x,x} }}

- \Infer{\JOrder {\tau_e}{\tau_l}{\tau_d} } + \Infer{e = \TUcast {\tau}{\tau_e} e' \ + e' = {\tuple[l'] \Delta {\vec e}} \ + l \not= l' \ + \JOrder {\tau_e}{\tau_l}{\tau_d}} {\JUstep{ - \TUcase {(\TUweaken {\tau}{_} {(\tuple[l'] \Delta {\vec e})})}{\tau_e} + \TUcase {e}{\tau_e} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} }{ - \Subst{e_d}{\id{refl},(\TUweaken {\tau}{\tau_d} {(\tuple[l'] \Delta {\vec - e})})}{P_y,y} + \Subst{e_d}{\id{refl}~{\tau_e}~e,\TUcast {\tau}{\tau_d} {e'}}{P_y,y} }} %% \end{array} \end{mathpar} @@ -891,11 +929,10 @@ type equalities. \label{fig:union-reduce} \end{figure*}

-%% \newpage -\subsection{Unions} - -Since our tuples carry labels, our sum types do not need to carry any labels -and we can hence use plain untagged union types for them. We extend the +Since our tuples carry labels, we can rely on them to discriminate between +alternatives of sum types, which frees us from the need to use disjoint +unions and instead we can use the leaner untagged union types. +We extend the syntax with a new union type as well as corresponding introduction and elimination constructs: %% @@ -904,36 +941,45 @@ elimination constructs: \textsl{(term)} & e,\tau &::=& ... ~\MAlign{ |~ \TUnion{\tau_1}{\tau_2} \ - |~ \TUweaken{\tau_1}{\tau_2}e \ - |~ {\MAlign{\TUcase {e} {\tau_e \} {\Ttagvar}{x}{e_\Ttagvar \}{y}{e_d}}} + |~ \TUcast{\tau_1}{\tau_2}e \ + |~ {\MAlign{\TUcase {e \} {\tau_e} {\Ttagvar}{x}{e_\Ttagvar \}{y}{e_d}}} } \end{array} \end{displaymath}

-The \kw{weaken} operation should be read as a form of casting from a subtype +The \kw{cast} operation should be read as a form of weakening from a subtype to a supertype, at no run-time cost, while the \kw{switch} construct lets us recover the corresponding information, with a run-time cost comparable to that of a C \kw{switch} in the sense that it only checks the label and jumps to the appropriate branch but does not perform any further extraction of -data. As presented, 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, and it can easily be -extended to allow the presence of an arbitrary number of branches before the -default branch, of course. - -Figure~\ref{fig:unions} shows the typing rules for unions. These include -the three new rules, one per construct, added to the main typing judgment as -well as a few auxiliary definitions: the subtype relation -$\Jsubtype{\tau_1}{\tau_2}$ used for \kw{weaken}; the ``smart constructor'' -$\TUnionSmart{\tau_1}{\tau_2}$ which is like $\cup$ except it tries to eliminate the -$\bot$ elements which might have been introduced; and finally -$\JOrder{\tau}{\tau_{\Ttagvar}}{\tau_{d}}$ which plays two roles. First, it is used to -ensure that \kw{switch} is only applied to (weakened) tuples, which is -indispensable at run-time so we can safely go fetch the object's label even -though its type is a union type rather than a tuple type. Second, it is used -to find the refined type of $e$ in each branch, splitting ${\tau}$ into the -part ${\tau_{\Ttagvar}}$ that matches the label $l$ and the part ${\tau_{d}}$ -which does not. +data. + +Figure~\ref{fig:unions} shows the typing rules for unions. These introduce +three new rules, one per construct, added to the main typing judgment and +they rely on three auxiliary judgments presented in +Figure~\ref{fig:unions-aux}: the subtype relation $\Jsubtype{\tau_1}{\tau_2}$ used +for \kw{cast}; the ``smart constructor'' $\TUnionSmart{\tau_1}{\tau_2}$ which is +like $\cup$ except it tries to eliminate the $\bot$ elements which might have been +introduced; and finally $\JOrder{\tau}{\tau_{\Ttagvar}}{\tau_{d}}$ which plays two +roles. First, it is used to ensure that \kw{switch} is only applied to +(weakened) tuples, which is indispensable at run-time so we can safely go +fetch the object's label even though its type is a union type rather than +a tuple type. Second, it is used to find the refined type of $e$ in each +branch, splitting ${\tau}$ into the part ${\tau_{\Ttagvar}}$ that matches the +label $l$ and the part ${\tau_{d}}$ which does not. + +As presented, our \kw{switch} statement has the unusual property that it +tests a single label before falling through to a default branch, but since +the default branch properly preserves the information that this label failed +to match, it can be trivially chained in order to select between several +possible labels. Also it is easy to extend the language to allow the +presence of an arbitrary number of branches before the default branch, +of course. + +Another unusual property of this \kw{switch} statement, compared to the case +analysis rule of traditional inductive types is that the return type of all +branches is the same: the type refinement used for dependent-elimination is +replaced by an explicit equality proof witnessing which branch was chosen.

Reduction rules of the languages are extended with the obvious congruence rules as well as the primitive reductions shown in @@ -1100,7 +1146,7 @@ extended with the following primitive reduction: \JUstep{\Tunfold{_}{_}{(\Tfold{_}{_}{e})}}{e}

\Infer{e_i = \tuple{_}{_} - ~\vee~ e_i = \TUweaken{_}{_}{(\tuple{_}{_})}} + ~\vee~ e_i = \TUcast{_}{_}{(\tuple{_}{_})}} {\JUstep{\Tapp{(\Tmu[i]{x}{\tau}{e})}{\vec e}} {\Tapp{(\Subst{e}{\Tmu[i]{x}{\tau}{e}}x)}{\vec e}}} \end{mathpar} @@ -1144,7 +1190,7 @@ in CIC so as to make it easier to show equivalence between the two. \newcommand \JEstep[1] {#1 ;;\stackrel{e}{\leadsto};; } \newcommand \JEstepr[1] {#1 \stackrel{e}{\leadsto}{!!}^*~}

-The intention of our calculus is for \kw{weaken}, \kw{fold}, and \kw{unfold} +The intention of our calculus is for \kw{cast}, \kw{fold}, and \kw{unfold} to have no run-time cost. In this section, we show that it is indeed the case, by defining an erasure function and showing that the evaluation and the erasure commute. @@ -1165,7 +1211,7 @@ terms in a straightforward manner: %% \Erase{(\tuple \Delta {\vec e})} & \tuple {\Erase \Delta} {\vec {\Erase e}} \ %% \Erase{(\Tproj e i)} & \Tproj{\Erase e}i \ %% \Erase{(\TUnion{\tau_1}{\tau_2})} & \TUnion{\Erase{\tau_1}}{\Erase{\tau_2}} \ - \Erase{(\TUweaken{\tau_1}{\tau_2}e)} & \Erase e \ + \Erase{(\TUcast{\tau_1}{\tau_2}e)} & \Erase e \ %% FIXME: hardcodes \Erase! %% \MAlign[c]{(\TUcase {e} {\tau_e \} {\Ttagvar}{x}{e_\Ttagvar \}{y}{e_d})*} & %% \MAlign[c]{\TUcase[\Erase{\tau_r}] {\Erase e} {\Erase{\tau_e} \} @@ -1220,7 +1266,7 @@ the following: \end{mathpar}

We can show that this erasure calculus is consistent with the original -calculus, and hence that \kw{weaken}, \kw{fold}, and \kw{unfold} can safely +calculus, and hence that \kw{cast}, \kw{fold}, and \kw{unfold} can safely be implemented as no-ops: %% \begin{lemma}[Erasure] @@ -1532,7 +1578,7 @@ in~\cite{Coquand92}: \newcommand \TIproj[2] {\pi_{#1}~#2}

\begin{figure} - Tags are erased, union types are converted to tagged sums, and \kw{weaken} + Tags are erased, union types are converted to tagged sums, and \kw{cast} replaced by a chunk of code \begin{displaymath} \begin{array}{l@{;=;}l} @@ -1569,7 +1615,7 @@ in~\cite{Coquand92}: \Ftocic {\TUnion{\tau_1}{\tau_2}} & \TIeither{\Ftocic {\tau_1}}{\Ftocic {\tau_2}} \ %% \Ftocic {\Jsubtype{\tau_1}{\tau_2}} & \Tsarw{\Ftocic {\tau_1}}{\Ftocic {\tau_2}} \ %% \Ftocic {\id{S.refl}{e}} & \ - \Ftocic {\TUweaken{\tau_1}{\tau_2}{e}} & + \Ftocic {\TUcast{\tau_1}{\tau_2}{e}} & \Tapp{\Ftocic{\Jsubtype{\tau_1}{\tau_2}}}{\Ftocic {e}} \ \Ftocic { \MAlign[c]{ @@ -1643,8 +1689,8 @@ of notation, we will often write $\Ftocic e$ instead of $\Ftocic{\Jcuc{e}{\tau}} \begin{figure} FIXME!

- \caption{Mapping CUC to CIC} - \label{fig:cuc-to-cic} + \caption{Mapping CIC to CUC} + \label{fig:cic-to-cuc} \end{figure}

If we have $\Jcic e \tau$ then $\Jcuc {\Ftocuc e} {\Ftocuc \tau}$. @@ -1662,14 +1708,13 @@ judgments into the logic: themselves be strictly positive) or of type $\Tapp{\id{terminating-function}}{f}$ (FIXME: how would this work? Can we just defer to F-star instead?). -\item \kw{weaken} can take a proof of type $\tau_1 \subseteq \tau_2$. -\item \kw{case}'s ordering/splitting relation can similarly be reified. +\item \kw{cast} can take a proof of type $\tau_1 \subseteq \tau_2$. +\item \kw{switch}'s ordering/splitting relation can similarly be reified. \item \kw{tuple} can take a list of fields (type $\Tapp{\id{field-list}}{\ell}$) \end{itemize}

\section{Related works}

-\nocite{Luo09} \nocite{Gimenez94} \nocite{Blume06,Castagna16} %Union types and extensible sums \nocite{Chapman10} %Levitation

View it on GitLab: https://gitlab.com/monnier/typer/commit/656f7ed7fd708968256e164c8faf8bced804...