Stefan pushed to branch report/itd at Stefan / Typer

Commits: 6f6e3745 by Stefan Monnier at 2018-11-13T18:05:37Z -

- - - - -

2 changed files:

- paper.tex - refs.bib

Changes:

===================================== paper.tex ===================================== @@ -57,9 +57,23 @@ \usepackage{fancybox} %For \ovalbox \usepackage{natbib} \renewcommand \cite \citep

+\DeclareUnicodeCharacter{03A9}{\ensuremath{\Omega}} \DeclareUnicodeCharacter{03B1}{\ensuremath{\alpha}} +\DeclareUnicodeCharacter{03BB}{\ensuremath{\lambda}} +\DeclareUnicodeCharacter{03C3}{\ensuremath{\sigma}} +\DeclareUnicodeCharacter{03C4}{\ensuremath{\tau}} +\DeclareUnicodeCharacter{03C9}{\ensuremath{\omega}} +\DeclareUnicodeCharacter{0394}{\ensuremath{\Delta}} +\DeclareUnicodeCharacter{2081}{\ensuremath{_1}} +\DeclareUnicodeCharacter{2082}{\ensuremath{_2}} +\DeclareUnicodeCharacter{21D2}{\ensuremath{\Rightarrow}} +\DeclareUnicodeCharacter{21DB}{\ensuremath{\Rrightarrow}} +\DeclareUnicodeCharacter{2200}{\ensuremath{\forall}} \DeclareUnicodeCharacter{2203}{\ensuremath{\exists}} \DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}} +\DeclareUnicodeCharacter{2980}{\ensuremath{|||}} +\DeclareUnicodeCharacter{1D4B0}{\ensuremath{\mathcal{U}}} +\DeclareUnicodeCharacter{1D4C5}{\ensuremath{\wp}}

