Stefan pushed to branch report/itd at Stefan / Typer

Commits: c856baf6 by Stefan Monnier at 2018-10-03T20:15:56Z -

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -74,7 +74,10 @@ \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} \newcommand \Tlam[2] {\lambda #1 : #2 .} +\newcommand \Tmlam[2] {\lambda \overrightarrow{#1 : #2} .} \newcommand \Tapp[1] {#1~} \newcommand \Tproj[1] {#1.} \newcommand \Tmax[1] {#1~\sqcup~} @@ -88,6 +91,8 @@ \newcommand \Ftocic {\MetaFunction{I}} \newcommand \Ftocuc {\MetaFunction{U}}

+\newcommand \MAlign[1]{\begin{array}[t]{@{}l@{}} #1 \end{array}} + \begin{document}

\title{Inductive types deconstructed} @@ -283,10 +288,12 @@ Contributions:

\begin{figure} \begin{displaymath} - \begin{array}{ll@{;;::=;;}l} - \textit{(contexts)} & \Gamma,\Delta & \EmptyCtx ~|~ \Gamma,x:\tau \ - \textit{(sorts)} & s & \Type \ell \ - \textit{(terms)} & e,\tau & s ~|~ x ~|~ \Tlam x \tau e ~|~ \Tapp{e_1}{e_2} + \begin{array}{lc@{;;}c@{;;}l} + \textit{(var)} & x &\in& \mathcal{V} \ + \textit{(level)} & \ell &\in& \mathbb{N} \ + \textit{(ctxt)} & \Gamma,\Delta &::=& \EmptyCtx ~|~ \Gamma,x:\tau \ + \textit{(sort)} & s &::=& \Type \ell \ + \textit{(term)} & e,\tau &::=& s ~|~ x ~|~ \Tlam x \tau e ~|~ \Tapp{e_1}{e_2} ~|~ \Tarw x {\tau_1} {\tau_2} \end{array} \end{displaymath} @@ -483,6 +490,34 @@ Fig.~\ref{fig:tuples} shows the typing rules for tagged tuples.

Fig.~\ref{fig:tagged-terms} shows the typing rules for tagged terms.

+\newpage +\section{Equality} + +\begin{figure} + \begin{displaymath} + \begin{array}{l@{;:;}l} + \id{Eq} & \Tarw{t}{\Type{}}{\Tarw {x,y} t {\Type{0}}}; \ + \id{refl} & \Tarw{t}{\Type{}}{\Tarw{x}{t}{\id{Eq}~t~x~x}}; \ + J & \MAlign{ + \Tarw{t}{\Type{}}{\Tarw {x,y} t {\Tarw u {\Type{}} {\Tarw + f {\Tsarw t u} {}}}} \ + \Tsarw{\id{Eq}~t~x~y}{\Tsarw{f~x}{f~y}} + ;} + \end{array} + \end{displaymath} + + %% With impredicativity we could define it as:\hfill\mbox{} + %% \begin{displaymath} + %% \begin{array}{l} + %% \id{Eq}~t~x~y = \Tarw u {\Type{}} {\Tarw + %% f {\Tsarw t u} {\Tsarw{f~x}{f~y}}}; \ + %% \id{refl}~t~x~=\Tlam u {\Type{}} {\Tlam f {(\Tsarw t u)} {\Tlam v {(f~x)} v}}; + %% \end{array} + %% \end{displaymath} + \caption{Equality type} + \label{fig:equality} +\end{figure} + \newpage \section{Unions}

@@ -574,6 +609,92 @@ run time cost, we show that this calculus shares all the other desirable characteristics of CIC by showing a translation between the two calculus which is sound and complete.

+\subsection{Inductive types} + +\newcommand \Tind[3] {\kw{Ind}(#1:#2)\langle#3\rangle} +\newcommand \Tcon[2] {\kw{Con}(#1,#2)} +\newcommand \Tcase[3] {{<}#1{>}\kw{Case}~#2~\kw{of}~\langle#3\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[5] {#1,#2,#3,#4 \vdash #5~\kw{decr}} +\newcommand \BT[2] {\id{BT}\llbracket #1 \rrbracket_{#2}} + +\begin{figure*} + %% Syntax + \begin{displaymath} + \begin{array}{lc@{;;}c@{;;}l} + \textit{(index)} & i &\in& \mathbb{N} \ + \textit{(term)} & e,\tau &::=& + ... ~\MAlign{ + |~ \Tind{x}{\tau}{\vec e} \ + |~ \Tcon{i}{e} \ + |~ \Tcase{\tau}{e}{\vec e} \ + |~ \Tfix{i}{x}{\tau}{e} + } \ + \end{array} + \end{displaymath} + + %% 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}} + + %% Actual typing rules + \Infer{\Jtyper{\tau}{\Type{\ell}} \ + \forall i \ + \Jtyper[\Gamma,x:\tau]{e_i}{\Type{\ell_i}} \ + \JIcon {e_i} \ + \ell_i < \ell} + {\Jtyper{\Tind{x}{\tau}{\vec e}}{\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 e} \ + \Jtyper e \tau} + {\Jtyper{\Tcon{i}{e}}{\Subst{e_i}{x}{e}}} + + \Infer{\Jtyper 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 \ + c_i = {\Tmarw{y}{\tau_y}{x~\vec {p'}}} \ + \Jtyper {b_i} + {\Tmarw{y}{\Subst{\tau_y}{x}{\tau_I}} + {\tau_r~\vec {p'}~{(\Tcon{i}{\tau_I}~\vec y)}}}} + {\Jtyper{\Tcase{\tau_r}{e}{\vec b}}{\tau_r~{\vec p}~e}} + + \Infer{\Jtyper \tau s \ + \Jtyper[\Gamma,x:\tau] e \tau \ + e = \Tmlam{z}{_}{\Tlam y {_} {e_b}} \ + i = |z| \ + \Jdecreasing{x}{i}{y}{\emptyset}{e_b}} + {\Jtyper {\Tfix{i}{x}{\tau}{e}} {\tau}} + \end{mathpar} + + %% Reduction rules + \begin{mathpar} + + \end{mathpar} + + \caption{Inductive types} + \label{fig:inductive} +\end{figure*} + + \subsection{CIC}

\begin{figure} @@ -590,13 +711,14 @@ presentation of CIC, mostly following the presentation of \citet{Gimenez94}. \begin{figure} Tags are erased, union types are converted to tagged sums, and \kw{weaken} replaced by a chunk of code - + \caption{Mapping CUC to CIC} \label{fig:cuc-to-cic} \end{figure}

-If we have $\Jcuc e \tau$ then $\Jcic {\Ftocic e} {\Ftocic \tau}$ -(and vice versa, hopefully). +If we have forall $e$ and $\tau$, +$\Jcuc e \tau$ then $\Jcic {\Ftocic e} {\Ftocic \tau}$ (and +vice versa, hopefully).

\subsection{CIC to CUC}

View it on GitLab: https://gitlab.com/monnier/typer/commit/c856baf64792c45b5b09b223301f60bc5f12...