Stefan pushed to branch report/itd at Stefan / Typer
Commits: 711697c7 by Stefan Monnier at 2018-10-05T19:20:19Z -
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -51,8 +51,7 @@ \usepackage{mathpartir} \usepackage{mdframed,empheq} \usepackage{parskip} - -\citestyle{acmauthoryear} %% For author/year citations +\usepackage{fancybox} %For \ovalbox
%% The doc says `vcenter` should work, but I get an error :-( %% \newcommand \Infer[1][] [\inferrule*[vcenter,right=#1]] @@ -86,7 +85,7 @@
\newcommand \Jcuc[2][\Gamma] {#1 \vdash_U #2 :} \newcommand \Jcic[2][\Gamma] {#1 \vdash_I #2 :} -\newcommand \Jconv[1] {#1 ;\simeq; } +\newcommand \Jstep[1] {#1 ;\leadsto; }
\newcommand \MetaFunction[2] {\llbracket #2 \rrbracket_{#1}} \newcommand \Ftocic {\MetaFunction{I}} @@ -94,6 +93,8 @@
\newcommand \MAlign[1]{\begin{array}[t]{@{}l@{}} #1 \end{array}}
+\newif \iflongversion + \begin{document}
\title{Inductive types deconstructed} @@ -352,9 +353,9 @@ Figure~\ref{fig:ccw} shows our base language \CCw{} as a pure type system à la ECC~\cite{Luo89}.
While inductive types have non-trivial interactions with impredicativity, -they are orthogonal to our work, so contrary to most other presentations, we -did not include an impredicative universe at the bottom in order to keep the -presentation simpler. +they are largely orthogonal to our work, so contrary to most other +presentations, we did not include an impredicative universe at the bottom in +order to keep the presentation simpler.
\newpage \section{Dependent pairs} @@ -618,9 +619,9 @@ which is sound and complete. ~\kw{of}~\langle#4\rangle} \newcommand \Tfix[3] {\kw{Fix}_{#1}~#2:#3~=~}
-\newcommand \JIcon[2][x] {#1 \vdash #2;;\kw{con}} -\newcommand \JIpos[2][x] {#1 \vdash #2;;\kw{pos}} -\newcommand \Jdecreasing[3][x_f,i,x_i] {#1,#2 \vdash #3~\kw{term}} +\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 \BT[2] {\id{BT}\llbracket #1 \rrbracket_{#2}}
\begin{figure*} @@ -628,42 +629,34 @@ which is sound and complete.
%% Typing rules \begin{mathpar} - %% 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 \not\in \kw{fv}(\vec e)}{\JIpos {\Tapp x {\vec e}}} - - \Infer{\JIpos e \ x \not\in \kw{fv}(\tau)}{\JIpos {\Tarw y \tau e}} - - \Infer{x \not\in \kw{fv}(\vec e)}{\JIcon {\Tapp x {\vec e}}} - - \Infer{\JIcon e \ x \not\in \kw{fv}(\tau)}{\JIcon {\Tarw y \tau e}} - - \Infer{\JIcon e \ \JIpos \tau}{\JIcon {\Tsarw \tau e}} + \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'$} + \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
%% Actual typing rules \Infer{\Jtyper{\tau}{\Type{\ell+1}} \ \tau = \Tmarw{_}{_}{\Type{\ell}} \ - \forall i \ + \forall i. \ \Jtyper[\Gamma,x:\tau]{c_i}{\Type{\ell}} \ - \JIcon {c_i} %% \ + \JIcon[{x};x] {c_i} %% \ %% \ell_i < \ell } {\Jtyper{\Tind{x}{\tau}{\vec c}}{\tau}}
- %% 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}}} - \Infer{\Jtyper 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}} \\ - \forall i \ + \forall i. \ c_i = {\Tmarw{y}{\tau_y}{x~\vec {p'}}} \ \Jtyper {b_i} {\Tmarw{y}{\Subst{\tau_y}{x}{\tau_I}} @@ -676,42 +669,101 @@ which is sound and complete. i = |z| \ \Jdecreasing{\emptyset}{e_b}} {\Jtyper {\Tfix{i}{x}{\tau}{e}} {\tau}} + \end{mathpar} + + \begin{mathpar} + %% Primitive reductions + \Infer{ }{ + \Jstep{\TIcase{\tau_r}{(\Tapp{\Tcon{i}{e}}{\vec e})}{\tau_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}} + {\Tapp{(\Subst{e_f}{e}{x})}{\vec e}}} + \end{mathpar} + + %% \caption{Typing rules of inductive types} + %% \label{fig:inductive-wf} + %% \end{figure*} + + %% \begin{figure*} + \begin{mathpar} + \ovalbox{\ensuremath{ + \begin{array}[b]{l|l} + \JIpos e & \text{$e$ is positive in $\nu$} \ + \JIcon e & + \text{$e$ is the type of a constructor of x, + positive in $\nu$} + \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{\JIpos e \ \nu \cap \kw{fv}(\tau) = \emptyset}{\JIpos {\Tarw y \tau e}} + + \Infer{\nu \cap \kw{fv}(\vec e) = \emptyset \ \forall i. \ \JIcon[{y}\cup\nu;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{\JIcon e \ \JIpos \tau}{\JIcon {\Tsarw \tau e}} + \end{mathpar} + + \begin{mathpar} + \ovalbox{\ensuremath{ + \begin{array}[b]{l|l} + \Jdecreasing \nu e & + \text{$i^{th}$ arg of $x_f$ always smaller than $x_i$ + in $e$, given that $\nu$ are smaller} + \end{array} + }} \vspace{-15pt} \hfill \\ %% Decreasing recursive calls - \Infer{x_f \not\in \kw{fv}(e)} - {\Jdecreasing \nu {e}} - + + \iflongversion + %% Uninteresting congruence rules \Infer{\Jdecreasing \nu \tau \ \Jdecreasing \nu e} {\Jdecreasing \nu {\Tlam x \tau e}} - + \Infer{\Jdecreasing \nu \tau \ \Jdecreasing \nu e} {\Jdecreasing \nu {\Tarw x \tau e}} - + \Infer{\Jdecreasing \nu \tau \ \Jdecreasing \nu e} {\Jdecreasing \nu {\Tfix{i'}{x}{\tau}{e}}} - + \Infer{\Jdecreasing \nu {e_1} \ \Jdecreasing \nu {e_2}} {\Jdecreasing \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}}} + \else \fi
+ \Infer{x_f \not\in \kw{fv}(e)} + {\Jdecreasing \nu {e}} + \Infer{\Jdecreasing \nu {\vec e} \ i < |e| \ e_i = \Tapp{x}{\vec {e'}} \ x \in \nu} {\Jdecreasing \nu {\Tapp{x_f}{\vec e}}}
- \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}}} - %% The rule for the impredicative case! \Infer{\Jdecreasing \nu e \ \Jdecreasing \nu {\tau_r} \ - \Jdecreasing \nu {\tau_e} \\ e = \Tapp{x_e}{\vec _} \ + %% \Jdecreasing \nu {\tau_e} \ + \\ x_e \in \nu \cup { x_i } \ - \forall 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}}} @@ -724,7 +776,7 @@ which is sound and complete. %% x_e \in \nu \cup { x_i } \ %% \tau_e = {\tau_I~{\vec _}} \ %% \tau_I = \Tind{x_I}{_}{\vec c} \ - %% \forall i \ + %% \forall i. \ %% b_i = \Tmlam{y}{_}{e_i} \ %% c_i = \Tmarw{_}{\tau_i}{_} \ %% \nu' = {~ y_j ~|~ \tau_{ij} = \Tapp{x_I}{\vec _} ~} \ @@ -733,38 +785,35 @@ which is sound and complete. \end{mathpar}
%% Reduction rules - \begin{mathpar} - %% Congruence rules - \Infer{\Jconv{\tau}{\tau'} \ - |\vec c| = |\vec {c'}| \ - \forall i \ \Jconv{c_i}{c'_i}} - {\Jconv{\Tind{x}{\tau}{\vec c}}{\Tind{x}{\tau'}{\vec {c'}}}} - - \Infer{\Jconv{e}{e'}} - {\Jconv{\Tcon{i}{e}}{\Tcon{i}{e'}}} - - \Infer{\Jconv{e}{e'} \ - \Jconv{\tau}{\tau'}} - {\Jconv{\Tfix{i}{x}{\tau}{e}}{\Tfix{i}{x}{\tau'}{e'}}} - - \Infer{\Jconv{e}{e'} \ - \Jconv{\tau_r}{\tau'_r} \ - \Jconv{\tau_e}{\tau'_e} \ - |\vec b| = |\vec {b'}| \ - \forall i \ - \Jconv{b_i}{b'_i}} - {\Jconv{\TIcase{\tau_r}{e}{\tau_e}{\vec b}} - {\TIcase{\tau'_r}{e'}{\tau'_e}{\vec b'}}} - - %% Primitive reductions - FIXME!! - \end{mathpar} - + %% \begin{mathpar} + %% %% Congruence rules + %% \Infer{\Jstep{\tau}{\tau'} \ + %% |\vec c| = |\vec {c'}| \ + %% \forall i. \ \Jstep{c_i}{c'_i}} + %% {\Jstep{\Tind{x}{\tau}{\vec c}}{\Tind{x}{\tau'}{\vec {c'}}}} + + %% \Infer{\Jstep{e}{e'}} + %% {\Jstep{\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{\Jstep{e}{e'} \ + %% \Jstep{\tau_r}{\tau'_r} \ + %% \Jstep{\tau_e}{\tau'_e} \ + %% |\vec b| = |\vec {b'}| \ + %% \forall i. \ + %% \Jstep{b_i}{b'_i}} + %% {\Jstep{\TIcase{\tau_r}{e}{\tau_e}{\vec b}} + %% {\TIcase{\tau'_r}{e'}{\tau'_e}{\vec b'}}} + %% \end{mathpar} + \caption{Inductive types} \label{fig:inductive} \end{figure*}
-We add inductive types following the presentation of \citet{Gimenez94} +We add inductive types following the style of \citet{Gimenez94} which separates induction into case analysis and recursive definitions, combined with a syntactic check that the recursive calls corresponds to a structural induction. The syntax of the base language is extended as @@ -782,6 +831,47 @@ 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; \ +$\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 +arguments that were passed to the constructor; \ +and finally $\Tfix{i}{x}{\tau}{e}$ +is 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 +introduced for those inductive types, as well as new auxiliary judgments to +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 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; +\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: +\begin{displaymath} + \MAlign{ + D = \Tind{D}{\kw{Set}}{\Tsarw{(\Tarw{t}{\kw{Set}}{\Tsarw{t}{t}})}{D}}; \ + d = \Tcon{0}{D}~\id{identity}; \ + \id{f} = \MAlign{ + \Tfix{0}{f}{\Tsarw{D}{\bot}}{} \ + ;;\Tlam{d}{D}{\TIcase{\Tlam{_}{D}\bot}{d}{}{\Tlam{id}{_}{f~(id~D~d)}}}; + }\ + \id{oops} = f~d; + } +\end{displaymath}
View it on GitLab: https://gitlab.com/monnier/typer/commit/711697c7360aa454dfdd51437b08903745fe...
Afficher les réponses par date