Stefan pushed to branch report/tcvi at Stefan / Typer

Commits: 6c93de25 by Stefan Monnier at 2019-11-23T07:52:15Z Develop the universe polymorphism a bit more

- - - - -

2 changed files:

- paper.tex - refs.bib

Changes:

===================================== paper.tex ===================================== @@ -39,10 +39,6 @@ %% \setcopyright{rightsretained} %% \copyrightyear{2018} %% If different from \acmYear

-%% Bibliography style -%% FIXME: I hate the way this bibliography looks because I find it -%% ridiculously hard to find the entry corresponding to a reference -%% like (Blume 2006) in the text. \newcommand \citet \cite %% Citation style %% Note: author/year citations are required for papers published as an @@ -107,7 +103,8 @@ \newcommand \Tmlam[2] {\lambda \overrightarrow{#1 : #2} .} \newcommand \Tapp[1] {#1~} \newcommand \Tproj[1] {#1.} -\newcommand \Tmax[1] {#1~\sqcup~} +\newcommand \Tmax[2] {\kw{max}(#1,#2)} +\newcommand \Tlub[1] {#1~\sqcup~}

\newcommand \Tif[2] {\kw{if}~#1~\kw{then}~#2~\kw{else}~}

@@ -265,7 +262,9 @@ might still enjoy consistency.

%% FIXME: I like to have the table of contents while writing, so I can get %% a quick overview of the structure. Should be removed before submission. -%% \newpage \tableofcontents + \newpage \tableofcontents + +\FIXME{Improve structure}

\section{Introduction}

@@ -436,7 +435,7 @@ are \Char{\kw{e}}rasable. The syntax of the terms is defined as follows: \begin{displaymath} \begin{array}{lccl} %% \textsl{(level)} & \ell &\in& \mathbb{N} \ - \textsl{(var)} & x,y,t &\in& \mathcal{V} \ + \textsl{(var)} & x,y,t,l &\in& \mathcal{V} \ \textsl{(sort)} & s &\in& \mathcal{S} \ \textsl{(argkind)} & k,c &::=& \kw{n} ~|~ \kw{e} \ \textsl{(term)} & e,\tau & ::= & s ~|~ x ~\MAlign{ @@ -818,7 +817,7 @@ as well. %% Could it be that this is not needed in CUC? \Infer{e = \Ind{x}{\tau}{\vec a} \ \Jcic e \tau} - {\Jcic{\Con{i}{e}}{\Subst{a_i}{x}{e}}} + {\Jcic{\Con{i}{e}}{\Subst{a_i}{e}{x}}}

\Infer{\forall i. %% \ \Jtype {\tau} {\tau_i} \ \Jtype {\tau_i} {\kw{Prop}}} @@ -842,8 +841,8 @@ as well. s = \kw{Prop} \vee \Jsmall{\vec {\tau_y}} \\ \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})}}} + {\ArwM[\ensuremath{c}]{y}{\Subst{\tau_y}{\tau_I}{x}} + {(\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}}

@@ -1082,8 +1081,8 @@ applicability of large inductive types. %% \\ %% \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})}}} + {\ArwM[\ensuremath{c}]{y}{\Subst{\tau_y}{\tau_I}{x}} + {(\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} @@ -1181,19 +1180,19 @@ Here is an example of code which relies on this possibility: %% \\ %% \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})}}} + {\ArwM[\ensuremath{c}]{y}{\Subst{\tau_y}{\tau_I}{x}} + {(\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} + \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 +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 @@ -1217,7 +1216,7 @@ 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 -ECoq is left for future work. +eCoq is left for future work.

\section{Multiple levels of impredicativity}

@@ -1301,7 +1300,7 @@ $\mathrm{\Delta}$ because of the $(k,\mathrm{\Delta},\square,\square)$ rule.

Following the same idea as in the previous section where we defined ECIC to rely on erasability to avoid inconsistency, we could thus define a new $\lambda -EU^-$ calculus that only allows the use of impredicativity with erasable +eU^-$ calculus that only allows the use of impredicativity with erasable abstractions: \begin{displaymath} \begin{array}{lcl} @@ -1314,17 +1313,17 @@ abstractions: \end{array} \end{displaymath} 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 +$\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} - $\lambda EU^-$ is not consistent. + $\lambda eU^-$ is not consistent. \end{theorem} \begin{proof} The proof is the same as the proof of inconsistency of $\lambda U^-$ shown in \citet{Hurkens95}. Figure~\ref{fig:hurkens} shows Hurken's original proof, using the same notation he used in his paper. To show that the - proof also applies to $\lambda EU^-$, we need to make sure that all + proof also applies to $\lambda eU^-$, we need to make sure that all impredicative abstractions can be annotated as erasable. For that, it suffices to know that the integers are variable names, the impredicative abstraction in $*$ is introduced by \kw{let}, the @@ -1370,6 +1369,34 @@ 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.

+\begin{figure} + \begin{displaymath} + \begin{array}{lccl} + %% \textsl{(level)} & \ell &\in& \mathbb{N} \ + \textsl{(level)} & \ell &::=& 0 ~|~ \kw{s}~\ell ~|~ l ~|~ \Tlub{\ell_1}{\ell_2} \ + \end{array} + \end{displaymath} + \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 {(\kw{s}~\ell)}) & \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 {\Tlub{\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} + \caption{Informal rules of an Agda-like system} + \label{fig:agda} +\end{figure} + The traditional definition of inductive types using Church's impredicative encoding looks like the following: \begin{displaymath} @@ -1381,30 +1408,15 @@ 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 + \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 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 the above universe-polymorphic definition of \id{NatL} +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. %% FIXME: Can we make this "everything" argument more formal? Yet everything that can be @@ -1413,7 +1425,7 @@ 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 + \id{ListType} = (l : \kw{Level}) \to (a : \Type{l}) \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. @@ -1427,8 +1439,157 @@ 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?

In the rest of this section we will consider one hypothesis, which is that -the universe level parameter $\ell$ is erasable. +the universe level parameter $\ell$ needs to be erasable. + +\subsection{Impredicative erasable universe polymorphism}

+\begin{figure} + \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} &=& + {~ (\kw{n}, l:\kw{Ul}, \Type{\ell}, \Type{\omega}) & + \ell\in\mathbb{N}\cup{\omega} ~} \ + &&\SMInsertBefore{\ensuremath{\cup ~}}{~ + (\kw{e}, l:\kw{Ul}, \Type{\ell}, \Type{\Subst{\ell}{0}{l}}) & + \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, x:\Type {\ell_1}, \Type {\ell_2}, \Type {\Tlub{\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} + \caption{Informal rules of EAgda} + \label{fig:eagda} +\end{figure} + +With universe polymorphism sorts are not closed any more, so +we cannot really represent the rules that govern them using a simple set +like $\mathcal{R}$. So, the $(k,\kw{Ul},\Type{\ell},\Type{\omega})$ rule +is really meant to say something like: +\begin{displaymath} + \frac{ + \Jtype{\tau_1}{\kw{Ul}} \hspace{20pt} \Jtype[\Gamma,l:\tau_1]{\tau_2}{\Type{\ell}} + }{ + \Jtype{\Arw{l}{\tau_1}{\tau_2}}{\Type{\omega}} + } +\end{displaymath} +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 +$\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: +\begin{displaymath} + \frac{ + \Jtype{\tau_1}{\kw{Ul}} \hspace{20pt} \Jtype[\Gamma,l:\tau_1]{\tau_2}{\Type{\ell}} + }{ + \Jtype{\Arw[e]{l}{\tau_1}{\tau_2}}{\Type{\Subst{\ell}{0}{l}}} + } +\end{displaymath} +While this places \id{NatL} in $\Type{1}$ rather than $\Type{0}$, it still +makes it impredicative, and if all our base types live in $\Type{1}$ we will +not notice much difference. + +Figure~\ref{fig:eagda} describes the the resulting calculus EAgda, where the +second fields of elements of $\mathcal{R}$ now have the shape ``$x:s$'' so we +can refer to the variable $x$ that can appear freely in the third field. + +\subsection{The power of EAgda} + +EAgda is basically a predicative calculus of constructions, with a tower of +universes, plus universe polymorphism, plus impredicative erasable +universe polymorphism. Compared to Agda, it lacks inductive types but it +adds a form of impredicativity. While we do not know if it is consistent, we +can try and compare it to existing systems. + +\begin{theorem} + EAgda can encode System-F. +\end{theorem} +\begin{proof} + We take as input a stratified version of System-F, so + as to make an encoding based purely on the syntax rather than the typing + derivation. + \begin{displaymath} + \begin{array}{lccl} + %% \textsl{(kinds)} & \kappa &::=& * ~|~ (t:\kappa_1)\to\kappa_2 ~|~ (x:\tau) \to \kappa \ + \textsl{(types)} & \tau &::=& + t ~|~ \tau_1\to\tau_2 ~|~ (t:*)\to\tau + %% ~|~ \lambda t:\kappa.\tau ~|~ \tau_1~\tau_2 ~|~ \lambda x:\tau_1.\tau_2 ~|~ \tau~e + \ + \textsl{(terms)} & e &::=& + x ~|~ \lambda x:\tau.e ~|~ e_1~e_2 ~|~ \lambda t:*.e ~|~ e~\tau + \end{array} + \end{displaymath} + \newcommand\Ftoa{\MetaFunction{}} + Then we define the encoding $\MetaFunction{}{\cdot}$ from System-F to EAgda: + %% FIXME: + %% What about Λt₁.Λt₂.id[t₁→t₂→t₁](λx:t₁→λy:t₂→x) ? + %% That should turn into + %% + %% (l₁:Level) ≡> (t₁:Type l₁) → + %% (l₂:Level) ≡> (t₂:Type l₂) → + %% id (l₁⊔l₂) (t₁→t₂→t₁) (λx:t₁→λy:t₂→x) + \begin{displaymath} + \begin{array}{r@{~=~}ll} + \MetaFunction{}{\bullet} & \bullet~;~\bullet \ + \MetaFunction{}{\Gamma,x:\tau} & + \Gamma',x:\MetaFunction{}{\tau} ~;~ \Delta& + \text{where }\Gamma';\Delta = \MetaFunction{}{\Gamma}\ + %% \MetaFunction{s}{\Gamma,t:\kappa} & + %% \MetaFunction{s}{\Gamma},t:\MetaFunction{s}{\kappa} \ + \MetaFunction{}{\Gamma,t:*} & + \Gamma',l:\kw{Level},t:\Type{l} ~;~ \Delta,t:l & + \text{where }\Gamma';\Delta = \MetaFunction{}{\Gamma} + \medskip \ + \MetaFunction{\Delta}{t} & t ~;~ \Delta(t) \ + \MetaFunction{\Delta}{\tau_1\to\tau_2} & + \ArwS[n]{\tau_1'}{\tau_2'} + ~;~ \Tlub{\ell_1}{\ell_2}& + \text{where } \tau_1';\ell_1 = \MetaFunction{\Delta}{\tau_1} + \text{ and } \tau_2';\ell_2 = \MetaFunction{\Delta}{\tau_2}\ + \MetaFunction{\Delta}{(t:*)\to\tau} & + \Arw[e]{l}{\kw{Level}}{ + \Arw[n]{t}{\Type{l}}{ + \tau'}} ~;~ \ell' & + \text{where } \tau';\ell = \MetaFunction{\Delta,t:l}{\tau} + \text{ and } \ell' = \Tlub{1!!}{!!\Subst{\ell}{0}{l}} + \medskip \ + \MetaFunction{\Delta}{x} & x \ + \MetaFunction{\Delta}{\lambda x:\tau . e} & + \Lam[n]{t}{\tau'}{\MetaFunction{\Delta}{e}} & + \text{where }\tau';\ell = \MetaFunction{\Delta}{\tau} \ + \MetaFunction{\Delta}{e_1~e_2} & + \App[n]{\MetaFunction{\Delta}{e_1}}{\MetaFunction{\Delta}{e_2}} \ + \MetaFunction{\Delta}{\lambda t:*.e} & + \Lam[e]{l}{\kw{Level}}{ + \Lam[n]{t}{\Type{l}}{ + \MetaFunction{\Delta,t:l}{e}}} \ + \MetaFunction{\Delta}{e~\tau} & + \App[n]{(\App[e]{\MetaFunction{\Delta}{e}}{\ell})}{ + \tau'} & + \text{where } \tau';\ell = \MetaFunction{\Delta}{\tau} + \medskip \ + %% \MetaFunction{s}{(t:\kappa_1)\to\kappa_2} & + %% \Arw[n]{t}{\MetaFunction{s}{\kappa_1}}{\MetaFunction{s}{\kappa_2}} \ + %% \MetaFunction{s}{\lambda t:\kappa . \tau} & + %% \Lam[n]{t}{\MetaFunction{s}{\kappa}}{\MetaFunction{s}{\tau}} \ + %% \MetaFunction{s}{\tau_1~\tau_2} & + %% \App[n]{\MetaFunction{s}{\tau_1}}{\MetaFunction{s}{\tau_2}} \ + %% \cdots&\cdots \ + \end{array} + \end{displaymath} + And then we can show by structural induction on the type derivation that + for any $\Jtype{e}{\tau}$ in System-F, we have + $\Jtype[\Gamma']{e'}{\tau'}$ in EAgda where $\Gamma';\Delta = \MetaFunction{}{\Gamma}$, + $e' = \MetaFunction{\Delta}{e}$, and $\tau';\ell = \MetaFunction{\Delta}{\tau}$. +\end{proof}

%% \section{Related work}

@@ -1458,7 +1619,7 @@ impredicative abstractions and fields to be erasable. We have also shown that while impredicativity and erasability seem to be correlated, erasability is neither a necessary nor a sufficient condition for impredicativity to be consistent, by showing that UTT's impredicative definitions are not all -erasable and showing that $\lambda EU^-$ is not consistent. +erasable and showing that $\lambda eU^-$ is not consistent.

It remains to be seen whether erasability as used in ECIC allows us to lift the restriction that strong elimination cannot be used on large inductive

===================================== refs.bib ===================================== @@ -374,8 +374,6 @@ different reduction rules from the ones used in [5] in order to obtain a decidable conversion relation for the system.}, - url = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR1995/RR1995- - 07.ps.Z}, }

@phdthesis{Werner94,

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