%% The doc says `vcenter` should work, but I get an error :-( %% \newcommand \Infer[1][] [\inferrule*[vcenter,right=#1]] @@ -78,7 +92,7 @@ \newcommand \CCw {CC$\omega$}

\newcommand \EmptyCtx {\bullet} -\newcommand \Jtyper[2][\Gamma] {#1 \vdash #2~:~} +\newcommand \Jtype[2][\Gamma] {#1 \vdash #2~:~} \newcommand \Type[1] {\kw{Type}_{#1}} \newcommand \Ttagvar {l} \newcommand \Tarw[2] {(#1:#2)\to} @@ -179,7 +193,7 @@ %% %% ... %% \end{CCSXML}

-\keywords{Inductive types, compilation, union types} +\keywords{Inductive types, compilation, union types, case analysis}

%% Note: \begin{abstract}...\end{abstract} environment must come %% before \maketitle command in ACM style. @@ -191,9 +205,9 @@

\section{Introduction}

-Typer is a functional language based on a pure type system, in the tradition -of Coq~\cite{Coq00}, Lean, and Agda~\cite{Bove09}, but focusing on programs -more than proofs, like Idris~\cite{Brady13}, F-star~\cite{Swamy16}, +Typer~\cite{Monnier19a} is a functional language based on a pure type system, +in the tradition of Coq~\cite{Coq00} and Agda~\cite{Bove09}, but focusing on +programs more than proofs, like Idris~\cite{Brady13}, F-star~\cite{Swamy16}, Zombie~\cite{Casinghino14}, and many others. Its design follows that of Scheme, in the sense that it intends to provide a minimalist core language on top of which a nice surface language can be built by metaprogramming. @@ -411,8 +425,7 @@ 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{The calculus of united constructions} -%% \subsection{Base calculus} +\subsection{The base calculus \CCw{}}

\begin{figure} \begin{displaymath} @@ -441,33 +454,33 @@ it practical to provide this feature even if it is not used very often. %% %% Context Rules %% \Infer{ }{\vdash \EmptyCtx} %% - %% \Infer{\vdash \Gamma \ \Jtyper \tau {\Type \ell}} + %% \Infer{\vdash \Gamma \ \Jtype \tau {\Type \ell}} %% {\vdash \Gamma,x:\tau} %% %% %% Term typing rules - %% \Infer{ }{\Jtyper{\Type \ell}{\Type {(\ell+1)}}} + %% \Infer{ }{\Jtype{\Type \ell}{\Type {(\ell+1)}}} %% - %% \Infer[(Var)]{\Gamma(x) = \tau}{\Jtyper x \tau} + %% \Infer[(Var)]{\Gamma(x) = \tau}{\Jtype x \tau} %% %% \Infer[(Lam)] - %% {\Jtyper{\tau_1}s \ \Jtyper[\Gamma,x:\tau_1]e{\tau_2}} - %% {\Jtyper{\Tlam x {\tau_1} e}{\Tarw{x}{\tau_1}{\tau_2}}} + %% {\Jtype{\tau_1}s \ \Jtype[\Gamma,x:\tau_1]e{\tau_2}} + %% {\Jtype{\Tlam x {\tau_1} e}{\Tarw{x}{\tau_1}{\tau_2}}} %% %% \Infer[(App)] - %% {\Jtyper{e_1}{\Tarw{x}{\tau_1}{\tau_2}} \ \Jtyper{e_2}{\tau_1}} - %% {\Jtyper{\Tapp {e_1} {e_2}}{\Subst{\tau_2}{e_2}{x}}} + %% {\Jtype{e_1}{\Tarw{x}{\tau_1}{\tau_2}} \ \Jtype{e_2}{\tau_1}} + %% {\Jtype{\Tapp {e_1} {e_2}}{\Subst{\tau_2}{e_2}{x}}} %% %% \Infer[(Arw)] %% {l = \Tmax{\ell_1}{\ell_2} \ - %% \Jtyper{\tau_1}{\Type{\ell_1}} \ - %% \Jtyper[\Gamma,x:\tau_1]{\tau_2}{\Type{\ell_2}}} - %% {\Jtyper{\Tarw x {\tau_1} {\tau_2}}{\Type \ell}} + %% \Jtype{\tau_1}{\Type{\ell_1}} \ + %% \Jtype[\Gamma,x:\tau_1]{\tau_2}{\Type{\ell_2}}} + %% {\Jtype{\Tarw x {\tau_1} {\tau_2}}{\Type \ell}} %% %% \Infer[(Conv)] - %% {\Jtyper e \tau \ + %% {\Jtype e \tau \ %% \tau \simeq \tau' \ - %% \Jtyper {\tau'} s} - %% {\Jtyper e {\tau'}} + %% \Jtype {\tau'} s} + %% {\Jtype e {\tau'}} %% %% %% Conversion rules, which double as reduction rules %% \Infer[($\beta$)]{ }{\Tapp{\Tlam x {e_1}}{e_2} \simeq \Subst{e_1}{e_2}x} @@ -476,119 +489,105 @@ 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. Figure~\ref{fig:ccw} shows our -%% FIXME: After adding the rest of the syntax, we'll need to update this. -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}. - -The different parts are not completely independent from each other, which -largely dictates the order in which they are presented, but to a first -approximation the base calculus can be replaced with any other -lambda calculus. -%% FIXME: The issue is much more serious, since impredicativity almost +Our calculus is built on top of a traditional $\lambda$-calculus, and to a first +approximation is independent from it, so we will use the same base calculus +for both the reference calculus of inductive constructions (CIC) as well as +our calculus of united constructions (CUC) which we present in the next few +sections in the form of a collection of extensions. 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}. We use the notation $\Tarw{x}{\tau_1}{\tau_2}$ +for the dependent function type, which can of course be shortened to +$\Tsarw{\tau_1}{\tau_2}$ when $x$ does not occur in $\tau_2$. We usually use the +metavariable $\tau$ to stand for a term which is supposed to be a type, +i.e. whose type is a sort. + +Because inductive types have non-trivial +interactions with impredicativity, we did not include an impredicative +universe at the bottom: all the calculi presented in this paper are +fully predicative. +%% FIXME: The issue is much quite serious, since impredicativity %% ends up introducing restrictions which prevent defining π₁ and/or π₂ %% on impredicative sums, so it's far from clear how to turn a `case` into -%% a switch+projections in such a case! -While inductive types have non-trivial interactions with impredicativity, -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 -(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{I}{\leadsto} e'$ when we talk about the +%% a switch+projections! Same for erasability: we'll probably need to add +%% some kind of `open..in..` construct as used in System-F for existential +%% types :-( + +The typing judgment of the base language is usually denoted $\Jtype 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{I}{\leadsto} e'$ when we talk about the reduction rule for CUC resp.~CIC.

-\Comment{ - \newpage - \subsection{Dependent pairs} - - \newcommand \TPair[2] {\Sigma#1:#2.} - \newcommand \Tpair[2] {\langle#1,#2\rangle} +\section{The calculus of united constructions} +%% \subsection{Base calculus}

- \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} +\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}

- Figure~\ref{fig:pairs} shows the usual typing rules for dependent pairs. -} +\newcommand \TUnion[1] {#1~\cup~} +\newcommand \TUnionSmart[1] {#1~\cup'~} +%% 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] { + \kw{switch}~#2~|~#4~#5~#5_=\Rightarrow #6~|~#7~#7_=\Rightarrow #8}

-\Comment{ - \newpage - \subsection{Tagged sums} +\newcommand \Tmu[4][] {\mu_{#1} #2:#3 . #4} +\newcommand \Tfold[2] {\kw{fold}~#1~#2~} +\newcommand \Tunfold[2] {\kw{unfold}~#1~#2~}

- \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} +Just like the full CIC, our new calculus is fairly large, so we present it +in several steps: the tuples, the equality type, the +sums, and finally the recursive definitions. +The different parts are not completely independent from each other, which +largely dictates the order in which they are presented.

- \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} +The syntax of the complete language is the following: +\begin{displaymath} + \begin{array}{lc@{;;}c@{;;}l} + \textsl{(var)} & x,y,t &\in& \mathcal{V} \ + \textsl{(level)} & \ell &\in& \mathbb{N} \ + \textsl{(label)} & l &\in& \mathcal{L} \ + \textsl{(index)} & i &\in& \mathbb{N} \ + \textsl{(sort)} & s &::=& \Type \ell \ + \textsl{(ctxt)} & \Gamma,\Delta &::=& \EmptyCtx ~|~ \Gamma,x:\tau \ + %% FIXME: Already give the full syntax here! + %% FIXME: Or maybe not, since this same base language is used for CIC! + \textsl{(term)} & e,\tau,p &::=& s ~|~ x ~|~ \Tlam x \tau e ~|~ \Tapp{e_1}{e_2} + ~|~ \Tarw x {\tau_1} {\tau_2} \ + \multicolumn 3 r {|~} & + \Tuple \Delta ~|~ \tuple \Delta {\vec e} ~|~ \Tproj e i \ + \multicolumn 3 r {|~} & + \TUnion{\tau_1}{\tau_2} + ~|~ \TUcast{\tau_1}{\tau_2}e + ~|~ {\MAlign{(\TUcase {e} {\tau_e} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d})}} \ + \multicolumn 3 r {|~} & + \Tmu[i]{x}{\tau}{e} + ~|~ \Tmu{x}{\tau}{e} + ~|~ \Tfold{\tau}{\vec p}{e} + ~|~ \Tunfold{\tau}{\vec p}{e} + \end{array} +\end{displaymath} +The terms are spread over 4 lines, where the first line reproduces the terms +of the base calculus, the second shows the terms of the tuple types, the +third shows the terms of the union types, and the last shows the terms of the +recursive functions and recursive types.

- Figure~\ref{fig:sums} shows the usual typing rules for tagged sums. -} +Clearly, this calculus is much larger than the base calculus. It is also +larger than the CIC: as often, there is a tension between keeping the +language small and making it efficient. The criteria which drove us to this +design favors a larger language as long as the different parts are +sufficiently orthogonal and are themselves simpler or more general.

%% \newpage -\subsection{Tuples} - -\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} +\subsection{Labeled tuples}

-\begin{figure} +\begin{figure}[tb] %% \begin{displaymath} %% %% FIXME: `Tnth` can't be a function since it's only defined if %% %% the index is within bounds! @@ -629,7 +628,7 @@ reduction rule for CUC resp.~CIC. n \ge i} {\Jcuc{\Tproj e i}{\tau_i[{\Tproj e 0,..,\Tproj e {i!-!1}}/x_0,..,x_{i!-!1}]}} \end{mathpar} - \caption{Tuples} + \caption{Typing rule of labeled tuples} \label{fig:tuples} \end{figure}

