[Git][monnier/typer][report/itd] -
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/} 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... -- View it on GitLab: https://gitlab.com/monnier/typer/commit/4cba1d8828ac289800254044e38ccd1889d6... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
participants (1)
-
Stefan