Stefan pushed to branch report/tcvi at Stefan / Typer

Commits: b3a46643 by Stefan Monnier at 2019-11-24T23:50:02Z -

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -301,7 +301,7 @@ inhabitants are all provably equal and hence erasable. For this reason, it is no ground breaking revelation to claim that there is an affinity between impredicativity and erasability, yet it is still unclear to what extent the two belong together nor which particular form of erasability would be the -true soulmate or impredicativity. +true soulmate of impredicativity.

Coq and the propositional resizing axiom basically link impredicativity to the concept of erasure usually called \emph{proof irrelevance}, where an @@ -317,12 +317,12 @@ with annotations of \emph{erasability}, and then show that all impredicative quantifications can be annotated as erasable.

Armed with this proverbial hammer, we then look at the two main limitations -of impredicative quantification in existing systems: the restriction (which -we call no-SELIT) which disallows strong elimination of large inductive -types in systems like Coq, and the fact that only the bottom universe can be -impredicative. We present how we could maybe replace those somewhat ad-hoc -restrictions with the arguably less ad-hoc restriction that impredicative -quantification is restricted to erasable quantification. +of impredicative quantification in existing systems: the restriction we call +no-SELIT (no strong elimination of large inductive types) in systems like +Coq, and the fact that only the bottom universe can be impredicative. +We present how we could maybe replace those somewhat ad-hoc restrictions +with the arguably less ad-hoc restriction that impredicative quantification +is restricted to erasable quantification.

%% a few other forms of impredicativity that are known to break consistency and %% argue that they look like nails: by restricting those forms of @@ -340,8 +340,8 @@ The contributions of this work are: types in the impredicative universe, all arguments to impredicative functions and all \emph{large} fields of inductive types are also erasable. -\item A new calculus ECIC which extends CIC with strong elimination of - large inductive types. +\item A new calculus ECIC which lifts the no-SELIT restriction, i.e.~it + extends CIC with strong elimination of large inductive types. \item A proof that the same idea does not directly make impredicativity in more than one universe consistent. \item An new calculus EpCCω with an impredicative universe polymorphism @@ -431,7 +431,8 @@ are \Char{\kw{e}}rasable. The syntax of the terms is defined as follows: \textsl{(sort)} & s &\in& \mathcal{S} \ \textsl{(argkind)} & k,c &::=& \kw{n} ~|~ \kw{e} \ \textsl{(term)} & e,\tau & ::= & s ~|~ x ~\MAlign{ - |~ \Arw{x}{\tau_1}{\tau_2} ~|~ \Lam{x}{\tau}{e} ~|~ \App{e_1}{e_2}} + |~ \Arw{x}{\tau_1}{\tau_2} ~|~ \Lam{x}{\tau}{e} ~|~ \App{e_1}{e_2}} \ + \textsl{(context)} & \Gamma &::=& \bullet ~|~ \Gamma,x:\tau \end{array} \end{displaymath} \FigEPTS @@ -499,7 +500,7 @@ This expresses the fact that erasable arguments do not influence evaluation. The domain of the erasure function is technically another language with a slightly different syntax, i.e. without erasability nor type annotations, but we will gloss over those details here since for the purpose of this -article we only really ever need to know if ``x \in $\kw{fv}(\Ferase e)$'' +article we only really ever need to know if ``$x \in \kw{fv}(\Ferase e)$'' rather than ``$\Ferase e$'' itself.

Since the new \textsc{e-Lam} rule is strictly more restrictive than the @@ -1231,7 +1232,7 @@ eCoq is left for future work.