@@ -640,9 +639,12 @@ 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, and even in the -worst case it just adds one extra field to those heap objects. +worst case it just adds one extra field to those heap objects, which is +still much cheaper than the extra heap object and indirection introduced by +tagged sums.

-To that end, our language's syntax is extended as follows: +To add tuples to our base language, our language's syntax is extended as +follows: \begin{displaymath} %% \begin{array}{l@{;:;}l} %% \TLabel & \Type 0; \ @@ -666,17 +668,18 @@ To that end, our language's syntax is extended as follows: %% \end{array} \begin{array}{lc@{;;}c@{;;}l} \textsl{(label)} & l &\in& \mathcal{L} \ + \textsl{(index)} & i &\in& \mathbb{N} \ \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 language are -extended with the obvious congruence rules as well as the following -primitive reduction: +$\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 +introduction form which lets you actually build tuple values; and $\Tproj e i$ +is the eliminator which extracts the value of a given field. +Figure~\ref{fig:tuples} shows the 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} \JUstep{(\tuple \Delta {\vec e}).i}{e_i} \end{displaymath} @@ -719,16 +722,16 @@ later parts of our system break it anyway.

\begin{mathpar} \Infer%% [N-form] - {\Jtyper \tau {\Type \ell}} - {\Jtyper {\TTag \tau} {\Type \ell}} + {\Jtype \tau {\Type \ell}} + {\Jtype {\TTag \tau} {\Type \ell}}

