Stefan pushed to branch report/itd at Stefan / Typer

Commits: 5225f4b5 by Stefan Monnier at 2018-10-31T15:05:17Z -

- - - - -

2 changed files:

- .gitignore - paper.tex

Changes:

===================================== .gitignore ===================================== @@ -16,6 +16,13 @@ manual.?? *.info comment.cut

+# llncs2e's other files, not needed to build the article +llncs2e/fig1.eps +llncs2e/history.txt +llncs2e/readme.txt +llncs2e/samplepaper.tex +llncs2e/splncs04.bst + *_build/

# Random backup/autosave files

===================================== paper.tex ===================================== @@ -156,7 +156,7 @@ presentation of CIC's inductive types where the various elements are provided separately, such that inductive types are built on top of tuples and sums rather than the other way around. The resulting language is - lower-level yet we show it to be equivalent to (a predicative version of) + lower-level yet we show it to be equivalent to a predicative version of the Calculus of Inductive Constructions. An additional benefit is that it can conveniently give a precise type to the default branch of \kw{case} statements. @@ -251,8 +251,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 (a predicative version - of) the Calculus of Inductive Constructions. +\item A proof of equivalence of this language with a predicative version + of the Calculus of Inductive Constructions. \end{itemize}

\section{Background} @@ -407,6 +407,7 @@ it practical to provide this feature even if it is not used very often. \textsl{(level)} & \ell &\in& \mathbb{N} \ \textsl{(ctxt)} & \Gamma,\Delta &::=& \EmptyCtx ~|~ \Gamma,x:\tau \ \textsl{(sort)} & s &::=& \Type \ell \ + %% FIXME: Already give the full syntax here! \textsl{(term)} & e,\tau &::=& s ~|~ x ~|~ \Tlam x \tau e ~|~ \Tapp{e_1}{e_2} ~|~ \Tarw x {\tau_1} {\tau_2} \end{array} @@ -471,6 +472,10 @@ Figure~\ref{fig:ccw} shows our base language \CCw{} as a pure type system (PTS)~\cite{Barendregt91b}. It is a variant of CoC with a tower of universes à la ECC~\cite{Luo89}.

+%% FIXME: The issue is much more serious, since impredicativity almost +%% ends up introducing restrictions which prevent defining π₁ and/or π₂ +%% on impredicative sums, so it's far from clear how to turn a `case` into +%% a switch+projections in such a case! While inductive types have non-trivial interactions with impredicativity, those interactions are largely orthogonal to our work, so contrary to most other presentations, we did not include an impredicative universe at the @@ -569,7 +574,7 @@ reduction rule for CUC resp.~CIC.

\begin{figure} %% \begin{displaymath} - %% %% FIXME: `Tnth` isn't be a function since it's only defined if + %% %% FIXME: `Tnth` can't be a function since it's only defined if %% %% the index is within bounds! %% \MAlign{ %% %% FIXME: Mutual recursion, yuck! @@ -938,9 +943,6 @@ be simplified in the erasure semantics presented in Section~\ref{sec:erasure}.

-%% FIXME: reduction rules? Especially for the `weaken` thingy! - - \subsection{Recursion}

\newcommand \Tmu[4][] {\mu_{#1} #2:#3 . #4} @@ -1237,6 +1239,13 @@ be implemented as no-ops: \section{Equivalence} \label{sec:equivalence}

+%% FIXME: We have a problem with inductive types's universe level: CUC +%% does not let the user define Bool elsewhere than Type₀, whereas +%% the CIC presented does. +%% More specifically, in CIC-as-presented, the user can choose the universe +%% level of any Ind type, whereas in CUC-as-presented the user can choose it +%% for types that are recursive but not for those that aren't! + Now that we have defined a calculus which provides us with the intended run-time cost, we show that this calculus is sound and complete with respect to a more classic presentation of inductive types. We will first present @@ -1539,8 +1548,6 @@ in~\cite{Coquand92}: \Ftocic {\Tproj e 0} & \TIproj 1 {\Ftocic {e}} \ \Ftocic {\Tproj e i} & \TIproj 2 {\Ftocic {\Tproj e {i - 1}}} \ \Ftocic {\Tapp{(\Tlam x {\tau} {e_1})}{\Tproj {e_2} 0}} & - %% FIXME: We don't have enough type annotations in CUC to - %% fill the type annotations in CIC! \TIcase {\Tlam _ _ ?} {e_2} {?} {\Tlam x \tau {\Tlam {x_2} _ {e_1}}} \ \Ftocic {\Tapp{(\Tlam x {\tau} {e_1})}{\Tproj {e_2} i}} & @@ -1594,6 +1601,11 @@ $\Jcuc e \bot$ only if there's a $e'$ such that $\Jcic {e'} \bot$, because $\Ftocic \bot = \bot$.

\FIXME{Second take:} +%% This is much better, but we need to adjust the presentation accordingly: +%% - We can throw away some type annotations (yay!) +%% - We have to explain that while $\Ftocic\cdot$ is defined on derivations +%% we present it as if it was derived on the syntax of terms, to be +%% more concise.

We define a translation function $\Ftocic\cdot$ which takes a derivation $\Jcuc{e}{\tau}$ and returns an equivalent expression $e'$ in CIC. As an abuse @@ -1639,6 +1651,8 @@ If we have $\Jcic e \tau$ then $\Jcuc {\Ftocuc e} {\Ftocuc \tau}$.

\section{Extensions}

+%% FIXME: Generalize to impredicativity! + The language can be made more general by reifying some of the auxiliary judgments into the logic: \begin{itemize}

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