Stefan pushed to branch report/itd at Stefan / Typer

Commits: 3bcb7c68 by Stefan Monnier at 2018-10-19T13:50:36Z -

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -66,6 +66,8 @@ \newcommand \Comment[1] {}

\newcommand \FIXME[1] {\fbox{\parbox{\columnwidth}{{\color{red}{¡FIXME!}} #1}}} +%% \newtheorem{theorem}{Theorem}[section] +%% \newtheorem{lemma}[theorem]{Lemma}

\newcommand \CCw {CC$\omega$}

@@ -86,13 +88,18 @@

\newcommand \Jcuc[2][\Gamma] {#1 \vdash_U #2 :} \newcommand \Jcic[2][\Gamma] {#1 \vdash_I #2 :} -\newcommand \Jstep[1] {#1 ;\leadsto; } +\newcommand \Jstep[1] {#1 ;;\leadsto;; } +%% \newcommand \Jstepr[1] {#1 \leadsto^{!*}} +\newcommand \JUstep[1] {#1 ;;\stackrel{U}{\leadsto};; } +\newcommand \JUstepr[1] {#1 \stackrel{U}{\leadsto}{!!}^*~}

-\newcommand \MetaFunction[2] {\llbracket #2 \rrbracket_{#1}} +%% \newcommand \MetaFunction[2] {\llbracket #2 \rrbracket_{#1}} +\newcommand \MetaFunction[2] {\left\llbracket #2 \right\rrbracket_{#1}} \newcommand \Ftocic {\MetaFunction{I}} \newcommand \Ftocuc {\MetaFunction{U}}

-\newcommand \MAlign[1]{\begin{array}[t]{@{}l@{}} #1 \end{array}} +\newcommand \MAlign[2][t]{\begin{array}[#1]{@{}l@{}} #2 \end{array}} +\newcommand \TAlign[1]{\begin{tabular}[t]{@{}l@{}} #1 \end{tabular}}

\newif \iflongversion

@@ -162,7 +169,7 @@

%% FIXME: I like to have the table of contents while writing, so I can get %% a quick overview of the structure. Should be removed before submission. -\newpage \tableofcontents +%% \newpage \tableofcontents

\section{Introduction}

@@ -245,8 +252,7 @@ The contributions of this article are:

\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 \TIcase[4] {\langle#1\rangle\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 @@ -269,16 +275,16 @@ 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, +The $\Tind{x}{\tau}{\vec c}$ constructor is a 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. +the only eliminator and is a large construct whose naive code size and +run-time complexity has as lower bound 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 definitions +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 @@ -384,7 +390,8 @@ we partly agree: it was not the primary motivation for our design. Yet, our design provides us with that kind of refinement at a much lower cost, making it practical to provide this feature even if it is not used very often.

-\section{Base calculus} +\section{The calculus of united constructions} +%% \subsection{Base calculus}

\begin{figure} \begin{displaymath} @@ -446,6 +453,13 @@ it practical to provide this feature even if it is not used very often. \label{fig:ccw} \end{figure}

+Just like the full CIC, our new calculus is fairly large, so we present it +in several steps: the base calculus, the tuples, the equality type, the +sums, and finally the recursive definitions. Those parts are not completely +independent from each other, which largely dictates the order in which they +are presented, but to a large extent the base calculus can be replaced with +any other lambda calculus. + Figure~\ref{fig:ccw} shows our base language \CCw{} as a pure type system (PTS)~\cite{Barendregt91b}. It is a variant of CoC with a tower of universes à la ECC~\cite{Luo89}. @@ -458,12 +472,17 @@ 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. +(CUC) which we present in the next few sections in the form of a collection +of extensions. The typing judgment of the base language is usually denoted +$\Jtyper e \tau$, and we will annotate it as $\Jcuc e \tau$ or $\Jcic e \tau$ when we +talk about the typing derivation of CUC resp.~CIC. Similarly, while the +base language's reduction rule is usually written $e\leadsto e'$, we will write it +as $e\stackrel{U}{\leadsto} e'$ or $e\stackrel{U}{\leadsto} e'$ when we talk about the +reduction rule for CUC resp.~CIC.

\Comment{ \newpage - \section{Dependent pairs} + \subsection{Dependent pairs}

\newcommand \TPair[2] {\Sigma#1:#2.} \newcommand \Tpair[2] {\langle#1,#2\rangle} @@ -493,15 +512,11 @@ extensions. \end{figure}

Figure~\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!} }

\Comment{ \newpage - \section{Tagged sums} + \subsection{Tagged sums}

\newcommand \TSum[1] {#1~{+}~} \newcommand \TSinj[1][\Ttagvar] {\kw{inj}_{#1}} @@ -538,7 +553,7 @@ extensions. }

%% \newpage -\section{Tuples} +\subsection{Tuples}

\newcommand \Tuple[2][\Ttagvar] {\kw{Tuple}_{#1}~#2} \newcommand \tuple[2][\Ttagvar] {\kw{tuple}_{#1}~{#2}~} @@ -561,30 +576,30 @@ extensions.

\begin{mathpar} \Infer%% [T-base] - { }{\Jtyper {\Tuple \EmptyCtx}{\Type 0}} + { }{\Jcuc {\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})}}} + {\Jcuc {\Tuple \Delta}{\Type {\ell_1}} \ + \Jcuc[\Gamma,\Delta] \tau {\Type {\ell_2}}} + {\Jcuc {\Tuple {\Delta,x:\tau}}{\Type {(\Tmax{\ell_1}{\ell_2})}}}

\Infer%% [TC-field] {|\vec e| = 0} - {\Jtyper {\vec e} {\EmptyCtx}} + {\Jcuc {\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}} + {\Jcuc {\vec e} {\Delta} \ + \Jcuc {e_i} {\tau_i[{\vec e}/\Delta]}} + {\Jcuc {\vec e, e_i} {\Delta, x:\tau_i}}

- \Infer{\Jtyper {\vec e} {\Delta}} - {\Jtyper {\tuple \Delta {\vec e}} {\Tuple \Delta}} + \Infer{\Jcuc {\vec e} {\Delta}} + {\Jcuc {\tuple \Delta {\vec e}} {\Tuple \Delta}}

\Infer%% [T-proj] - {\Jtyper{e}{\Tuple \Delta} \ + {\Jcuc{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}]}} + {\Jcuc{\Tproj e i}{\tau_i[{\Tproj e 0,..,\Tproj e {i!-!1}}/x_0,..,x_{i!-!1}]}} \end{mathpar} \caption{Tuples} \label{fig:tuples} @@ -596,9 +611,10 @@ 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. +within the metadata needed for memory management purposes, and even in the +worst case it just adds one extra field to those heap objects.

-Our language's syntax is extended as follows: +To that end, our language's syntax is extended as follows: \begin{displaymath} %% \begin{array}{l@{;:;}l} %% \TLabel & \Type 0; \ @@ -630,26 +646,28 @@ Where $\Tuple \Delta$ is the type constructor for tuples with label $l$ where $\ 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 +typing rules for our labeled tuples. Reduction rules of the language are extended with the obvious congruence rules as well as the following primitive reduction: \begin{displaymath} - (\tuple \Delta {\vec e}).i ;;\leadsto;; e_i + \JUstep{(\tuple \Delta {\vec e}).i}{e_i} \end{displaymath}

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$. +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.

\Comment{ %% \newpage - \section{Tagged terms} + \subsection{Tagged terms}

\newcommand \TTag[1][\Ttagvar] {\kw{Tag}_{#1}~} \newcommand \Ttag[1][\Ttagvar] {\kw{tag}_{#1}} @@ -690,43 +708,60 @@ that any value of arrow type has to be of the form $\lambda x:\tau.e$. }

%% \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} - -%% \newpage -\section{Unions} +\subsection{Equality} + +Armed with tuples, we can now do most of what is done with single-constructor +inductive types, but not all: our tuples do not offer us any way to define +the equivalent of those single-constructor inductive types which are +\emph{indexed}. The main example of such a type is the equality type. +In the CoC, the equality type can be defined using the impredicative +encoding, with the usual associated restrictions, but our base calculus +being predicative we don't even have that option. So we extend our language +with a built-in equality type. + +Rather than extend the syntax, this time we add new axioms to the initial +environment: +\begin{displaymath} + \begin{array}{l@{;:;}l} + \id{Eq} & \Tarw{t}{\Type{\ell}}{\Tarw {x,y} t {\Type{\ell}}}; \ + \id{refl} & \Tarw{t}{\Type{\ell}}{\Tarw{x}{t}{\id{Eq}~t~x~x}}; \ + J & \MAlign{ + \Tarw{t}{\Type{\ell_1}}{\Tarw {x,y} t {\Tarw u {\Type{\ell_2}} {\Tarw + f {\Tsarw t u} {}}}} \ + \Tsarw{\id{Eq}~t~x~y}{\Tsarw{f~x}{f~y}} + ;} + \end{array} +\end{displaymath} +\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 +from context. + +Note that we are cheating a bit in those declarations: +%% not only those declarations use +%% a shorthand notation eliding some arguments that can be inferred, but they +they rely on some form of universe polymorphism, so they +should be read as declaration schemas, which need to be freshly instantiated +for each use. + +Additionally to the declarations, we need to add the following primitive +reduction rule: +\begin{mathpar} + \JUstep {J~_~_~_~_~_~(\id{refl}~_~_)~x}x +\end{mathpar} +where the underscores represent subterms which are ignored by the rule. + +While the equality type was not the only single-constructor inductive type +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.

\newcommand \TUnion[1] {#1~\cup~} \newcommand \TUnionSmart[1] {#1~\cup'~} -\newcommand \TUweaken[1] {\id{S.weaken}~#1~} -\newcommand \TUcase[6] {\kw{switch}~#1~|~#2~#3~P_{#3}~\Rightarrow #4~|~#5~P_{#5}~\Rightarrow #6} +\newcommand \TUweaken[2] {\kw{weaken}~#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}

\newcommand \JSplit[3] {#2 \Longleftarrow #1~/\Ttagvar \Longrightarrow #3} \newcommand \JOrder[3] {#1;\stackrel\Ttagvar\Longrightarrow;\TUnion{#2}{#3}} @@ -734,9 +769,45 @@ that any value of arrow type has to be of the form $\lambda x:\tau.e$. \newcommand \Jsubtype [1] {#1~\subseteq~}

\begin{figure} + \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{\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} \\ + %% \tau_e = \TUnion{_}{_} \\ + \Jcuc[\Gamma,x:{{\tau_\Ttagvar}},P_x:(e \equiv \TUweaken{\tau_l}{\tau_e}{x})] + {e_\Ttagvar} {\tau_r} \ + \Jcuc[\Gamma,y:{\tau_d},P_y:(e \equiv \TUweaken{\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}

+ %% \begin{figure} \begin{mathpar} - %% FIXME: Make it return the \Jsubtype proofs! + \ovalbox{\ensuremath{ + \begin{array}[b]{l|l} + \JOrder{\tau}{\tau_{\Ttagvar}}{\tau_{d}} & + \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$} + \end{array} + }} \vspace{-15pt} \hfill \\ \Infer%% [U-order1] { }{\JOrder{\Tuple{\Delta}}{\Tuple{\Delta}}{\bot}}

@@ -744,7 +815,7 @@ that any value of arrow type has to be of the form $\lambda x:\tau.e$. {\Ttagvar' \neq \Ttagvar} {\JOrder{\Tuple[\Ttagvar']{\Delta}}{\bot}{\Tuple[\Ttagvar']{\Delta}}}

- \Infer[U-order-union] + \Infer%% [U-order-union] {\JOrder{\tau_1}{\tau_{\Ttagvar{}1}}{\tau_{d1}} \ \JOrder{\tau_2}{\tau_{\Ttagvar{}2}}{\tau_{d2}}} {\JOrder{\TUnion{\tau_1}{\tau_2}} @@ -761,193 +832,410 @@ that any value of arrow type has to be of the form $\lambda x:\tau.e$. \end{mathpar}

\begin{mathpar} - \Infer[U-elim] - {\Jtyper e {\tau_u} \ - \JOrder {\tau_u} {\tau_\Ttagvar} {\tau_d} \ - %% FIXME: Args to TUweaken! - \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} - \end{mathpar} + \Infer{ }{\Jsubtype {\tau}{\tau}} + + \Infer{\Jsubtype {\tau_1}{\tau_2}} + {\Jsubtype {\tau_1}{\TUnion{\tau_2}{\tau_3}}} + + \Infer{\Jsubtype {\tau_1}{\tau_2}} + {\Jsubtype {\tau_1}{\TUnion{\tau_3}{\tau_2}}}

- \caption{Unions} + \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} \end{figure}

+\begin{figure*} + \begin{mathpar} + %% \begin{array}{r@{;;\leadsto;;}l} + \JUstep{\TUweaken{_}{\tau_2}{(\TUweaken{\tau_1}{_}e)}} + {\TUweaken{\tau_1}{\tau_2}e} + + \JUstep{\TUweaken{\tau}{\tau}e}{e} + + \Infer{\JOrder {\tau_e}{\tau_l}{\tau_d} } + {\JUstep{ + \TUcase {(\TUweaken {\tau}{_} {(\tuple \Delta {\vec 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} + }} + + \Infer{\JOrder {\tau_e}{\tau_l}{\tau_d} } + {\JUstep{ + \TUcase {(\TUweaken {\tau}{_} {(\tuple[l'] \Delta {\vec 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} + }} + %% \end{array} + \end{mathpar} + \caption{Reduction rules for the union types} + \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 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{S.refl};\tau & \Jsubtype \tau \tau \ - \id{S.left};\tau_3 & - \Jsubtype{\tau_1}{\tau_2} \to \Jsubtype{\tau_1}{\TUnion{\tau_2}{\tau_3}} \ - \id{S.right};\tau_3 & - \Jsubtype{\tau_1}{\tau_2} \to \Jsubtype{\tau_1}{\TUnion{\tau_3}{\tau_2}} \ - \id{S.both} & - \Jsubtype{\tau_1}{\tau_3} \to \Jsubtype{\tau_2}{\tau_3} \to - \Jsubtype{\TUnion{\tau_1}{\tau_2}}{\tau_3} \ - \id{S.trans} & - \Jsubtype{\tau_1}{\tau_2} \to \Jsubtype{\tau_2}{\tau_3} \to - \Jsubtype{\tau_1}{\tau_3} \ - \TUweaken{} & \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 constructors that allow constructing proofs of -subtyping between union types, and finally the \id{S.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 -as 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: +and we can hence use plain untagged union types for them. We extend the +syntax with a new union type as well as corresponding introduction and +elimination constructs: %% \begin{displaymath} \begin{array}{lc@{;;}c@{;;}l} \textsl{(term)} & e,\tau &::=& ... ~\MAlign{ - |~ {\MAlign{\TUcase {e \} {\Ttagvar}{x}{e_\Ttagvar \}{y}{e_d}}} + |~ \TUnion{\tau_1}{\tau_2} \ + |~ \TUweaken{\tau_1}{\tau_2}e \ + |~ {\MAlign{\TUcase {e} {\tau_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.

-Reduction rules of the languages are -extended with the obvious congruence rules as well as the following -primitive reductions: -\begin{figure*} - \begin{displaymath} - \begin{array}{r@{;;\leadsto;;}l} - \id{S.weaken}~P_1~(\id{S.weaken}~P_2~e) & - \id{S.weaken}~(\id{S.trans}~P_2~P_1)~e \ - %% \multicolumn 2 l {\TUcase {(\tuple \Delta {\vec e})} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d}} \ - %% & - %% \Subst{e_\Ttagvar}{\id{refl},\tuple \Delta {\vec e}}{P_x,x} \ - %% \multicolumn 2 l {\TUcase {(\tuple[l'] \Delta {\vec e})} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d}} \ - %% & - %% \Subst{e_d}{\id{refl},\tuple[l'] \Delta {\vec e}}{P_y,y} \ - %% \multicolumn 2 l {\TUcase {(\TUweaken P {(\tuple \Delta {\vec e})})} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d}} \ - %% & - %% \Subst{e_\Ttagvar}{\id{refl},\tuple \Delta {\vec e}}{P_x,x} \ - %% \multicolumn 2 l {\TUcase {(\tuple[l'] \Delta {\vec e})} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d}} \ - %% & - %% \Subst{e_d}{\id{refl},\tuple[l'] \Delta {\vec e}}{P_y,y} \ - %% FIXME: Get rid of those first two! - \TUcase {(\tuple \Delta {\vec e})} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} & - \Subst{e_\Ttagvar}{\id{refl},\tuple \Delta {\vec e}}{P_x,x} \ - \TUcase {(\tuple[l'] \Delta {\vec e})} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} & - \Subst{e_d}{\id{refl},\tuple[l'] \Delta {\vec e}}{P_y,y} \ - \TUcase {(\TUweaken P {(\tuple \Delta {\vec e})})} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} & - \Subst{e_\Ttagvar}{\id{refl},\tuple \Delta {\vec e}}{P_x,x} \ - \TUcase {(\TUweaken P {(\tuple[l'] \Delta {\vec e})})} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} & - \Subst{e_d}{\id{refl},\tuple[l'] \Delta {\vec e}}{P_y,y} \ - \end{array} - \end{displaymath} -\end{figure*} +The \kw{weaken} operation should be read as a form of casting 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. + +Reduction rules of the languages are extended with the obvious congruence +rules as well as the primitive reductions shown in +Figure~\ref{fig:union-reduce}. These reductions rules are fairly complex to +our taste, especially compared to something like the $\beta$ rule, but they will +be simplified in the erasure semantics presented in +Section~\ref{sec:erasure}.

-\begin{displaymath} - \begin{array}{l@{;;\leadsto;;}l} - \id{S.trans}~\id{S.refl}~P & P \ - \id{S.trans}~P~\id{S.refl} & P \ - \id{S.trans}~P_1~(\id{S.left}~\tau~P_2) & - \id{S.left}~\tau~(\id{S.trans}~P_1~P_2) \ - \id{S.trans}~P_1~(\id{S.right}~\tau~P_2) & - \id{S.right}~\tau~(\id{S.trans}~P_1~P_2) \ - \id{S.trans}~(\id{S.left}~\tau~P_1)~(\id{S.both}~P_2~P_3) & - \id{S.trans}~P_1~P_2 \ - \id{S.trans}~(\id{S.right}~\tau~P_1)~(\id{S.both}~P_2~P_3) & - \id{S.trans}~P_1~P_3 \ - \id{S.trans}~(\id{S.both}~P_1~P_2)~P_3 & - \id{S.both}~(\id{S.trans}~P_1~P_3)~(\id{S.trans}~P_2~P_3) \ - \end{array} -\end{displaymath}

%% FIXME: reduction rules? Especially for the `weaken` thingy!

-Figure~\ref{fig:unions} shows the 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.

-\section{Recursion} +\subsection{Recursion}

\newcommand \Tmu[4][] {\mu_{#1} #2:#3 . #4} -\newcommand \Tfold[1] {\kw{fold}~#1~} -\newcommand \Tunfold {\kw{unfold}~} -\newcommand \Jpos[2][\nu] {#1 \vdash #2;;\kw{pos}} -\newcommand \Jterm[3][x_f;i;x_i] {#1;#2 \vdash #3;;\kw{term}} +\newcommand \Tfold[2] {\kw{fold}~#1~#2~} +\newcommand \Tunfold[2] { + \kw{unfold}~#1~#2~ +} +\newcommand \JUpos[2][x] {#1 \vdash #2;;\kw{pos}} +\newcommand \JUdecreasing[3][x_f;i;x_i] {#1;#2 \vdash #3;;\kw{term}} +\newcommand \JUsmaller[3][x_f;i;x_i] {#1;#2 \vdash #3;;\kw{smaller}}

+\newcommand \FigRecurse{ \begin{figure} - \begin{displaymath} - \begin{array}{lc@{;;}c@{;;}l} - \textsl{(index)} & i &\in& \mathbb{N} \ - \textsl{(term)} & e,b,c,\tau &::=& - ... ~\MAlign{ - |~ \Tmu[i]{x}{\tau}{e} - ~|~ \Tmu{x}{\tau}{e} \ - |~ \Tfold{\tau}{e} - ~|~ \Tunfold{e} - } \ - \end{array} - \end{displaymath}

\begin{mathpar} - \Infer{\Jtyper{\tau}{s} \ - \Jtyper[\Gamma,x:\tau]{e}{\tau} \ - \Jpos[{x}]e} - {\Jtyper{\Tmu{x}{\tau}{e}}{\tau}} - - %% FIXME: Define term - \Infer{\Jtyper{\tau}{s} \ - \Jtyper[\Gamma,x:\tau]{e}{\tau} \ + \Infer{\Jcuc{\tau}{s} \ + \Jcuc[\Gamma,x:\tau]{e}{\tau} \ + e = \Tmlam y \tau {e'} \ + x \not\in \kw{fv}(\vec \tau) \ + \JUpos {e'}} + {\Jcuc{\Tmu{x}{\tau}{e}}{\tau}} + + \Infer{\Jcuc{\tau}{s} \ + \Jcuc[\Gamma,x:\tau]{e}{\tau} \ e = \Tmlam{y}{_}{e_b} \ i < |y| \ - \Jterm[x;i;y_i]{\emptyset}{e_b}} - {\Jtyper{\Tmu[i]{x}{\tau}{e}}{\tau}} + \JUdecreasing[x;i;y_i]{\emptyset}{e_b}} + {\Jcuc{\Tmu[i]{x}{\tau}{e}}{\tau}}

- \Infer{\Jtyper{e}{\Tapp{\tau}{\vec p}} \ + \Infer{\Jcuc{e}{\Tapp{\tau}{\vec p}} \ + \Jcuc{\tau}{_} \ \tau = \Tmu{x}{_}{e_\tau}} - {\Jtyper{\Tunfold{e}}{\Tapp{(\Subst{e_\tau}{\tau}{x})}{\vec p}}} + {\Jcuc{\Tunfold{\tau}{\vec p}{e}}{\Tapp{(\Subst{e_\tau}{\tau}{x})}{\vec p}}}

- \Infer{\Jtyper{e}{\Tapp{(\Subst{e_\tau}{\tau}{x})}{\vec p}} \ - FIXME! \ + \Infer{\Jcuc{e}{\Tapp{(\Subst{e_\tau}{\tau}{x})}{\vec p}} \ + \Jcuc{\tau}{_} \ \tau = \Tmu{x}{_}{e_\tau}} - {\Jtyper{\Tfold{e}}{\Tapp{\tau}{\vec p}}} + {\Jcuc{\Tfold{\tau}{\vec p}{e}}{\Tapp{\tau}{\vec p}}} + \end{mathpar} + \begin{mathpar} + \ovalbox{\ensuremath{ + \begin{array}[b]{l|l} + \JUpos e & \text{$e$ is positive in $x$} + \end{array} + }} \vspace{-15pt} \hfill \\ + + \Infer{x \not\in \kw{fv}(e)}{\JUpos e} + + \Infer{x \not\in \kw{fv}(\vec e)}{\JUpos {\Tapp x {\vec e}}} + + \Infer{\JUpos e \ x \not\in \kw{fv}(\tau)}{\JUpos {\Tarw y \tau e}} + + \Infer{\Delta = x_0:\tau_0,..,x_n:\tau_n \ + \forall i . \ x \not\in \kw{fv}({\tau_i}) ~\vee~ (\JUpos {\tau_i} ~\wedge~ \forall j>i.~ x_i\not\in \kw{fv}({\tau_j}))} + {\JUpos {\Tuple \Delta}}

- FIXME! + \Infer{\JUpos {\tau_1} \ \JUpos {\tau_2}} + {\JUpos {\TUnion{\tau_1}{\tau_2}}} + + \Infer{\JUpos {e} \ x \not\in \kw{fv}(\tau)} + {\JUpos {\Tmu{y}{\tau}{e}}} + \end{mathpar} + \begin{mathpar} + \ovalbox{\ensuremath{ + \begin{array}[b]{l|l} + \JUdecreasing{\nu}{e} & + \text{\TAlign{$i^{th}$ arg of $x_f$ always smaller than \ + $x_i$ in $e$, given that $\nu$ are smaller}} + \end{array} + }} \vspace{-15pt} \hfill \\ + + \iflongversion + %% Uninteresting congruence rules + \Infer{\JUdecreasing \nu \tau \ \JUdecreasing \nu e} + {\JUdecreasing \nu {\Tlam x \tau e}} + + %% FIXME : add more congruence rules + \else \fi + + \Infer{x_f \not\in \kw{fv}(e)} + {\JUdecreasing \nu {e}} + + \Infer{\JUdecreasing \nu {\vec e} \ + i < |e| \ + e_i = \Tapp{x_e}{\vec {_}} \ + x_e \in \nu} + {\JUdecreasing \nu {\Tapp{x_f}{\vec e}}} + + \Infer{e_2 = \Tapp{x_e}{\vec _} \ + \JUdecreasing {\nu} {e_2} \ + x_e \in \nu \cup { x_i } \ + \JUdecreasing {{x}\cup\nu} {e_1}} + {\JUdecreasing \nu {\Tapp{(\Tlam x \tau {e_1})}{(\Tproj {e_2} {i'})}}} + + \Infer{e_2 = \Tapp{x_e}{\vec _} \ + \JUdecreasing {\nu} {e_2} \ + x_e \in \nu \cup { x_i } \ + \JUdecreasing {{x}\cup\nu} {e_1}} + {\JUdecreasing \nu {\Tapp{(\Tlam x \tau {e_1})}{(\Tunfold{_}{_}{e_2})}}} + + \Infer{\JUdecreasing {\nu} {\tau_e} \ + \JUdecreasing {\nu} {\tau_r} \ + \JUdecreasing {\nu} {e} \ + e = \Tapp{x_e}{\vec _} \ + \JUdecreasing {{x}\cup\nu} {e_l} \ + x_e \in \nu \cup { x_i } \ + \JUdecreasing {{y}\cup\nu} {e_d}} + {\JUdecreasing \nu {\TUcase {e} {\tau_e} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d}}} + \end{mathpar} \caption{Recursive definitions} \label{fig:recurse} \end{figure} +} + +%% type U | u (U -> U); +%% f (u g) = g (u g); +%% infloop = f (u f); +%% +%% U = μx . (x \to x) +%% f g = (unfold g) g + +The final missing component of inductive types is that which gives it its +name: the ability to define recursive types and to perform induction on +values of those types. Both of those correspond to forms of recursive +definitions, one of them for types and the other for functions. +We could handle both cases within the same fixpoint construct, but since +they require different termination checking rules, we have kept the +two separate. Concretely, the syntax is extended as follows: +%% +\begin{displaymath} + \begin{array}{lc@{;;}c@{;;}l} + \textsl{(index)} & i &\in& \mathbb{N} \ + \textsl{(term)} & e,b,c,\tau &::=& + ... ~\MAlign{ + |~ \Tmu[i]{x}{\tau}{e} + ~|~ \Tmu{x}{\tau}{e} \ + |~ \Tfold{\tau}{\vec p}{e} + ~|~ \Tunfold{\tau}{\vec p}{e} + } \ + \end{array} +\end{displaymath} +\FigRecurse +Where $\Tmu{x}{\tau}{e}$ is the fixpoint construct that can be used to define +recursive types, as along as the obey the customary strict positivity +constraint; while $\Tmu[i]{x}{\tau}{e}$ is the fixpoint cons-truct that can be +used to define recursive functions when they abide by a syntactic +restriction that ensures that the $i^{th}$ argument becomes smaller at each +recursive call. The $\Tmu{x}{\tau}{e}$ type constructor has corresponding +introduction and elimination forms \kw{fold} resp. \kw{unfold}. + +As usual, additionally to the congruence rules, the reduction rules are +extended with the following primitive reduction: +\begin{mathpar} + \JUstep{\Tunfold{_}{_}{(\Tfold{_}{_}{e})}}{e} + + \Infer{e_i = \tuple{_}{_} + ~\vee~ e_i = \TUweaken{_}{_}{(\tuple{_}{_})}} + {\JUstep{\Tapp{(\Tmu[i]{x}{\tau}{e})}{\vec e}} + {\Tapp{(\Subst{e}{\Tmu[i]{x}{\tau}{e}}x)}{\vec e}}} +\end{mathpar} +The first is the usual $\beta$-like application of an elimination operation on +the corresponding constructor, but the second is less usual: +$\Tmu[i]{x}{\tau}{e}$ is a value constructor with no matching type constructor +nor elimination construct. Its elimination rule is designed to carefully +unfold the function often enough not to get in the way, but not too often to +cause infinite unfoldings. + +The typing rules are given in Figure~\ref{fig:recurse}. +As was the case for union types, the figure shows first the four new rules +added to the main typing judgment, one for each new construct, and then some +auxiliary judgments: first the $\JUpos {\tau}$ judgment, which enforces the +strict positivity rule on $\Tmu{x}{\tau}{e}$, and then the $\JUdecreasing \nu e$ +judgment which enforces termination of $\Tmu[i]{x_f}{\tau}{e}$. + +The positivity check is fairly straightforward. It allows nested recursive +definitions and does not check that those are themselves positive, because +this verification will have been done by the typing rules already. +More importantly, the positivity rule for our (dependent) tuples enforces +that we cannot have a dependence on a recursive argument: if field $x_i$ +refers to the recursive argument $x$, then subsequent fields cannot depend on +$x_i$ (i.e.~the type of subsequent fields cannot refer to $x_i$). + +The rules for the termination check do not include the straightforward +congruence rules. They consider \kw{switch} operations, field projections +$\Tproj e i$, $\Tunfold{\tau}{\vec p} e$, as well as function calls, as those +operations which return something smaller. Since it only keeps tracks of +variables being smaller than the original argument, rather than expressions +it can only keep track of $\Tproj e i$ and $\Tunfold{\tau}{\vec p}e$ being +smaller when those expression get bound to a variable. This same problem +applies to the case of function calls, of course, but it is solved +differently for them. The reason for this is to better match the rules used +in CIC so as to make it easier to show equivalence between the two.

\section{Erasure} +\label{sec:erasure} + +\newcommand \Erase[1] {#1{*}} +\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} +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. + +The erasure function $\Erase{(\cdot)}$ is defined recursively on the syntax of +terms in a straightforward manner: +%% +\begin{displaymath} + \begin{array}{l@{;\mapsto;}l} + %% \Erase{\EmptyCtx} & \EmptyCtx \ + %% \Erase{(\Delta,x:\tau)} & \Erase \Delta,x:\Erase \tau \medskip \ + \Erase x & x \ + \Erase{(\Tapp{e_1}{e_2})} & \Tapp{\Erase {e_1}}{\Erase{e_2}} \ + \Erase{(\Tarw{x}{\tau_1}{\tau_2})} & \Tarw{x}{\Erase{\tau_1}}{\Erase{\tau_2}} \ + \Erase{(\Tlam x \tau e)} & \Tlam x {\Erase \tau} {\Erase e} \ + \hfill \cdots \hfill\hfill & \cdots \ + %% \Erase{(\Tuple \Delta)} & \Tuple {\Erase \Delta} \ + %% \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 \ + %% 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} \} + %% {\Ttagvar}{x}{\Erase{e_\Ttagvar} \}{y}{\Erase{e_d}}} \ + %% \Erase{(\Tmu[i]{x}{\tau}{e})} & \Tmu[i]{x}{\Erase \tau}{\Erase e} \ + %% \Erase{(\Tmu{x}{\tau}{e})} & \Tmu{x}{\Erase \tau}{\Erase e} \ + \Erase{(\Tfold{\tau}{\vec p}{e})} & \Erase e \ + \Erase{(\Tunfold{\tau}{\vec p}{e})} & \Erase e \ + \end{array} +\end{displaymath} +The $\cdots$ stand for all the remaining constructs where the function simply +recurses in the obvious way on all subterms. We do not need to introduce +a new syntax for erased terms because they simply use a subset of the syntax +of the non-erased terms. + +On the other hand, we do need to introduce new reduction rules. Other than +the usual congruence rules, the reduction rules of the erased calculus are +the following: +%% +\begin{mathpar} + \JEstep{\Tapp{(\Tlam x \tau {e_1})}{e_2}}{\Subst{e_1}{e_2}x} + + \JEstep{(\tuple \Delta {\vec e}).i}{e_i} + + \JEstep {J~_~_~_~_~_~(\id{refl}~_~_)~x}x + + \begin{array}{c} + \JEstep{ + \TUcase {(\tuple \Delta {\vec e})} {\tau_e} + {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} \ + }{ + \Subst{e_\Ttagvar} + {\id{refl},(\tuple \Delta {\vec e})} + {P_x,x} + } + \end{array}

-The intention of our calculus is for \kw{weaken} 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. + \begin{array}{c} + \JEstep{ + \TUcase {(\tuple[l'] \Delta {\vec e})}{\tau_e} + {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} \ + }{ + \Subst{e_d} + {\id{refl},(\tuple[l'] \Delta {\vec e})} + {P_y,y} + } + \end{array} + + \Infer{e_i = \tuple{_}{_}} + {\JEstep{\Tapp{(\Tmu[i]{x}{\tau}{e})}{\vec e}} + {\Tapp{(\Subst{e}{\Tmu[i]{x}{\tau}{e}}x)}{\vec e}}} +\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 +be implemented as no-ops: +%% +\begin{lemma} + \label{lem:erasure} + Assuming $ \Jcuc e \tau$, we have: + \begin{itemize} + \item If $\JUstepr e {e_1}$ then $\JEstepr{\Erase e}{\Erase {e_1}}$. + \item If $\JEstepr{\Erase e}{e_2}$ then there exists an $e_3$ such that + $\Erase{e_3} = e_2$ and $\JUstepr e {e_3}$. + \end{itemize} +\end{lemma} +%% \begin{proof} +%% FIXME +%% \end{proof}

\section{Equivalence} \label{sec:equivalence}

Now that we have defined a calculus which provides us with the intended -run time cost, we show that this calculus shares all the other desirable -characteristics of CIC by showing a translation between the two calculus -which is sound and complete. +run-time cost, we show that this calculus is sound and complete with respect +to a more classic presentation of inductive types. We will first present +a variant of our base calculus extended with inductive types in the style +of~\citet{Gimenez94}, and then show that any expression of our CUC can be +compiled to this CIC, and the reverse as well.

\subsection{Inductive types}

@@ -957,10 +1245,12 @@ which is sound and complete. %% ~\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}} -\newcommand \Jdecreasing[3][x_f;i;x_i] {#1;#2 \vdash #3~\kw{term}} +\newcommand \JIcon[2][x;y] {#1 \vdash #2;;\kw{con}} +\newcommand \JIpos[2][x] {#1 \vdash #2;;\kw{pos}} +\newcommand \JIdecreasing[3][x_f;i;x_i] {#1;#2 \vdash #3;;\kw{term}} \newcommand \BT[2] {\id{BT}\llbracket #1 \rrbracket_{#2}} +\newcommand \JIstep[1] {#1 ;;\stackrel{I}{\leadsto};; } +\newcommand \JIstepr[1] {#1 \stackrel{I}{\leadsto}{!!}^*~}

\begin{figure*} %% Syntax @@ -969,55 +1259,55 @@ which is sound and complete. \begin{mathpar} \ovalbox{\ensuremath{ \begin{array}[b]{l|l} - \Jtyper e \tau & \text{$e$ has type $\tau$ in $\Gamma$} \ - \Jstep {e}{e'} & \text{$e$ reduces to $e'$} + \Jcic e \tau & \text{$e$ has type $\tau$ in $\Gamma$} \ + \JIstep {e}{e'} & \text{$e$ reduces to $e'$} \end{array} }} \hfill %% FIXME: This presentation doesn't allow `Con(0,Nat)` but requires %% substituting every `Nat` with its definition. %% Could it be that this is not needed in CUC? \Infer{e = \Tind{x}{\tau}{\vec c} \ - \Jtyper e \tau} - {\Jtyper{\Tcon{i}{e}}{\Subst{c_i}{x}{e}}} \hfill + \Jcic e \tau} + {\Jcic{\Tcon{i}{e}}{\Subst{c_i}{x}{e}}} \hfill

%% Actual typing rules - \Infer{\Jtyper{\tau}{\Type{\ell+1}} \ + \Infer{\Jcic{\tau}{\Type{\ell+1}} \ \tau = \Tmarw{_}{_}{\Type{\ell}} \ \forall i. \ - \Jtyper[\Gamma,x:\tau]{c_i}{\Type{\ell}} \ - \JIcon[{x};x] {c_i} %% \ + \Jcic[\Gamma,x:\tau]{c_i}{\Type{\ell}} \ + \JIcon[x;x] {c_i} %% \ %% \ell_i < \ell } - {\Jtyper{\Tind{x}{\tau}{\vec c}}{\tau}} + {\Jcic{\Tind{x}{\tau}{\vec c}}{\tau}}

- \Infer{\Jtyper e {\tau_e} \ + \Infer{\Jcic e {\tau_e} \ \tau_e = {\tau_I~{\vec p}} \ \tau_I = \Tind{x}{\Tmarw{z}{\tau_z}{s}}{\vec c} \ - \Jtyper {\tau_r}~{\Tmarw{z}{\tau_z}{\Tsarw{\tau_I~\vec z}s}} \\ + \Jcic {\tau_r}~{\Tmarw{z}{\tau_z}{\Tsarw{\tau_I~\vec z}s}} \\ \forall i. \ c_i = {\Tmarw{y}{\tau_y}{x~\vec {p'}}} \ - \Jtyper {b_i} + \Jcic {b_i} {\Tmarw{y}{\Subst{\tau_y}{x}{\tau_I}} {\tau_r~\vec {p'}~{(\Tcon{i}{\tau_I}~\vec y)}}}} - {\Jtyper{\TIcase{\tau_r}{e}{\tau_e}{\vec b}}{\tau_r~{\vec p}~e}} + {\Jcic{\TIcase{\tau_r}{e}{\tau_e}{\vec b}}{\tau_r~{\vec p}~e}}

- \Infer{\Jtyper \tau s \ - \Jtyper[\Gamma,x_f:\tau] e \tau \ + \Infer{\Jcic \tau s \ + \Jcic[\Gamma,x_f:\tau] e \tau \ e = \Tmlam{y}{_}{\Tlam {x_i} {_} {e_b}} \ i = |y| \ - \Jdecreasing{\emptyset}{e_b}} - {\Jtyper {\Tfix{i}{x_f}{\tau}{e}} {\tau}} + \JUdecreasing{\emptyset}{e_b}} + {\Jcic {\Tfix{i}{x_f}{\tau}{e}} {\tau}} \end{mathpar}

\begin{mathpar} %% Primitive reductions \Infer{ }{ - \Jstep{\TIcase{\tau_r}{(\Tapp{\Tcon{i}{e}}{\vec e})}{\tau_e}{\vec b}} + \JIstep{\TIcase{\tau_r}{(\Tapp{\Tcon{i}{e}}{\vec e})}{_}{\vec b}} {\Tapp{b_i}{\vec e}}}

\Infer{i < |\vec e| \ e_i = \Tcon{_}{_} \ e = \Tfix{i}{x}{\tau}{e_f}} { - \Jstep{\Tapp{e}{\vec e}} + \JIstep{\Tapp{e}{\vec e}} {\Tapp{(\Subst{e_f}{e}{x})}{\vec e}}} \end{mathpar}

@@ -1029,27 +1319,27 @@ which is sound and complete. \begin{mathpar} \ovalbox{\ensuremath{ \begin{array}[b]{l|l} - \JIpos e & \text{$e$ is positive in $\nu$} \ + \JIpos e & \text{$e$ is positive in $x$} \ \JIcon e & - \text{$e$ is the type of a constructor of x, - positive in $\nu$} + \text{$e$ is the type of a constructor of $y$, + positive in $x$} \end{array} }} \vspace{-15pt} \hfill \\

%% Positivity - %% FIXME: For the CUC->CIC translation to work, we'll need to extend - %% \JIpos so Ind(y)<e> is considered positive in x if x occurs - %% positively inside it! - \Infer{x \in \nu \ \nu \cap \kw{fv}(\vec e) = \emptyset}{\JIpos {\Tapp x {\vec e}}} + \Infer{x \not\in \kw{fv}(\vec e)}{\JIpos {\Tapp x {\vec e}}}

- \Infer{\JIpos e \ \nu \cap \kw{fv}(\tau) = \emptyset}{\JIpos {\Tarw y \tau e}} + \Infer{\JIpos e \ x \not\in \kw{fv}(\tau)}{\JIpos {\Tarw y \tau e}}

- \Infer{\nu \cap \kw{fv}(\vec e) = \emptyset \ \forall i. \ \JIcon[{y}\cup\nu;y] {c_i}} + \Infer{x \not\in \kw{fv}(\vec e) \ x \not\in \kw{fv}(\tau) \ + \forall i. \ \JIcon[x;y] {c_i}} {\JIpos {\Tapp{(\Tind{y}{\tau}{\vec c})}{\vec e}}}

- \Infer{\nu \cap \kw{fv}(\vec e) = \emptyset}{\JIcon {\Tapp x {\vec e}}} + \\

- \Infer{\JIcon e \ \nu \cap \kw{fv}(\tau) = \emptyset}{\JIcon {\Tarw y \tau e}} + \Infer{x \not\in \kw{fv}(\vec e)}{\JIcon {\Tapp y {\vec e}}} + + \Infer{\JIcon e \ x \not\in \kw{fv}(\tau)}{\JIcon {\Tarw z \tau e}}

\Infer{\JIcon e \ \JIpos \tau}{\JIcon {\Tsarw \tau e}} \end{mathpar} @@ -1057,7 +1347,7 @@ which is sound and complete. \begin{mathpar} \ovalbox{\ensuremath{ \begin{array}[b]{l|l} - \Jdecreasing \nu e & + \JIdecreasing \nu e & \text{$i^{th}$ arg of $x_f$ always smaller than $x_i$ in $e$, given that $\nu$ are smaller} \end{array} @@ -1066,50 +1356,50 @@ which is sound and complete.

\iflongversion %% Uninteresting congruence rules - \Infer{\Jdecreasing \nu \tau \ \Jdecreasing \nu e} - {\Jdecreasing \nu {\Tlam x \tau e}} + \Infer{\JIdecreasing \nu \tau \ \JIdecreasing \nu e} + {\JIdecreasing \nu {\Tlam x \tau e}}

- \Infer{\Jdecreasing \nu \tau \ \Jdecreasing \nu e} - {\Jdecreasing \nu {\Tarw x \tau e}} + \Infer{\JIdecreasing \nu \tau \ \JIdecreasing \nu e} + {\JIdecreasing \nu {\Tarw x \tau e}}

- \Infer{\Jdecreasing \nu \tau \ \Jdecreasing \nu e} - {\Jdecreasing \nu {\Tfix{i'}{x}{\tau}{e}}} + \Infer{\JIdecreasing \nu \tau \ \JIdecreasing \nu e} + {\JIdecreasing \nu {\Tfix{i'}{x}{\tau}{e}}}

- \Infer{\Jdecreasing \nu {e_1} \ \Jdecreasing \nu {e_2}} - {\Jdecreasing \nu {\Tapp{e_1}{e_2}}} + \Infer{\JIdecreasing \nu {e_1} \ \JIdecreasing \nu {e_2}} + {\JIdecreasing \nu {\Tapp{e_1}{e_2}}}

- \Infer{\Jdecreasing \nu e \ - \Jdecreasing \nu {\tau_r} \ - %% \Jdecreasing \nu {\tau_e} \ - \Jdecreasing \nu {\vec b}} - {\Jdecreasing \nu {\TIcase{\tau_r}{e}{\tau_e}{\vec b}}} + \Infer{\JIdecreasing \nu e \ + \JIdecreasing \nu {\tau_r} \ + \JIdecreasing \nu {\tau_e} \ + \JIdecreasing \nu {\vec b}} + {\JIdecreasing \nu {\TIcase{\tau_r}{e}{\tau_e}{\vec b}}} \else \fi

\Infer{x_f \not\in \kw{fv}(e)} - {\Jdecreasing \nu {e}} + {\JIdecreasing \nu {e}}

- \Infer{\Jdecreasing \nu {\vec e} \ + \Infer{\JIdecreasing \nu {\vec e} \ i < |e| \ e_i = \Tapp{x}{\vec {e'}} \ x \in \nu} - {\Jdecreasing \nu {\Tapp{x_f}{\vec e}}} + {\JIdecreasing \nu {\Tapp{x_f}{\vec e}}}

- %% The rule for the impredicative case! - \Infer{\Jdecreasing \nu e \ - \Jdecreasing \nu {\tau_r} \ - e = \Tapp{x_e}{\vec _} \ - %% \Jdecreasing \nu {\tau_e} \ + %% The rule for the predicative case! + \Infer{\JIdecreasing \nu e \ + \JIdecreasing \nu {\tau_r} \ + \JIdecreasing \nu {\tau_e} \\ + e = \Tapp{x_e}{\vec _} \ x_e \in \nu \cup { x_i } \ \forall i. \ b_i = \Tmlam{y}{_}{e_i} \ - \Jdecreasing {\nu \cup \vec y} {b_i}} - {\Jdecreasing \nu {\TIcase{\tau_r}{e}{\tau_e}{\vec b}}} + \JIdecreasing {\nu \cup \vec y} {b_i}} + {\JIdecreasing \nu {\TIcase{\tau_r}{e}{\tau_e}{\vec b}}}

%% The rule for the impredicative case! - %% \Infer{\Jdecreasing \nu e \ - %% \Jdecreasing \nu {\tau_r} \ - %% \Jdecreasing \nu {\tau_e} \\ + %% \Infer{\JIdecreasing \nu e \ + %% \JIdecreasing \nu {\tau_r} \ + %% \JIdecreasing \nu {\tau_e} \\ %% e = \Tapp{x_e}{\vec _} \ %% x_e \in \nu \cup { x_i } \ %% \tau_e = {\tau_I~{\vec _}} \ @@ -1118,32 +1408,32 @@ which is sound and complete. %% b_i = \Tmlam{y}{_}{e_i} \ %% c_i = \Tmarw{_}{\tau_i}{_} \ %% \nu' = {~ y_j ~|~ \tau_{ij} = \Tapp{x_I}{\vec _} ~} \ - %% \Jdecreasing {\nu \cup \nu'} {b_i}} - %% {\Jdecreasing \nu {\TIcase{\tau_r}{e}{\tau_e}{\vec b}}} + %% \JIdecreasing {\nu \cup \nu'} {b_i}} + %% {\JIdecreasing \nu {\TIcase{\tau_r}{e}{\tau_e}{\vec b}}} \end{mathpar}

%% Reduction rules %% \begin{mathpar} %% %% Congruence rules - %% \Infer{\Jstep{\tau}{\tau'} \ + %% \Infer{\JIstep{\tau}{\tau'} \ %% |\vec c| = |\vec {c'}| \ - %% \forall i. \ \Jstep{c_i}{c'_i}} - %% {\Jstep{\Tind{x}{\tau}{\vec c}}{\Tind{x}{\tau'}{\vec {c'}}}} + %% \forall i. \ \JIstep{c_i}{c'_i}} + %% {\JIstep{\Tind{x}{\tau}{\vec c}}{\Tind{x}{\tau'}{\vec {c'}}}}

- %% \Infer{\Jstep{e}{e'}} - %% {\Jstep{\Tcon{i}{e}}{\Tcon{i}{e'}}} + %% \Infer{\JIstep{e}{e'}} + %% {\JIstep{\Tcon{i}{e}}{\Tcon{i}{e'}}}

- %% \Infer{\Jstep{e}{e'} \ - %% \Jstep{\tau}{\tau'}} - %% {\Jstep{\Tfix{i}{x}{\tau}{e}}{\Tfix{i}{x}{\tau'}{e'}}} + %% \Infer{\JIstep{e}{e'} \ + %% \JIstep{\tau}{\tau'}} + %% {\JIstep{\Tfix{i}{x}{\tau}{e}}{\Tfix{i}{x}{\tau'}{e'}}}

- %% \Infer{\Jstep{e}{e'} \ - %% \Jstep{\tau_r}{\tau'_r} \ - %% \Jstep{\tau_e}{\tau'_e} \ + %% \Infer{\JIstep{e}{e'} \ + %% \JIstep{\tau_r}{\tau'_r} \ + %% \JIstep{\tau_e}{\tau'_e} \ %% |\vec b| = |\vec {b'}| \ %% \forall i. \ - %% \Jstep{b_i}{b'_i}} - %% {\Jstep{\TIcase{\tau_r}{e}{\tau_e}{\vec b}} + %% \JIstep{b_i}{b'_i}} + %% {\JIstep{\TIcase{\tau_r}{e}{\tau_e}{\vec b}} %% {\TIcase{\tau'_r}{e'}{\tau'_e}{\vec b'}}} %% \end{mathpar}

@@ -1191,7 +1481,7 @@ system differs from that of~\citet{Gimenez94} in the following aspects: termination judgment; \item Our rules are extended to a tower of universes; \item The typing rule of \kw{Ind} enforces predicativity; -\item Giménez does not have the \kw{Ind} rule of $\JIpos e$; which allows to +\item Giménez does not include the \kw{Ind} rule of $\JIpos e$; which allows to define for example an inductive type $t$ where one of the fields has type $\id{List}~t$. Most proof assistants allow such a relaxation of the positivity requirement; @@ -1216,28 +1506,79 @@ in~\cite{Coquand92}: \end{displaymath}

- -\subsection{CIC} - -\begin{figure} - FIXME! - \caption{Calculus of Inductive Constructions} - \label{fig:cic} -\end{figure} - -Figure~\ref{fig:cic} shows the typing rules of the traditional -presentation of CIC, mostly following the presentation of \citet{Gimenez94}. - \subsection{CUC to CIC}

+\newcommand \TIeither[2] {\id{Either}~#1~#2} +\newcommand \TIUnit {\id{Unit}} +\newcommand \TIunit {\id{unit}} +\newcommand \TIPair[3] {\Sigma #1:#2. #3} +\newcommand \TIpair[2] {\id{dcons}~#1~#2} +\newcommand \TIproj[2] {\pi_{#1}~#2} + \begin{figure} Tags are erased, union types are converted to tagged sums, and \kw{weaken} replaced by a chunk of code - + \begin{displaymath} + \begin{array}{l@{;=;}l} + \Ftocic x & x \ + \Ftocic {\Tlam{x}{\tau}{e}} & \Tlam{x}{\Ftocic {\tau}}{\Ftocic {e}} \ + \Ftocic {\Tapp{e_1}{e_2}} & \Tapp{\Ftocic {e_1}}{\Ftocic {e_2}} \ + \Ftocic {\Tarw{x}{\tau_1}{\tau_2}} & \Tarw{x}{\Ftocic {\tau_1}}{\Ftocic {\tau_2}} + \medskip \ + \Ftocic {\Tuple \EmptyCtx} & \TIUnit \ + \Ftocic {\Tuple {x:\tau,\Delta}} & \TIPair{x}{\tau}{\Ftocic {\Tuple \Delta}} \ + \Ftocic {\tuple \Delta {\cdot}} & \TIunit \ + \Ftocic {\tuple \Delta {e,\vec e}} & \TIpair e {\Ftocic {\tuple \Delta {\vec e}}}\ + \Ftocic {\Tproj e 0} & \TIproj 1 {\Ftocic {e}} \ + \Ftocic {\Tproj e i} & \TIproj 2 {\Ftocic {\Tproj e {i - 1}}} \ + \Ftocic {\Tapp{(\Tlam x {\tau} {e_1})}{\Tproj {e_2} 0}} & + %% FIXME: We don't have enough type annotations in CUC to + %% fill the type annotations in CIC! + \TIcase {\Tlam _ _ ?} {e_2} {?} + {\Tlam x \tau {\Tlam {x_2} _ {e_1}}} \ + \Ftocic {\Tapp{(\Tlam x {\tau} {e_1})}{\Tproj {e_2} i}} & + \TIproj 2 {\Ftocic {\Tproj e {i - 1}}} + \medskip \ + \Ftocic {\id{Eq}} & \id{Eq} \ + \Ftocic {\id{refl}} & \id{refl} \ + \Ftocic {J} & J + \medskip \ + \Ftocic {\Tmu[i]{x}{\tau}{e}} & \Tfix{i}{x}{\tau}{e} \ + \Ftocic {\Tmu{x}{\tau}{(\Tmlam y \tau e)}} & + \Tind{x}{\tau}{\Tmarw y \tau {e\to \Tapp x {\vec y}}} \ + \Ftocic {\Tfold \tau {\vec p} e} & \Tcon{\Ftocic {\tau}}{0}~{\vec p}~e \ + \Ftocic {\Tunfold{\tau}{\vec p} e} & + \Ftocic {\Tapp{(\Tlam x {\Tapp{\tau}{\vec p}} x)}{(\Tunfold{\tau}{\vec p} e)}} \ + \Ftocic {\Tapp{(\Tlam x \tau {e_1})}{(\Tunfold{\tau}{\vec p} e)}} & + \TIcase{?}{e}{\Tapp{\tau}{\vec p}}{\Tmlam y {\tau_y} {\Tlam x x}} \ + \medskip \ + \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}} & + \Tapp{\Ftocic{\Jsubtype{\tau_1}{\tau_2}}}{\Ftocic {e}} \ + \Ftocic { + \MAlign[c]{ + \TUcase {e} {\tau_e \} {\Ttagvar}{x}{e_\Ttagvar \}{y}{e_d} + }} & FIXME \ + \end{array} + \end{displaymath} + Inductive types get turned into tuples, tags, explicit equality proofs, + and unions; case turns into case plus field extraction plus equality casts + \caption{Mapping CUC to CIC} \label{fig:cuc-to-cic} \end{figure}

+The first question about CUC is whether this calculus is sound, meaning that +if we consider it as a logic, we want to know that this logic is consistent. +Rather than show it directly we do it by reducing the problem to that of the +consistency of CIC. More specifically, we present a translation $\Ftocic \cdot$ +which takes any expression of CUC and translates it to an equivalent +expression in CIC; then we show that this translation is type preserving, +and then we use this result to show that there can only be a proof of $\bot$ in +CUC if there is a proof of $\bot$ in CIC. + If we have forall $e$ and $\tau$, $\Jcuc e \tau$ then $\Jcic {\Ftocic e} {\Ftocic \tau}$.

@@ -1245,36 +1586,46 @@ Corollary: CUC is as sound as CIC in the sense that there is an $e$ such that $\Jcuc e \bot$ only if there's a $e'$ such that $\Jcic {e'} \bot$, because $\Ftocic \bot = \bot$.

-\subsection{CIC to CUC} +\FIXME{Second take:} + +We define a translation function $\Ftocic\cdot$ which takes a derivation +$\Jcuc{e}{\tau}$ and returns an equivalent expression $e'$ in CIC. As an abuse +of notation, we will often write $\Ftocic e$ instead of $\Ftocic{\Jcuc{e}{\tau}}$. + +\begin{lemma} + Type Preserving translation: Given $\Jcuc e \tau$, we have $\Jcuc \tau s$ and + $\Jcic[\Ftocic{\Gamma}] {\Ftocic{\Jcuc e \tau}}{\Ftocic{\Jcuc \tau s}}$. +\end{lemma} +\begin{proof} + It's easy to show that given $\Jcuc e \tau$ we have $\Jcuc \tau s$, by induction + on the derivation. The remaining part of the proof is longer but is also + done by induction on the derivation. It requires proving several side + lemmas such as the fact that a strictly positive recursive type is + translated to a strictly positive inductive type, same for terminating + recursive functions, as well as the fact that $\JUstepr{e}{e'}$ implies + $\JIstepr{\Ftocic e}{\Ftocic{e'}}$, which itself requires proving that + reduction preserves types. +\end{proof} + +\begin{corollary} + Relative consistency: Assuming there is no $e$ in CIC such that + $\Jcic[\EmptyCtx]{e}{\bot}$, then there is no $e$ in CUC such that + $\Jcuc[\EmptyCtx]{e}{\bot}$. +\end{corollary} +\begin{proof} + Since $\Ftocic{\Jcuc \bot {\Type 1}} = \bot$ and $\Ftocic{\EmptyCtx} = + \EmptyCtx$, we have that $\Jcuc[\EmptyCtx] e \bot$ implies + $\Jcic[\EmptyCtx]{\Ftocic{\Jcuc e \bot}}\bot$, so any proof of $\bot$ in CUC can be + used to find a proof of $\bot$ in CIC. +\end{proof}

-\newcommand \TIeither[2] {\id{Either}~#1~#2} -\newcommand \TIPair {\Sigma} -\newcommand \TIpair {\id{dcons}} +\subsection{CIC to CUC}

\begin{figure} - \begin{displaymath} - \begin{array}{l@{;=;}l} - \Ftocuc x & x \ - \Ftocuc {\Tlam{x}{\tau}{e}} & \Tlam{x}{\Ftocuc {\tau}}{\Ftocuc {e}} \ - \Ftocuc {\Tapp{e_1}{e_2}} & \Tapp{\Ftocuc {e_1}}{\Ftocuc {e_2}} \ - \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{S.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, - and unions; case turns into case plus field extraction plus equality casts + FIXME!

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

If we have $\Jcic e \tau$ then $\Jcuc {\Ftocuc e} {\Ftocuc \tau}$. @@ -1291,7 +1642,6 @@ judgments into the logic: $\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$. - FIXME: I think we can actually do it and still show equivalence to CIC! \item \kw{case}'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} @@ -1302,6 +1652,7 @@ judgments into the logic: \nocite{Blume06,Castagna16} %Union types and extensible sums \nocite{Chapman10} %Levitation \nocite{Christiansen16} %Idris's use in elaboration +\nocite{Firsov18} %Cedille

\section{Conclusion}

View it on GitLab: https://gitlab.com/monnier/typer/commit/3bcb7c68278104d50f1f82fd827e19fc0f3c...