\Infer%% [N-intro] - {\Jtyper e \tau} - {\Jtyper {\Ttag e} {\TTag \tau}} + {\Jtype e \tau} + {\Jtype {\Ttag e} {\TTag \tau}}

\Infer%% [N-elim] - {\Jtyper {\Ttag e} {\TTag \tau}} - {\Jtyper {\Tuntag e} \tau} + {\Jtype {\Ttag e} {\TTag \tau}} + {\Jtype {\Tuntag e} \tau} \end{mathpar} \caption{Tagged terms} \label{fig:tagged-terms} @@ -746,7 +749,7 @@ 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 +being predicative we don't 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 @@ -763,7 +766,7 @@ environment: \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 +corresponding introduction form, 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 often write $x \equiv y$ since $\tau$ can always be inferred from context. @@ -809,14 +812,6 @@ 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'~} -%% 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] { - \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}}

@@ -841,9 +836,9 @@ the explicit equality witnesses can be used to get the same effect. %% \Jcuc {\tau_e}{s} \ %% \Jcuc {\tau_r}{s} \ %% \tau_e = \TUnion{_}{_} \\ - \Jcuc[\Gamma,x:{{\tau_\Ttagvar}},P_x:(e \equiv \TUcast{\tau_l}{\tau_e}{x})] + \Jcuc[\Gamma,x:{{\tau_\Ttagvar}},x_=:(e \equiv \TUcast{\tau_l}{\tau_e}{x})] {e_\Ttagvar} {\tau_r} \ - \Jcuc[\Gamma,y:{\tau_d},P_y:(e \equiv \TUcast{\tau_d}{\tau_e}{y})] + \Jcuc[\Gamma,y:{\tau_d},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} @@ -920,7 +915,7 @@ the explicit equality witnesses can be used to get the same effect. \TUcase {e} {\tau_e} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} }{ - \Subst{e_\Ttagvar}{\id{refl}~{\tau_e}~e, \TUcast {\tau}{\tau_l} e'}{P_x,x} + \Subst{e_\Ttagvar}{\id{refl}~{\tau_e}~e, \TUcast {\tau}{\tau_l} e'}{x_=,x} }}

