Stefan pushed to branch report/itd at Stefan / Typer
Commits: 6fa653a8 by Stefan Monnier at 2018-11-14T19:43:05Z -
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -489,13 +489,17 @@ reduction rule for CUC resp.~CIC. \newcommand \TLabel {\id{Label}} %% \newcommand \Tsel {\pi}
+\newcommand \Teq[1] {#1 \equiv} +\newcommand \Trefl {\kw{refl}~} +\newcommand \TJ[2] {\kw{J}~#1~#2~} + \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} + \kw{switch}~#2~|~#4~#5~#5_\equiv\Rightarrow #6~|~#7~#7_\equiv\Rightarrow #8}
\newcommand \Tmu[4][] {\mu_{#1} #2:#3 . #4} \newcommand \Tfold[2] {\kw{fold}~#1~#2~} @@ -520,6 +524,8 @@ The syntax of the complete language is the following: ~|~ \Tarw x {\tau_1} {\tau_2} \ \multicolumn 3 r {|~} & \Tuple \Delta ~|~ \tuple \Delta {\vec e} ~|~ \Tproj e i \ + \multicolumn 3 r {|~} & + \Teq{e_1}{e_2} ~|~ \Trefl{e} ~|~ \TJ{e_\equiv}{e_f}{e} \ \multicolumn 3 r {|~} & \TUnion{\tau_1}{\tau_2} ~|~ \TUcast{\tau_1}{\tau_2}e @@ -531,16 +537,18 @@ The syntax of the complete language is the following: ~|~ \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. +The terms are spread over 5 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 equality types, +the fourth shows the terms of the union types, +and the last shows the terms of the recursive functions and recursive types.
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. +orthogonal and are themselves simpler or more general.
%% \newpage \subsection{Labeled tuples} @@ -688,45 +696,49 @@ later parts of our system break it anyway. %% \newpage \subsection{Equality}
+\newcommand\FigEquality { +\begin{figure}[b] + \begin{mathpar} + \Infer{\Jtype{e_1}{\tau} \ \Jtype{e_2}{\tau} \ \Jtype{\tau}{\Type\ell}} + {\Jtype{\Teq{e_1}{e_2}}{\Type\ell}} + + \Infer{\Jtype{e}{\tau}} + {\Jtype{\Trefl{e}}{\Teq{e}{e}}} + + \Infer{\Jtype{e_\equiv}{\Teq{e_1}{e_2}} \ + \Jtype{\Tapp{e_f}{e_1}}{s} \ + \Jtype{e}{\Tapp{e_f}{e_1}}} + {\Jtype{\TJ{e_\equiv}{e_f}{e}}{\Tapp{e_f}{e_2}}} + \end{mathpar} + \caption{Typing rules of the equality types} + \label{fig:equality} +\end{figure} +} + +\FigEquality + 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 +In 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 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: +with an equality type: \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}} - ;} + \begin{array}{lc@{;;}c@{;;}l} + \textsl{(term)} & e,\tau &::=& + ... ~|~ \Teq{e_1}{e_2} ~|~ \Trefl{e} ~|~ \TJ{e_\equiv}{e_f}{e} \end{array} \end{displaymath} -\id{Eq} is the type constructor for this new equality type; \id{refl} is 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. - -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: +$\equiv$ is the type constructor for this new equality type; \id{refl} is the +corresponding introduction form, and \kw{J} its eliminator which encodes the +Leibniz equality. Figure~\ref{fig:equality} shows the corresponding +typing rules. +%% +The corresponding new primitive reduction rule is the following: \begin{mathpar} - \JUstep {J~_~_~_~_~_~(\id{refl}~_~_)~x}x + \JUstep {\TJ{(\Trefl{_})}{_}{x}}{x} \end{mathpar} where the underscores represent subterms which are ignored by the rule.
@@ -781,9 +793,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}},x_=:(e \equiv \TUcast{\tau_l}{\tau_e}{x})] + \Jcuc[\Gamma,x:{{\tau_\Ttagvar}},x_\equiv:(e \equiv \TUcast{\tau_l}{\tau_e}{x})] {e_\Ttagvar} {\tau_r} \ - \Jcuc[\Gamma,y:{\tau_d},y_=:(e \equiv \TUcast{\tau_d}{\tau_e}{y})] + \Jcuc[\Gamma,y:{\tau_d},y_\equiv:(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} @@ -860,7 +872,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'}{x_=,x} + \Subst{e_\Ttagvar}{\id{refl}~{\tau_e}~e, \TUcast {\tau}{\tau_l} e'}{x_\equiv,x} }}
\Infer{e = \TUcast {\tau}{\tau_e} e' \ @@ -871,7 +883,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'}}{y_=,y} + \Subst{e_d}{\id{refl}~{\tau_e}~e,\TUcast {\tau}{\tau_d} {e'}}{y_\equiv,y} }} %% \end{array} \end{mathpar} @@ -902,7 +914,7 @@ 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. In the switch branches, $x$/$x_=$ and $y$/$y_=$ are pairs of +data. In the switch branches, $x$/$x_\equiv$ and $y$/$y_\equiv$ 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$.
@@ -914,7 +926,7 @@ for \kw{cast}; the ``smart constructor'' $\TUnionSmart{\tau_1}{\tau_2}$ which i 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 +(weakened) tuples, which is indispensable at run-time so that 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 @@ -930,9 +942,9 @@ 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 the explicit equality proof bound to $x_=$ or $y_=$ witnessing -which branch was chosen +branches is the same: the type refinement used for dependent elimination is +replaced by the explicit equality proof bound to $x_\equiv$ or $y_\equiv$ 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 @@ -1186,7 +1198,7 @@ of the erased calculus are the following: }{ \Subst{e_\Ttagvar} {\id{refl},(\tuple \Delta {\vec e})} - {x_=,x} + {x_\equiv,x} } \end{array}
@@ -1199,7 +1211,7 @@ of the erased calculus are the following: }{ \Subst{e_d} {\id{refl},(\tuple[l'] \Delta {\vec e})} - {y_=,y} + {y_\equiv,y} } \end{array}
@@ -1218,13 +1230,15 @@ be implemented as no-ops: \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 $e \JUstepArw {e_1}$ then either ${\Erase e} = {\Erase + {e_1}}$ or ${\Erase e}\JEstepArw{\Erase {e_1}}$. \item If ${\Erase e}\JEstepArw{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 + The first part is proved by induction on the derivation of $e \JUstepArw + {e_1}$, \end{proof}
\section{Equivalence}
View it on GitLab: https://gitlab.com/monnier/typer/commit/6fa653a8a308c464e29534b48b345cc26fc8...