[Git][monnier/typer][report/itd] -
Stefan pushed to branch report/itd at Stefan / Typer Commits: 40e74549 by Stefan Monnier at 2018-10-10T20:15:50Z - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -72,8 +72,6 @@ \newcommand \Jtyper[2][\Gamma] {#1 \vdash #2~:~} \newcommand \Type[1] {\kw{Type}_{#1}} \newcommand \Ttagvar {l} -\newcommand \Tuple[2][\Ttagvar] {\kw{Tuple}_{#1}(#2)} -\newcommand \tuple[2][\Ttagvar] {\kw{tuple}_{#1}^{#2}} \newcommand \Tarw[2] {(#1\:#2)\to} \newcommand \Tmarw[2] {\overrightarrow{(#1\:#2)}\to} \newcommand \Tsarw[1] {#1\to} @@ -239,8 +237,8 @@ The contributions of this article are: \item A kind of case-analysis construct where the default branch also gets refined type information witnessing in an efficient way precise information about the branches already tested. -\item A proof of equivalence of this language with the Calculus of Inductive - Constructions, showing it enjoys the same meta-theoretic properties. +\item A proof of equivalence of this language with (a predicative version + of) the Calculus of Inductive Constructions. \end{itemize} \section{Background} @@ -492,31 +490,75 @@ Fig.~\ref{fig:sums} shows the usual typing rules for tagged sums. \newpage \section{Tuples} -\newcommand \Tcons[2]{#1 \to #2} +\newcommand \Tuple[2][\Ttagvar] {\kw{Tuple}~{#1}~#2} +\newcommand \tuple[2][\Ttagvar] {\kw{tuple}_{#1}^{#2}} +\newcommand \TLabel {\id{Label}} +\newcommand \Tsel {\pi} \begin{figure} - \begin{mathpar} - \Infer[T-base]{ }{\Jtyper {\Tuple \EmptyCtx}{\Type 0}} - - \Infer[T-field] - {\Jtyper {\Tuple \Delta}{\Type {\ell_1}} \\ - \Jtyper[\Gamma,\Delta] \tau {\Type {\ell_2}}} - {\Jtyper {\Tuple {\Delta,x\:\tau}}{\Type {(\Tmax{\ell_1}{\ell_2})}}} - - \Infer[TC-base] { }{\Jtyper \EmptyCtx \EmptyCtx} - - \Infer[TC-field] - {\Jtyper {\vec e} {\Delta} \\ - \Jtyper e {\tau_i[{\vec e}/\Delta]}} - {\Jtyper {\vec e, e_i} {\Delta, x\:\tau_i}} + \begin{displaymath} + \begin{array}{l@{\;:\;}l} + \TLabel & \Type 0; \\ + %% `Tcons Int Tnil : Types 0` comparable to `cons Int nil : list Type₀` + %% `list Int : Type₀` and `list Type₀ : Type₁` so `Types 0 : Type₁`! + \id{Types}~\ell & \Type {\ell+1}; \\ + \id{Tnil} & \id{Types}~0; \\ + \id{Tcons} & + \MAlign{\Tarw{t}{\Type{\ell_1}} + {\Tsarw{(\Tsarw{t}{\id{Types}~{\ell_2}})} + {}} \\ + \;\;\id{Types}~{(\Tmax{\ell_1}{\ell_2});}} \medskip \\ + \id{Values} & \Tsarw{\id{Types}~\ell}{\Type {\ell}}; \\ + \id{Vnil} & \id{Values}~{\id{Tnil}}; \\ + \id{Vcons} & + \MAlign{ + \Tarw{x}{\tau}{\Tsarw{\id{Values}~{(f~x)}}{}} \\ + \;\; \id{Values}~{(\id{Tcons}~\tau~f)}; + } \medskip \\ + \Tuple[]{} & \TLabel \to \id{Types}~\ell \to \Type \ell; \\ + \end{array} + \end{displaymath} + + \begin{displaymath} + %% FIXME: `Tnth` isn't be a function since it's only defined if + %% the index is within bounds! + \MAlign{ + %% FIXME: Mutual recursion, yuck! + \id{nth} : (n:\id{Nat})\to(x:\tau:\id{Types}~\ell)\to\id{Tnth}~x~n~0~\tau \\ + \id{Tnth}~x~0~i~(\id{Tcons}~\tau~f) = \tau \\ + \id{Tnth}~x~(s~n)~i~(\id{Tcons}~\tau~f) = \\ + \;\;\;\; + \id{Tnth}~x~n~(s~i)~(f~(\id{nth}~i~x)) + } + \end{displaymath} - \Infer[T-intro] - {\Jtyper{\Tuple \Delta}{\Type \ell} \\ - \Jtyper{\vec e}{\Delta}} - {\Jtyper{\tuple \Delta (\vec e)} {\Tuple \Delta}} + \begin{mathpar} + %% \Infer[T-base]{ }{\Jtyper {\Tuple \EmptyCtx}{\Type 0}} + %% + %% \Infer[T-field] + %% {\Jtyper {\Tuple \Delta}{\Type {\ell_1}} \\ + %% \Jtyper[\Gamma,\Delta] \tau {\Type {\ell_2}}} + %% {\Jtyper {\Tuple {\Delta,x\:\tau}}{\Type {(\Tmax{\ell_1}{\ell_2})}}} + %% + %% \Infer[TC-base] { }{\Jtyper \EmptyCtx {\id{Tup.Tnil}}} + + %% \Infer[TC-field] + %% {\Jtyper {\vec e} {\Delta} \\ + %% \Jtyper e {\tau_i[{\vec e}/\Delta]}} + %% {\Jtyper {\vec e, e_i} {\Delta, x\:\tau_i}} + %% \Infer[TC-field] + %% {\Jtyper {\vec e} {\Delta} \\ + %% \Jtyper e {\tau_i[{\vec e}/\Delta]}} + %% {\Jtyper {e, \vec e} {\id{Tup.Tcons}~\tau~f}} + + \Infer{\Jtyper{\Ttagvar}{\TLabel} \\ + \Jtyper{\tau}{\id{Types}~\ell} \\ + \Jtyper{\id{Vcons}~e_0~(..(\id{Vcons}~e_n~\id{Vnil})..)} + {\id{Values}~\tau}} + {\Jtyper{\tuple~\tau~\vec e} {\Tuple \tau}} \Infer[T-proj] - {\Jtyper{e}{\Tuple {x_0\:\tau_0,..,x_i\:\tau_i,\Delta}}} + {\Jtyper{e}{\Tuple \tau}} {\Jtyper{\Tproj e i}{\tau_i[{\Tproj e 0,..,\Tproj e {i\!-\!1}}/x_0,..,x_{i\!-\!1}]}} \end{mathpar} \caption{Tuples} @@ -624,12 +666,12 @@ Fig.~\ref{fig:tagged-terms} shows the typing rules for tagged terms. \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} & + \_{\subseteq}\_ & \Type{\ell_1}\to\Type{\ell_2}\to\Type{\Tmax{\ell_1}{\ell_2}} \\ + \_\cup\_ & \Type{\ell_1}\to\Type{\ell_2}\to\Type{\Tmax{\ell_1}{\ell_2}} \medskip \\ + \id{Sub.refl}\;\tau & \Jsubtype \tau \tau \\ + \id{Sub.left}\;\tau_3 & \Jsubtype{\tau_1}{\tau_2} \to \Jsubtype{\tau_1}{\TUnion{\tau_2}{\tau_3}} \\ - \id{Sub.right} & + \id{Sub.right}\;\tau_3 & \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 @@ -1046,6 +1088,8 @@ $\Ftocic \bot = \bot$. \subsection{CIC to CUC} \newcommand \TIeither[2] {\id{Either}~#1~#2} +\newcommand \TIPair {\Sigma} +\newcommand \TIpair {\id{dcons}} \begin{figure} \begin{displaymath} @@ -1056,8 +1100,14 @@ $\Ftocic \bot = \bot$. \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}} \\ - \Ftocuc {\id{Sub.refl}{e}} & \Tapp{\Ftocuc {P}}{\Ftocuc {e}} \\ + %% \Ftocuc {\id{Sub.refl}{e}} & \\ \Ftocuc {\TUweaken{P}{e}} & \Tapp{\Ftocuc {P}}{\Ftocuc {e}} \\ + \Ftocuc {\id{Tup.Types}~\ell} & \Type~\ell \\ + \Ftocuc {\id{Tup.Tnil}} & \id{True} \\ + \Ftocuc {\id{Tup.Tcons}} & \TIPair \\ + \Ftocuc {\id{Tup.Values}} & \Tlam{x}{\Type \ell}{x} \\ + \Ftocuc {\id{Tup.Vnil}} & I \\ + \Ftocuc {\id{Tup.Vcons}} & \TIpair \\ \end{array} \end{displaymath} Inductive types get turned into tuples, tags, explicit equality proofs, View it on GitLab: https://gitlab.com/monnier/typer/commit/40e745495eace8f3ec3ef4dc31d5ec90b77f... -- View it on GitLab: https://gitlab.com/monnier/typer/commit/40e745495eace8f3ec3ef4dc31d5ec90b77f... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
participants (1)
-
Stefan