\Infer{e = \TUcast {\tau}{\tau_e} e' \ @@ -931,7 +926,7 @@ the explicit equality witnesses can be used to get the same effect. \TUcase {e}{\tau_e} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} }{ - \Subst{e_d}{\id{refl}~{\tau_e}~e,\TUcast {\tau}{\tau_d} {e'}}{P_y,y} + \Subst{e_d}{\id{refl}~{\tau_e}~e,\TUcast {\tau}{\tau_d} {e'}}{y_=,y} }} %% \end{array} \end{mathpar} @@ -962,7 +957,9 @@ 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. +data. In the switch branches, $x$/$x_=$ and $y$/$y_=$ are pairs of +variables which get bound to the value of $e$ strengthened to a more specific +type and to a proof that this new variable can indeed be weakened back to $e$.

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 @@ -989,7 +986,8 @@ 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. +replaced by the explicit equality proof bound to $x_=$ or $y_=$ 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 @@ -1001,11 +999,6 @@ Section~\ref{sec:erasure}.

\subsection{Recursion}

-\newcommand \Tmu[4][] {\mu_{#1} #2:#3 . #4} -\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}} @@ -1127,12 +1120,12 @@ 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: +two syntactically 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 &::=& + \textsl{(term)} & e,\tau,p &::=& ... ~\MAlign{ |~ \Tmu[i]{x}{\tau}{e} ~|~ \Tmu{x}{\tau}{e} \ @@ -1142,9 +1135,9 @@ two separate. Concretely, the syntax is extended as follows: \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 +$\Tmu{x}{\tau}{e}$ is the fixpoint construct that can be used to define +recursive types, as along as they obey the customary strict positivity +constraint; $\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 @@ -1161,11 +1154,12 @@ extended with the following primitive reduction: {\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: +the corresponding introduction, 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. +cause infinite unfoldings. This rule is directly adapted from the +corresponding one presented by \citet{Gimenez94}.

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 @@ -1185,13 +1179,14 @@ $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 +operations which return something smaller. Since it only keeps track 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 +smaller when those expressions 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. +differently for them. The reason for this irregularity 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} @@ -1255,7 +1250,7 @@ the following: }{ \Subst{e_\Ttagvar} {\id{refl},(\tuple \Delta {\vec e})} - {P_x,x} + {x_=,x} } \end{array}

@@ -1266,7 +1261,7 @@ the following: }{ \Subst{e_d} {\id{refl},(\tuple[l'] \Delta {\vec e})} - {P_y,y} + {y_=,y} } \end{array}

@@ -1531,13 +1526,13 @@ follows: } \ \end{array} \end{displaymath} -where $\Tind{x}{\tau}{\vec c}$ is an inductive type of kind $\tau$ with $|\vec c|$ +$\Tind{x}{\tau}{\vec c}$ is an inductive type of kind $\tau$ with $|\vec c|$ constructors where $c_i$ is the type of the $i^{th}$ constructor; \ $\Tcon{i}{e}$ is the $i^{th}$ constructor of the inductive type $e$; \ $\TIcase{\tau_r}{e}{\tau_e}{\vec b}$ performs case analysis on an object $e$ of inductive type; for an object built with the -$i^{th}$ constructor, branch $b_i$ will be called passing to it the +$i^{th}$ constructor, branch $b_i$ will be called, passing to it the arguments that were passed to the constructor; \ and finally $\Tfix{i}{x}{\tau}{e}$ defines a recursive function which performs a structural

===================================== refs.bib ===================================== @@ -1,5 +1,14 @@

+@techreport{Monnier19a, + author = {Stefan Monnier}, + institution = {Université de Montréal - DIRO}, + title = {Typer: ML boosted with type theory and Scheme}, + year = {2019}, + url = {https://www.iro.umontreal.ca/%5C~%7B%7Dmonnier/typer-overview- + 2019.pdf}, +} + @misc{Coq00, author = {Gérard P. Huet and Christine Paulin-Mohring and others}, @@ -296,7 +305,7 @@ booktitle = {Annual Symposium on Logic in Computer Science}, key = {LICS'89}, pages = {386-395}, - title = {ECC, an extended calculus of constructions}, + title = {ECC, an Extended Calculus of Constructions}, year = {1989}, }

View it on GitLab: https://gitlab.com/monnier/typer/commit/6f6e3745365e8793e79600828923ae2a87d0...