Stefan pushed to branch report/itd at Stefan / Typer
Commits: 4cba1d88 by Stefan Monnier at 2018-10-09T04:00:37Z -
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -541,7 +541,7 @@ Fig.~\ref{fig:tagged-terms} shows the typing rules for tagged terms.
\newcommand \TUnion[1] {#1~\cup~} \newcommand \TUnionSmart[1] {#1~\cup'~} -\newcommand \TUweaken {\kw{weaken}~} +\newcommand \TUweaken[1] {\id{Sub.weaken}~#1~} \newcommand \TUcase[6] {\kw{case}~#1~|~#2~#3~P_{#3}~\Rightarrow #4~|~#5~P_{#5}~\Rightarrow #6}
\newcommand \JSplit[3] {#2 \Longleftarrow #1~/\Ttagvar \Longrightarrow #3} @@ -555,23 +555,32 @@ Fig.~\ref{fig:tagged-terms} shows the typing rules for tagged terms. \begin{array}{lc@{;;}c@{;;}l} \textit{(term)} & e,\tau &::=& ... ~\MAlign{ - |~ !FIXME! + |~ \TUnion{\tau_1}{\tau_2} \ + !FIXME! } \ \end{array} \end{displaymath}
- \begin{mathpar} - \Infer{ }{\Jsubtype \tau \tau} - - \Infer{\Jsubtype {\tau_1} \tau \ - \Jsubtype {\tau_2} \tau} - {\Jsubtype {\TUnion{\tau_1}{\tau_2}} \tau} - - \Infer{\Jsubtype \tau {\tau_i}} - {\Jsubtype \tau {\TUnion{\tau_1}{\tau_2}}} - \end{mathpar} + \begin{displaymath} + \begin{array}{l@{;:;}l} + %% \multicolumn 1 l {_{\subseteq}_ \hfill :} & + _{\subseteq}_ & \Type{\ell_1}\to\Type{\ell_2}\to\Type{\ell_1 \sqcup \ell_2} \ + _\cup_ & \Type{\ell_1}\to\Type{\ell_2}\to\Type{\ell_1 \sqcup \ell_2} \medskip \ + \id{Sub.refl} & \Jsubtype \tau \tau \ + \id{Sub.left} & + \Jsubtype{\tau_1}{\tau_2} \to \Jsubtype{\tau_1}{\TUnion{\tau_2}{\tau_3}} \ + \id{Sub.right} & + \Jsubtype{\tau_1}{\tau_2} \to \Jsubtype{\tau_1}{\TUnion{\tau_3}{\tau_2}} \ + \id{Sub.both} & + \Jsubtype{\tau_1}{\tau_3} \to \Jsubtype{\tau_2}{\tau_3} \to + \Jsubtype{\TUnion{\tau_1}{\tau_2}}{\tau_3} \ + \id{Sub.weaken} & \Jsubtype{\tau_1}{\tau_2} \to \tau_1 \to \tau_2 \ + %% + \end{array} + \end{displaymath}
\begin{mathpar} + %% FIXME: Make it return the \Jsubtype proofs! \Infer[U-order1]{ }{\JOrder{\TTag{\tau}}{\TTag{\tau}}{\bot}}
\Infer[U-order2] @@ -595,24 +604,13 @@ Fig.~\ref{fig:tagged-terms} shows the typing rules for tagged terms. \end{mathpar}
\begin{mathpar} - \Infer[U-form] - {\Jtyper {\tau_1} {\Type {\ell_1}} \ - \Jtyper {\tau_2} {\Type {\ell_2}}} - {\Jtyper {\TUnion{\tau_1}{\tau_2}} - {\Type{(\Tmax{\ell_1}{\ell_2})}}} - - \Infer[U-intro] - {\Jtyper e {\tau_1} \ - \Jsubtype {\tau_1} {\tau_2}} - {\Jtyper {\TUweaken{e}} {\tau_2}} - - %% FIXME: Allow dependent elimination! \Infer[U-elim] {\Jtyper e {\tau_u} \ \JOrder {\tau_u} {\TTag{\tau_\Ttagvar}} {\tau_d} \ - \Jtyper[\Gamma,x:{{\TTag{\tau_\Ttagvar}}},P_x:(e \equiv \TUweaken x)] + %% FIXME: Args to TUweaken! + \Jtyper[\Gamma,x:{{\TTag{\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[\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}
@@ -978,13 +976,27 @@ presentation of CIC, mostly following the presentation of \citet{Gimenez94}. \end{figure}
If we have forall $e$ and $\tau$, -$\Jcuc e \tau$ then $\Jcic {\Ftocic e} {\Ftocic \tau}$ (and -vice versa, hopefully). +$\Jcuc e \tau$ then $\Jcic {\Ftocic e} {\Ftocic \tau}$.
+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}
+\newcommand \TIeither[2] {\id{Either}~#1~#2} + \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}} \ + \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
@@ -992,20 +1004,35 @@ vice versa, hopefully). \label{fig:cic-to-cuc} \end{figure}
-If we have $\Jcic e \tau$ then $\Jcuc {\Ftocuc e} {\Ftocuc \tau}$ -(and vice versa, hopefully). +If we have $\Jcic e \tau$ then $\Jcuc {\Ftocuc e} {\Ftocuc \tau}$. + +\section{Extensions}
+The language can be made more general by reifying some of the auxiliary +judgments into the logic: +\begin{itemize} +\item $\mu f$ can take a proof argument of type + $\Tapp{\id{strictly-positive}}{f}$ (which makes it possible to define + inductive types parameterized over type constructors that have to + themselves be strictly positive) or of type + $\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}
\section{Related works}
-\nocite{Gimenez94,Blume06,Castagna16} +\nocite{Gimenez94,Blume06,Castagna16,Levitation}
\section{Conclusion}
\begin{acks} This work was supported by the \grantsponsor{NSERC}{Natural Sciences and Engineering Research Council of Canada}{http://nserc-crsng.gc.ca/%7D grant - No.~\grantnum{NSERC}{298311/2012}. Any opinions, findings, and + N$^o$~\grantnum{NSERC}{298311/2012}. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the NSERC. \end{acks}
View it on GitLab: https://gitlab.com/monnier/typer/commit/4cba1d8828ac289800254044e38ccd1889d6...
Afficher les réponses par date