Stefan pushed to branch report/tcvi at Stefan / Typer
Commits: 02f30d15 by Stefan Monnier at 2019-11-21T00:26:35Z Improve the UTT part
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -66,6 +66,7 @@ \DeclareUnicodeCharacter{03C4}{\ensuremath{\tau}} \DeclareUnicodeCharacter{03C9}{\ensuremath{\omega}} \DeclareUnicodeCharacter{0394}{\ensuremath{\Delta}} +\DeclareUnicodeCharacter{2080}{\ensuremath{_0}} \DeclareUnicodeCharacter{2081}{\ensuremath{_1}} \DeclareUnicodeCharacter{2082}{\ensuremath{_2}} \DeclareUnicodeCharacter{21D2}{\ensuremath{\Rightarrow}} @@ -1051,7 +1052,7 @@ applicability of large inductive types. k \in {\kw{n},\kw{e}}, s \in \mathcal{S} ~} \ \SMInsertBefore{\ensuremath{\cup ~}}{~ (\kw{e},\Type{\ell},\kw{Prop},\kw{Prop}) & - k \in {\kw{n},\kw{e}}, \ell \in \mathbb{N} ~} \ + \ell \in \mathbb{N} ~} \ \SMInsertBefore{\ensuremath{\cup ~}}{~ (k, \Type {\ell_1}, \Type {\ell_2}, \Type {\Tmax{\ell_1}{\ell_2}}) & k \in {\kw{n},\kw{e}}, \ell_1,\ell_2 \in\mathbb{N} ~} @@ -1111,45 +1112,98 @@ circumstantial evidence, we venture to state the following: As noted in Section~\ref{sec:cic}, we were careful to restrict our inductive types to live in \kw{Prop}. This was no accident: we can see in the proof of confinement that we rely on this property to show the erasability of -impredicative arguments in CIC. More specifically, the lack of confinement -appears when we do a case analysis from an inductive type in $\Type{\ell}$ to -a return value in \kw{Prop}. - -\FIXME{Rework the rest of this section} - -We could relax this constraint by allowing -inductive types in higher universes but disallowing elimination from those -types to \kw{Prop}. This would be a kind of opposite to the outlawing of -strong elimination of large inductive types. With such a restriction, we -could then still show the erasability of impredicative arguments. - -But systems such as Coq and UTT~\cite{Luo92} allow impredicative definitions -in \kw{Prop}, inductive types in higher universes, and elimination from -those inductive types to \kw{Prop}. So, these systems are examples of -impredicativity which is not erasable, showing clearly that while -impredicativity and erasability seem to be strongly correlated, the kind of -erasability used in EPTS is not a necessary condition for impredicativity to -be consistent. - -\FIXME{Where is this going?} - -Concretely, the lack of confinement appears when we do a case analysis from -an inductive type in $\Type{\ell}$ to a return value in \kw{Prop}. -For example: +impredicative arguments in CIC. More specifically, confinement does not hold +if we can do a case analysis on an inductive type that lives in $\Type{\ell}$ +and return a value in \kw{Prop}. + +Systems such as Coq and UTT~\cite{Luo92} allow impredicative definitions in +\kw{Prop}, inductive types in higher universes, and elimination from those +inductive types to \kw{Prop}. These systems are hence examples of +impredicativity which is not erasable like it is in the systems seen so far. +Here is an example of code which relies on this possibility: \begin{verbatim} - Inductive Ω : Type := - | int : Ω - | arw : Ω -> Ω -> Ω - | all : forall k:Type, (k -> Ω) -> Ω. -\end{verbatim} + Inductive List (t : Type₀) : Type₀ := + nil | cons (x : t) (xs : List t).
-But the -confinement proof only breaks down in this one spot, which means that we -still cannot do very much with an object from $\Type{\ell}$ when we are in -a \kw{Prop} context, other than select a particular branch in a case -statement. This suggests that we might be able to recover erasability in -the following way: + Definition ifnil (ts : List Prop) (t : Prop) (x y : t) := + match ts with + | nil => x + | cons _ _ => y. +\end{verbatim} +\begin{figure} + \begin{displaymath} + \begin{array}{lcl} + \mathcal{R} &=& + \begin{array}[t]{@{}l@{~~|~~}l} + {~ (k, \kw{Prop}, s, s) & + k \in {\kw{n},\kw{e}}, s \in \mathcal{S} ~} \ + \SMInsertBefore{\ensuremath{\cup ~}}{~ + (\kw{e},\Type{\ell},\kw{Prop},\kw{Prop}) & + \ell \in \mathbb{N} ~} \ + \SMInsertBefore{\ensuremath{\cup ~}}{~ + (\kw{n},\Type{\ell},\kw{Prop},\Type{\ell}) & + \ell \in \mathbb{N} ~} \ + \SMInsertBefore{\ensuremath{\cup ~}}{~ + (k, \Type {\ell_1}, \Type {\ell_2}, \Type {\Tmax{\ell_1}{\ell_2}}) & + k \in {\kw{n},\kw{e}}, \ell_1,\ell_2 \in\mathbb{N} ~} + \end{array} + \end{array} + \end{displaymath} \medskip + \begin{mathpar} + \Infer{\Jcic{\tau}{s} \ + %% \tau = \ArwM[_]{_}{_}{\kw{Prop}} \ + \forall i. \ + \Jcic[\Gamma,x:\tau]{a_i}{s'} \ + \Jcon[x] {a_i} %% \ + %% \ell_i < \ell + } + {\Jcic{\Ind{x}{\tau}{\vec a}}{\tau}}
+ \Infer{\Jcic e {\AppM{\tau_I}{p}} \ + \tau_I = \Ind{x}{\ArwM{z}{\tau_z}{s'}}{\vec a} \ + \Jcic {\tau_r}{\ArwM{z}{\tau_z}{\Arw[n]{_}{\AppM{\tau_I}{z}}s}} \\ + \forall i.\hspace{-1pt} \ + a_i = {\ArwM[\ensuremath{c}]{y}{\tau_y}{\AppM{x}{p'}}} \ + %% \\ + %% \forall i. \ + \Jcic {b_i} + {\ArwM[\ensuremath{c}]{y}{\Subst{\tau_y}{x}{\tau_I}} + {\App[n]{\AppM{\tau_r}{p'}}{(\AppM[\ensuremath{c}]{\Con{i}{\tau_I}}{y})}}} + } + {\Jcic{\Case{\tau_r}{e}{\vec b}}{\App[n]{\AppM{\tau_r}{p}}e}} + \end{mathpar} + \caption{Rules of the ECoq system} + \label{fig:ecoq} +\end{figure} +Short of re-adding the non-erasable impredicativity with rule +$(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$, the closest we can get is by +replacing it with the predicative rule +$(\kw{n},\Type{\ell},\kw{Prop},\Type{\ell})$ instead. Figure~\ref{fig:ecoq} shows +the relevant rules of such a system we call ECoq. With such a system, we can +handle the above example in one of the following ways: +\begin{itemize} +\item Live with the fact that \id{ifnil} will now live in $\Type{0}$ rather + than \kw{Prop}. \ + Experience with Agda and other systems suggests that most code does not + crucially rely on impredicativity, so this first approach should be + applicable in many cases. +\item Replace the above ``\id{List Prop}'' lists with ``\id{eList Prop}'' + lists which are ``thinner'' lists whose elements are marked as erasable, + so that ``\id{eList Prop}'' lists can live in \kw{Prop}. +\end{itemize} +We call the second approach \emph{thinning}. It replaces inductive objects +from a higher universe with similar objects that fit in \kw{Prop}. +This thinning works as follows: when applied to an element from \kw{Prop} +it keeps the element untouched, otherwise if the element is not inductive +then it marks it as erasable, and else it defines another inductive type of +the same shape but living in \kw{Prop} by applying thinning to +every field. This approach should also be applicable fairly widely since +the confinement property still holds for non-inductive higher +universe elements. + +Whether the use of thinning is sufficient to show that any valid typing +derivation in a system like UTT has a corresponding typing derivation in +ECoq is left for future work.
\section{Multiple levels of impredicativity}
View it on GitLab: https://gitlab.com/monnier/typer/commit/02f30d158a65d4acf393494a75748c188657...
Afficher les réponses par date