Stefan pushed to branch report/itd at Stefan / Typer
Commits: cba8406c by Stefan Monnier at 2018-10-05T21:13:49Z -
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -143,7 +143,7 @@ and sums rather than the other way around. The resulting language is lower-level yet we show it to be equivalent to (a predicative version of) the Calculus of Inductive Constructions. An additional benefit is that - it can also conveniently give a precise type to the default branch of + it can conveniently give a precise type to the default branch of \kw{case} statements. \end{abstract}
@@ -291,7 +291,7 @@ Contributions: \begin{figure} \begin{displaymath} \begin{array}{lc@{;;}c@{;;}l} - \textit{(var)} & x &\in& \mathcal{V} \ + \textit{(var)} & x,y,t &\in& \mathcal{V} \ \textit{(level)} & \ell &\in& \mathbb{N} \ \textit{(ctxt)} & \Gamma,\Delta &::=& \EmptyCtx ~|~ \Gamma,x:\tau \ \textit{(sort)} & s &::=& \Type \ell \ @@ -473,16 +473,29 @@ Fig.~\ref{fig:tuples} shows the typing rules for tagged tuples. \newcommand \Tuntag {\kw{untag}~}
\begin{figure} + + \begin{displaymath} + \begin{array}{lc@{;;}c@{;;}l} + \textit{(label)} & l &\in& \mathcal{L} \ + \textit{(term)} & e,\tau &::=& + ... ~\MAlign{ + |~ \TTag{\tau} + ~|~ \Ttag e + ~|~ \Tuntag{e} + } \ + \end{array} + \end{displaymath} + \begin{mathpar} - \Infer[N-form] + \Infer%% [N-form] {\Jtyper \tau {\Type \ell}} {\Jtyper {\TTag \tau} {\Type \ell}}
- \Infer[N-intro] + \Infer%% [N-intro] {\Jtyper e \tau} {\Jtyper {\Ttag e} {\TTag \tau}}
- \Infer[N-elim] + \Infer%% [N-elim] {\Jtyper {\Ttag e} {\TTag \tau}} {\Jtyper {\Tuntag e} \tau} \end{mathpar} @@ -508,6 +521,9 @@ Fig.~\ref{fig:tagged-terms} shows the typing rules for tagged terms. \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} @@ -534,6 +550,16 @@ Fig.~\ref{fig:tagged-terms} shows the typing rules for tagged terms. \newcommand \Jsubtype [1] {#1~\subseteq~}
\begin{figure} + + \begin{displaymath} + \begin{array}{lc@{;;}c@{;;}l} + \textit{(term)} & e,\tau &::=& + ... ~\MAlign{ + |~ !FIXME! + } \ + \end{array} + \end{displaymath} + \begin{mathpar} \Infer{ }{\Jsubtype \tau \tau}
@@ -598,6 +624,58 @@ Fig.~\ref{fig:unions} shows our typing rules for unions. Our unions are unusual in that the subterms that make up the type cannot be arbitrary types, to make sure we can apply \kw{case} to them.
+\section{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}} + +\begin{figure} + \begin{displaymath} + \begin{array}{lc@{;;}c@{;;}l} + \textit{(index)} & i &\in& \mathbb{N} \ + \textit{(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} + %% FIXME: Define pos (will require something like `con`) + \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} \ + e = \Tmlam{y}{_}{e_b} \ + i < |y| \ + \Jterm[x;i;y_i]{\emptyset}{e_b}} + {\Jtyper{\Tmu[i]{x}{\tau}{e}}{\tau}} + + \Infer{\Jtyper{e}{\Tapp{\tau}{\vec p}} \ + \tau = \Tmu{x}{_}{e_\tau}} + {\Jtyper{\Tunfold{e}}{\Tapp{(\Subst{e_\tau}{\tau}{x})}{\vec p}}} + + \Infer{\Jtyper{e}{\Tapp{(\Subst{e_\tau}{\tau}{x})}{\vec p}} \ + FIXME! \ + \tau = \Tmu{x}{_}{e_\tau}} + {\Jtyper{\Tfold{e}}{\Tapp{\tau}{\vec p}}} + + FIXME! + \end{mathpar} + \caption{Recursive definitions} + \label{fig:recurse} +\end{figure} + \section{Erasure}
The intention of our calculus is for \kw{weaken} to have no run time cost. @@ -664,11 +742,11 @@ which is sound and complete. {\Jtyper{\TIcase{\tau_r}{e}{\tau_e}{\vec b}}{\tau_r~{\vec p}~e}}
\Infer{\Jtyper \tau s \ - \Jtyper[\Gamma,x:\tau] e \tau \ - e = \Tmlam{z}{_}{\Tlam y {_} {e_b}} \ - i = |z| \ + \Jtyper[\Gamma,x_f:\tau] e \tau \ + e = \Tmlam{y}{_}{\Tlam {x_i} {_} {e_b}} \ + i = |y| \ \Jdecreasing{\emptyset}{e_b}} - {\Jtyper {\Tfix{i}{x}{\tau}{e}} {\tau}} + {\Jtyper {\Tfix{i}{x_f}{\tau}{e}} {\tau}} \end{mathpar}
\begin{mathpar} @@ -831,8 +909,8 @@ follows: } \ \end{array} \end{displaymath} -where $\Tind{x}{\tau}{\vec c}$ is an inductive type of kind $\tau$ and with $|\vec c|$ -constructors where $c_i$ gives the type of each constructor; \ +where $\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 @@ -840,7 +918,7 @@ inductive type; for an object built with 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}$ -is defines a recursive function which performs a structural +defines a recursive function which performs a structural induction on its $i^{th}$ argument.
Figure~\ref{fig:inductive} shows the new typing rules and reduction rules @@ -849,18 +927,22 @@ enforce that inductive types are indeed inductive and that recursive definitions are terminating. Beside the slightly different syntax, our system differs from that of~\citet{Gimenez94} in the following aspects: \begin{itemize} +\item We omitted the obvious congruence rules for the $\leadsto$ relation and the + 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 define for example an inductive type $t$ where one of the fields has type - $\id{List}~t$. Most proof assistants allow such a rule; + $\id{List}~t$. Most proof assistants allow such a relaxation of the + positivity requirement; \item The termination check on \kw{Case} is simpler in that it considers all fields of an object to be smaller than the object analyzed, whereas Giménez limits this to the fields which are in a \emph{recursive position}. \end{itemize} Giménez needs this additional restriction because his \kw{Set} universe is -impredicative, so he needs to disallow recursions such as: +impredicative, so he needs to disallow recursions such as the one hinted at +in~\cite{Coquand92}: \begin{displaymath} \MAlign{ D = \Tind{D}{\kw{Set}}{\Tsarw{(\Tarw{t}{\kw{Set}}{\Tsarw{t}{t}})}{D}}; \
View it on GitLab: https://gitlab.com/monnier/typer/commit/cba8406c5a9725a6108cef1a9ff26d68311b...