Like most known consistent type systems that support impredicative definitions, CCω accepts them only in the bottom universe, called \kw{Prop} -(one counter example being arguably the $\lambda PRED\omega+$ presented +(one counter example being arguably the $\lambda\textrm{PRED}\omega^+$ presented in~\cite{Geuvers07}). This is a direct consequence of various paradoxes formalized in systems which allow impredicative definitions in more than one universe, such as those shown in \citet{Girard72}, \citet{Coquand94}, and @@ -1243,8 +1244,9 @@ universes as well.

\subsection{Erasing impredicative arguments in $\lambda U^-$}

-The last two showed a paradox in the system $\lambda U^-$ which is System-F$_\omega$ -extended with one extra rule. It can be defined as an EPTS as follows: +The last two papers referenced above showed a paradox in the system $\lambda U^-$ +which is System-F$_\omega$ extended with one extra rule. It can be defined as an +EPTS as follows: \begin{displaymath} \begin{array}{lcl} \mathcal{S} &=& {~ *,~\square,~\mathrm{\Delta} ~} \ @@ -1429,10 +1431,10 @@ any universe, which amounts to using the following Church-like encoding: \id{NatL} = (l : \kw{Level}) \to (a : \Type{l}) \to a \to (a \to a) \to a \end{displaymath} Such a definition is possible is systems like Agda which provide the -necessary universe polymorphism. We have not been able to find a clear -description of the rules used in Agda, but a first approximation of its -type system is described in Figure~\ref{fig:agda} where $\omega$ stands for the -smallest infinite ordinal. +necessary universe polymorphism (the $l$ above is a universe-level +variable). We have not been able to find a clear description of the rules +used in Agda, but a first approximation of its type system is described in +Figure~\ref{fig:agda} where $\omega$ stands for the smallest infinite ordinal.

So Agda would place the above universe-polymorphic definition of \id{NatL} squarely in the far away $\Type{\omega}$ universe. @@ -1467,7 +1469,7 @@ the universe level parameter $\ell$ needs to be erasable. \mathcal{S} &=& {~ \kw{Ul};~\Type \ell & \ell\in\mathbb{N}\cup{\omega} ~} \ \mathcal{A} &=& {~ (\kw{Level} : \kw{Ul});~ - (\Type \ell : \Type {\ell+1}) & \ell\in\mathbb{N} ~} \ + (\Type \ell : \Type {(\kw{s}~\ell)}) & \ell\in\mathbb{N} ~} \ \mathcal{R} &=& {~ (\kw{n}, l:\kw{Ul}, \Type{\ell}, \Type{\omega}) & \ell\in\mathbb{N}\cup{\omega} ~} \ @@ -1500,7 +1502,7 @@ is really meant to say something like: Now if we want to make this impredicative when $k = \kw{e}$, since $\ell$ can refer to $l$ we need to substitute $l$ with \emph{something} before we can use it in the sort of the product. For the \id{NatL} case, for example, $\ell$ -will be ``$l+1$'' and we argued that this product type should live in +will be ``$\kw{s}~l$'' and we argued that this product type should live in $\Type{0}$, so we would need to substitute $l$ with $-1$! Rather than argue why a negative value could make sense, we will use 0 in our rule: @@ -1550,7 +1552,11 @@ can try and compare it to existing systems. Then we define the encoding $\MetaFunction{}{\cdot}$ from System-F to EpCCω: \begin{displaymath} \begin{array}{r@{~=~}ll} - \MetaFunction{}{\bullet} & \bullet~;~\bullet \ + %% FIXME: This is visually ugly/illegible! + \multicolumn{2}{l}{ + \text{--- }\MetaFunction{}{\Gamma} \text{ returns a pair } \Gamma';\Delta \text{ ---}} \ + \MetaFunction{}{\bullet} & \bullet~;~\bullet %% & \text{where } \bullet \text{ is an empty context} + \ \MetaFunction{}{\Gamma,x:\tau} & \Gamma',x:\MetaFunction{\Delta}{\tau} ~;~ \Delta& \text{where }\Gamma';\Delta = \MetaFunction{}{\Gamma}\ @@ -1560,6 +1566,8 @@ can try and compare it to existing systems. \Gamma',l:\kw{Level},t:\Type{l} ~;~ \Delta,t:l & \text{where }\Gamma';\Delta = \MetaFunction{}{\Gamma} \medskip \ + \multicolumn{2}{l}{ + \text{--- }\MetaFunction{\Delta}{\tau} \text{ returns a pair } \tau';\ell \text{ ---}} \ \MetaFunction{\Delta}{t} & t ~;~ \Delta(t) \ \MetaFunction{\Delta}{\tau_1\to\tau_2} & \ArwS[n]{\tau_1'}{\tau_2'} @@ -1573,6 +1581,8 @@ can try and compare it to existing systems. \text{where } \tau';\ell = \MetaFunction{\Delta,t:l}{\tau} \text{ and } \ell' = \Tlub{1!!}{!!\Subst{\ell}{0}{l}} \medskip \ + \multicolumn{2}{l}{ + \text{--- }\MetaFunction{\Delta}{e} \text{ returns } e' \text{ ---}} \ \MetaFunction{\Delta}{x} & x \ \MetaFunction{\Delta}{\lambda x:\tau \to e} & \Lam[n]{t}{\tau'}{\MetaFunction{\Delta}{e}} &

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