Stefan pushed to branch report/tcvi at Stefan / Typer

Commits: 9341af95 by Stefan Monnier at 2019-11-21T03:17:10Z Started the new section on universe polymorphism

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -1197,9 +1197,9 @@ 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. +every field. This approach should also be applicable widely since +the confinement property still holds for all higher +universe terms that are not inductive.

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 @@ -1211,7 +1211,7 @@ Like all known consistent systems that support impredicative definitions, CCω accepts them only in the bottom universe. This is a direct consequence of various paradoxes formalized in systems which allow impredicative definitions in more than one universe, -such as those shown by \citet{Girard72}, \citet{Coquand94}, and +such as those shown in \citet{Girard72}, \citet{Coquand94}, and \citet{Hurkens95}. The last two showed a paradox in the system $\lambda U^-$ which can be defined as an EPTS as follows: \begin{displaymath} @@ -1299,8 +1299,8 @@ abstractions: } \end{array} \end{displaymath} -The failure to prove the confinement lemma in $\lambda U^-$ shows clearly that $\lambda -EU^-$ can type fewer terms than $\lambda U^-$. This might make us hopeful that +The failure to prove the confinement lemma in $\lambda U^-$ suggests clearly that +$\lambda EU^-$ can type fewer terms than $\lambda U^-$. This might make us hopeful that maybe it's sufficiently weaker to avoid the inconsistency of $\lambda U^-$. Alas, this is not the case: \begin{theorem} @@ -1322,6 +1322,70 @@ this is not the case: impredicative functions. %% \qed \end{proof}

+This demonstrates that, even though the notion of erasability we use here has +shown strong affinities with consistent uses of impredicativity, it is +not in general sufficient to tame the excesses of impredicativity. + +\section{Universe polymorphism} + +While paradoxes like Hurkens's suggest that it is impossible to have +impredicative definitions in more than one universe without losing +consistency, inductive definitions suggest otherwise. + +The traditional definition of inductive types using Church's impredicative +encoding looks like the following: +\begin{displaymath} + \id{NatC} = (a : \kw{Prop}) \to a \to (a \to a) \to a +\end{displaymath} +But this is much more restrictive than the real definition of \id{Nat} as an +inductive type. More specifically, when defined as an inductive type we get +two extra features: the ability to do dependent elimination, which can't be +expressed in Church's encoding, and the ability to perform elimination to +any universe, which amounts to using the following Church-like encoding: +\begin{displaymath} + \id{NatL} = (\ell : \kw{Level}) \to (a : \Type{\ell}) \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 to a first approximation its +type system could be described as the following EPTS: +\begin{displaymath} + \begin{array}{lcl@{~~|~~}l} + \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} ~} \ + \mathcal{R} &=& + {~ (k, \kw{Ul}, \Type{\ell}, \Type{\omega}) & + k \in {\kw{n},\kw{e}}, \ell\in\mathbb{N}\cup{\omega} ~} \ + %% &&\SMInsertBefore{\ensuremath{\cup ~}}{~ + %% (\kw{e},\Type{\ell},\kw{Prop},\kw{Prop}) & + %% \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 \in\mathbb{N}, \ell_2\in\mathbb{N}\cup{\omega} ~} + \end{array} +\end{displaymath} +So it would place our universe-polymorphic definition of \id{NatL} above +squarely in the far away $\Type{\omega}$ universe. Yet everything that can be +done with it can also be done with the real \id{Nat} inductive type, which +lives in the much more palatable $\Type{0}$ universe, so it would arguably +be safe to let \id{NatL} live in $\Type{0}$ (and thus make this definition +impredicative). The same reasoning applies to the following type: +\begin{displaymath} + \id{ListType} = (\ell : \kw{Level}) \to (a : \Type{\ell}) \to a \to (\Type{0} \to a \to a) \to a +\end{displaymath} +So \id{ListType} should arguably live in $\Type{1}$ rather than in +$\Type{\omega}$ since that is what happens when defined as a real inductive type. +This would also make \id{ListType} impredicative but should not threaten +consistency. This illustrates that every inductive type corresponds to an +impredicative definition that could live in the same universe, making it +clear that having impredicative definitions in multiple universe levels is +not inherently incompatible with consistency. + +Of course, this begs the question: what is it that makes it safe to let +those definitions be treated as impredicative? What is special about them? + %% \section{Related work}

%% \nocite{Gimenez94}

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