Novembre 2019 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][report/tcvi] Submitted to TYPES postproceedings, depite the bad title
by Stefan 25 Nov '19

25 Nov '19

Stefan pushed to branch report/tcvi at Stefan / Typer Commits: 89b5f9db by Stefan Monnier at 2019-11-25T06:03:32Z Submitted to TYPES postproceedings, depite the bad title - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -344,7 +344,7 @@ The contributions of this work are: 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 +\item A new calculus EpCCω with an impredicative universe polymorphism which allows more powerful forms of impredicativity, such as a Church encoding with strong elimination. \item As needed for some of the above contributions, we sketch a calculus @@ -498,10 +498,10 @@ annotations as well as all erasable arguments: \end{displaymath} 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, +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)$'' -rather than ``$\Ferase e$'' itself. +rather than the specific shape of ``$\Ferase e$'' itself. Since the new \textsc{e-Lam} rule is strictly more restrictive than the normal one, it is trivial to show that every EPTS $S$, just like every CPTS, @@ -542,7 +542,7 @@ where convertibility is checked after erasure (so-called internal erasure): We use the weaker rule because it is sufficient for our needs and makes it immediately obvious that every well-typed term $e$ in an EPTS $S$ has a corresponding well-typed term $\Fforget e$ in $\Fforget S$. -Our results likely carry over to systems with the stronger rule, of course. +Our results would carry over to systems with the stronger rule, of course. %% otherwise the %% consistency of the corresponding PTS might not automatically carry over to @@ -665,22 +665,22 @@ universe \kw{Prop} is almost always erasable and armed with this observation along with some circumstantial evidence, we propose to rely on this property in order to lift the no-SELIT restriction. -\subsection{Erasing impredicative arguments of CCω} +\subsection{\kw{e}CCω: Erasing impredicative arguments of CCω} %% \FIXME{Abel mentions in~\cite{Abel13} that in the pure CoC, dependent %% arguments are always erasable, but that this doesn't hold any more %% once we add inductive types and ``recursion''. Not sure why/how} +\newcommand \SMInsertBefore[1]{ + \settowidth{\dimen0}{#1}\hspace{-\dimen0}#1 +} + We will start by showing that impredicative arguments in the calculus of constructions extended with a tower of universes (CCω) are always erasable. We use CCω because it is arguably the pure type system that is most closely related to existing systems like Coq. The calculus we use for that can be described by the following EPTS: - -\newcommand \SMInsertBefore[1]{ - \settowidth{\dimen0}{#1}\hspace{-\dimen0}#1 -} - +%% \begin{displaymath} \begin{array}{lcl} \mathcal{S} &=& \{~ \kw{Prop}; \Type \ell ~|~ \ell\in\mathbb{N} ~\} \\ @@ -722,27 +722,27 @@ second is redundant: \begin{lemma}[Confinement of impredicativity in CCω] \label{lem:erasable} \mbox{} \\ \normalfont - %% FIXME: Make it a bit more formal? - In CCω, if $\Jtype{x}{\tau_x : \Type \ell}$ and - $\Jtype[\Gamma,x\:\tau_x,\Gamma']{e}{\tau_e:\kw{Prop}}$, then $x$ can only appear in $\Ferase - e$ within arguments to functions of type $(y\:\tau_1) \TEarw \tau_2$ where - $\tau_2 : \kw{Prop}$ and \ $\exists \ell'$ such that $\tau_1 : \Type {\ell'}$. + In CCω, if $\Jtype{x}{\tau_x}$ and $\Jtype{e}{\tau_e}$ and + $\Jtype{\tau_x}{\Type{\ell}}$ and $\Jtype{\tau_e}{\kw{Prop}}$ then $x$ can only + appear in $\Ferase e$ within arguments to impredicative functions, + i.e.~functions whose return values live in \kw{Prop} and whose arguments + don't.. \end{lemma} \begin{proof} By induction on the type derivation of $e$: \begin{itemize} \item Given $\tau_e : \kw{Prop}$, clearly $e$ is too small to be a type like a sort $s$ or an - arrow $\Arw{x}{\tau_1}{\tau_2}$, and it is also too small to be $x$ itself. + arrow $\Arw{y}{\tau_1}{\tau_2}$, and it is also too small to be $x$ itself. \item If the derivation uses the \textsc{Conv} rule to convert $e : \tau_e$ to $e : \tau_e'$, we know that $\tau_e'$ also has type \kw{Prop}, by virtue of the type preservation property, so we can use the induction hypothesis on $e : \tau_e'$. \item If $e$ is a function $\Lam{y}{\tau_y}{e_y}$, then $\tau_y$ does not matter since it is erased from $\Ferase e$ and only occurrences of $x$ in - $e_y$ is a concern, but since $\tau_e : \kw{Prop}$, we also know that the + $e_y$ is a concern, and since $\tau_e : \kw{Prop}$, we also know that the type of $e_y$ is itself in \kw{Prop}, hence we can use the induction - hypothesis. + hypothesis on it. \item If $e$ is an application $\App{e_1}{e_2}$, as above we can apply the induction hypothesis to $e_1$. As for $e_2$, there are two cases: either $e_1$ takes an argument of type $\tau_1\:\kw{Prop}$ in which @@ -750,7 +750,7 @@ second is redundant: argument of type $\tau_1\:\Type{\ell'}$ in which case we're done. %% \qed \end{itemize} - \vspace{-\baselineskip} + \vspace{-1.5\baselineskip} \end{proof} Let's call \kw{e}CCω the restriction of CCω where all arguments to @@ -762,8 +762,8 @@ i.e.~$(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ is removed. %% CCω's rule $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ is redundant since for any derivation $\Jtype e \tau$ in CCω there is a corresponding derivation - $\Jtype[\Gamma'] {e'} {\tau'}$ in \kw{e}CCω such that $\Fforget{\Jtype e \tau} = - \Fforget{\Jtype[\Gamma'] {e'} {\tau'}}$ + $\Jtype[\Gamma'] {e'} {\tau'}$ in \kw{e}CCω such that + $\Fforget{\Jtype{e}{\tau}}=\Fforget{\Jtype[\Gamma']{e'}{\tau'}}$. \end{theorem} \begin{proof} By induction on the type derivation of $e$ where we systematically replace @@ -784,7 +784,7 @@ This shows that the erasability of System-F's impredicative type abstractions can be extended to all of CCω's impredicative abstractions as well. -\subsection{Erasing impredicative arguments of CIC} +\subsection{\kw{e}CIC: Erasing impredicative arguments of CIC} \label{sec:cic} \newcommand \Ind[3] {\kw{Ind}(#1\:#2)\langle#3\rangle} @@ -864,12 +864,12 @@ proof irrelevant like Coq's \kw{Prop}; for readers more familiar with Coq, our CIC's \kw{Prop} is more like Coq's impredicative \kw{Set}). Note also that our CIC does have a tower of universes, like Coq, but its inductive types only exist in the bottom universe, as was the case in the -original CIC. +original CIC, which is why we prefer to call it CIC than CICω. We mostly follow the presentation of \citet{Gimenez94} for the syntax of inductive types but we extend its rules according to the presentation of \citet{Werner94} which adds a strong elimination, i.e.~the -ability to compute a type by cases analysis on an inductive type, which is +ability to compute a type by case analysis on an inductive type, which is needed for many proofs, even simple ones. %% The syntax of terms is extended as follows: @@ -887,13 +887,14 @@ The syntax of terms is extended as follows: \end{displaymath} $\Ind{x}{\tau}{\vec a}$ is a (potentially indexed) inductive type which itself has type $\tau$ and whose $i^{\text{th}}$ constructor has type $a_i$, where -$\vec a$ represent the sequence of terms $a_0 \dots a_n$. $\Con{i}{e}$ +we use the vector notation $\vec a$ to represent a sequence of terms +$a_0\dots{}a_n$. $\Con{i}{e}$ denotes the $i^{\text{th}}$ constructor of the inductive type $e$. $\Case{\tau_r}{e}{\vec b}$ is a case analysis of the term $e$ which should be an object of inductive type; it will dispatch to the corresponding branch $b_i$ if $e$ was built with the $i^{\text{th}}$ constructor of the inductive type; $\tau_r$ describes the return type of the case expression. -Finally $\Fix{i}{x}{\tau}{e}$ is a recursive function of type $\tau$, defined by +Finally $\Fix{i}{x}{\tau}{e}$ is a recursive function $x$ of type $\tau$, defined by structural induction on its $i^{\text{th}}$ argument. We must of course also extend the definition of our erasure function to @@ -960,12 +961,11 @@ impredicativity is still redundant in this new system, we proceed in the same way: \begin{lemma}[Confinement of impredicativity in CIC] \label{lem:erasable-cic} \mbox{} \\ \normalfont - %% FIXME: Make it a bit more formal? - In CIC, if $\Jtype{x}{\tau_x:\Type{\ell}}$ and - $\Jtype[\Gamma,x\:\tau_x,\Gamma']{e}{\tau_e:\kw{Prop}}$, then $x$ can only appear in - $\Ferase e$ within arguments to functions of type - $(y\:\tau_1) \TEarw \tau_2$ where $\tau_2:\kw{Prop}$ and $\exists \ell'$ such that - $\tau_1:\Type{\ell'}$. + In CIC, if $\Jtype{x}{\tau_x}$ and $\Jtype{e}{\tau_e}$ and + $\Jtype{\tau_x}{\Type{\ell}}$ and $\Jtype{\tau_e}{\kw{Prop}}$ then $x$ + can only appear in $\Ferase e$ within arguments to impredicative functions, + i.e.~functions whose return values live in \kw{Prop} and whose arguments + don't. \end{lemma} \begin{proof} The proof stays the same, with the following additional cases: @@ -983,7 +983,7 @@ way: $b_i$ are as well, hence we can also invoke the induction hypothesis on every $b_i$. %% \qed \end{itemize} - \vspace{-\baselineskip} + \vspace{-1.5\baselineskip} \end{proof} Let's call \kw{e}CIC the restriction of CIC where all arguments to @@ -1024,7 +1024,7 @@ abstractions can be extended not only to all of CCω's impredicative abstractions but also to CIC's impredicative abstractions and impredicative inductive types. -\subsection{Strong elimination of large inductive types} +\subsection{ECIC: Strong elimination of large inductive types} The reason behind the $\Jsmall e$ special constraint on strong eliminations of CIC in Figure~\ref{fig:cic} is pretty @@ -1038,12 +1038,13 @@ of universe \kw{Prop}: | box x' => x' end. \end{verbatim} -Note that such a box is perfectly valid in CIC, but the $\Jsmall e$ -constraint rejects the \texttt{unbox} definition. If we remove the $\Jsmall -e$ constraint, the effect of such a \texttt{box}/\texttt{unbox} pair would be -to lower any value of a higher universe to the \kw{Prop} universe and would -hence defeat the purpose of the stratification introduced by the tower of -universes. This was first shown to be inconsistent in \cite{Coquand86b}. +Note that such a box (a large inductive type) is perfectly valid in CIC, but +the $\Jsmall e$ constraint rejects the \texttt{unbox} definition (which uses +a strong elimination). If we remove the $\Jsmall e$ constraint, the effect +of such a \texttt{box}/\texttt{unbox} pair would be to lower any value of +a higher universe to the \kw{Prop} universe and would hence defeat the +purpose of the stratification introduced by the tower of universes. +This was first shown to be inconsistent in \cite{Coquand86b}. This restriction makes the system more complex since elimination is allowed from any inductive type to any universe except for the one special case of @@ -1114,8 +1115,8 @@ Figure~\ref{fig:ecic} shows a refinement of \kw{e}CIC we call ECIC whose ECIC is more elegant and regular than CIC thanks to the absence of this special corner case, and it allows typing more terms than \kw{e}CIC and hence CIC. For instance in ECIC we can define the above $\Omega$ inductive type with an -erasable $k$ and then prove the mentioned property (again with erasable -$k_1$ and $k_2$). +erasable $k$ and then prove the mentioned property (with +$k_1$ and $k_2$ marked as erasable). Note also that the lack of an $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ rule, means we cannot define a \texttt{box} as above in this system; instead we @@ -1130,7 +1131,7 @@ circumstantial evidence, we venture to state the following: The ECIC system is consistent. \end{conjecture} -\subsection{Erasing impredicativity in Coq and UTT} +\subsection{\kw{e}Coq: Erasing impredicativity in Coq and UTT} 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 @@ -1195,21 +1196,21 @@ Here is an example of code which relies on this possibility: } {\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 \kw{e}Coq 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: +the relevant rules of such a system we call \kw{e}Coq. 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. + crucially rely on impredicativity, so in practice this first approach + should be applicable in most 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}. @@ -1218,7 +1219,7 @@ 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 +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 widely since the confinement property still holds for all higher @@ -1226,63 +1227,24 @@ 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. +\kw{e}Coq is left for future work. \section{Universe-agnostic impredicativity} -Like most known consistent type systems that support impredicative -definitions, CCω accepts them only in the bottom universe, called \kw{Prop} +CCω accepts impredicative definitions only in the bottom universe, called +\kw{Prop}, just as is the case in most known consistent type systems that +support impredicative definitions (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 \citet{Hurkens95}. -In this section we investigate the use of an erasability constraint in order +In this section we investigate the use of erasability constraints in order to lift this restriction and thus allow impredicative definitions in higher universes as well. -\subsection{Erasing impredicative arguments in $\lambda U^-$} - -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} ~\} \\ - \mathcal{A} &=& \{~ (*,~\square), (\square,~\mathrm{\Delta}) ~\} \\ - \mathcal{R} &=& - \{~ \MAlign{ - (k,*,*,*),~(k,\square,*,*),~%% ~(k,\mathrm{\Delta},*,*), - %% \\ - (k,\square,\square,\square),~(k,\mathrm{\Delta},\square,\square) - \hspace{40pt}~|~ k \in \{\kw{n},\kw{e}\} ~\} - } - \end{array} -\end{displaymath} -Of the four pairs of rules, two are impredicative: $(k,\square,*,*)$ %% , -%% $(k,\mathrm{\Delta},*,*)$, -and $(k,\mathrm{\Delta},\square,\square)$, but since $*$ is the bottom -universe and hence corresponds to \kw{Prop} in CCω, the first is -generally considered safe and is included in System-F and CCω. The new one is -$(k,\mathrm{\Delta},\square,\square)$ which introduces impredicativity in the second -universe, $\square$. - -In such a system, the lemma of confinement of impredicativity cannot -be shown. The statement of the lemma would look like the following: -\begin{lemma}[Confinement of impredicativity in $\lambda U^-$] - \label{lem:erasable-lU} \mbox{} \\ \normalfont - In $\lambda U^-$, if $\Jtype{x}{\tau_x : s_1}$ and - $\Jtype[\Gamma,x\:\tau_x,\Gamma']{e}{\tau_e:s_2}$ and $s_1 > s_2$, then $x$ can only - appear in $\Ferase e$ within arguments to functions of type - $(y\:\tau_1)\TEarw \tau_2$ where $\tau_1 : s_3$ and $\tau_2 : s_4$ and $s_3 > s_4$. -\end{lemma} -When we attempt to adapt the earlier proof for CCω, is breaks down when $e$ -is of the form $\Arw{y}{\tau_1}{\tau_2}$: we can invoke the induction hypothesis -on $\tau_2$ because it necessarily lives in the same universe as $e$, but we -cannot invoke the induction hypothesis on $\tau_1$ if $x$ is in the universe -$\mathrm{\Delta}$, because $\tau_1$ might itself also be in the universe -$\mathrm{\Delta}$ because of the $(k,\mathrm{\Delta},\square,\square)$ rule. +\subsection{$\lambda\kw{e}U^-$: Erasing impredicative arguments in $\lambda U^-$} \begin{figure}[tb] \begin{displaymath} @@ -1318,9 +1280,51 @@ $\mathrm{\Delta}$ because of the $(k,\mathrm{\Delta},\square,\square)$ rule. \label{fig:hurkens} \end{figure} +The last two papers referenced above showed a paradox in the system $\lambda U^-$ +which is 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} ~\} \\ + \mathcal{A} &=& \{~ (*,~\square), (\square,~\mathrm{\Delta}) ~\} \\ + \mathcal{R} &=& + \{~ \MAlign{ + (k,*,*,*),~(k,\square,*,*),~%% ~(k,\mathrm{\Delta},*,*), + %% \\ + (k,\square,\square,\square),~(k,\mathrm{\Delta},\square,\square) + \hspace{40pt}~|~ k \in \{\kw{n},\kw{e}\} ~\} + } + \end{array} +\end{displaymath} +Of the four pairs of rules, two are impredicative, $(k,\square,*,*)$ %% , +%% $(k,\mathrm{\Delta},*,*)$, +and $(k,\mathrm{\Delta},\square,\square)$, but since $*$ is the bottom +universe and hence corresponds to \kw{Prop} in CCω, the first is +generally considered harmless. The new one is +$(k,\mathrm{\Delta},\square,\square)$ which introduces impredicativity in the second +universe, $\square$. + +%% FIXME: I think confinement fails in λU (which I used in the earlier +%% version of the paper), but not in λU- ! +%% In such a system, the lemma of confinement of impredicativity cannot +%% be shown. The statement of the lemma would look like the following: +%% \begin{lemma}[Confinement of impredicativity in $\lambda U^-$] +%% \label{lem:erasable-lU} \mbox{} \\ \normalfont +%% In $\lambda U^-$, if $\Jtype{x}{\tau_x : s_1}$ and +%% $\Jtype{e}{\tau_e:s_2}$ and $s_1 > s_2$, then $x$ can only +%% appear in $\Ferase e$ within arguments to functions of type +%% $(y\:\tau_1)\TEarw \tau_2$ where $\tau_1 : s_3$ and $\tau_2 : s_4$ and $s_3 > s_4$. +%% \end{lemma} +%% When we attempt to adapt the earlier proof for CCω, it breaks down when $e$ +%% is of the form $\Arw{y}{\tau_1}{\tau_2}$: we can invoke the induction hypothesis +%% on $\tau_2$ because it necessarily lives in the same universe as $e$, but we +%% cannot invoke the induction hypothesis on $\tau_1$ if $x$ is in the universe +%% $\mathrm{\Delta}$, because $\tau_1$ might itself also be in the universe +%% $\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 +\kw{e}U^-$ calculus that only allows the use of impredicativity with erasable abstractions: \begin{displaymath} \begin{array}{lcl} @@ -1332,18 +1336,18 @@ 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 -maybe it's sufficiently weaker to avoid the inconsistency of $\lambda U^-$. Alas, -this is not the case: +%% The failure to prove the confinement lemma in $\lambda U^-$ suggests clearly that +%% $\lambda\kw{e}U^-$ 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 does not help: \begin{theorem} - $\lambda eU^-$ is not consistent. + $\lambda\kw{e}U^-$ 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\kw{e}U^-$, 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 @@ -1389,6 +1393,26 @@ 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. Let us focus on the second one. The ability to perform +elimination to any universe amounts to using the following Church-like +encoding: +\begin{displaymath} + \id{NatL} = (l : \kw{Level}) \to (a : \Type{l}) \to a \to (a \to a) \to a +\end{displaymath} +Such a definition is possible in systems like Agda which provide the +necessary universe polymorphism (the $l$ above is a universe-level +variable), but this type \id{NatL} is traditionally placed in a universe too +high to be useful as an encoding of natural numbers. + \begin{figure} \begin{displaymath} \begin{array}{lccl} @@ -1417,27 +1441,12 @@ consistency, inductive definitions suggest otherwise. \label{fig:agda} \end{figure} -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} = (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 (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 +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 informally 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. +According to those rules, 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 done with it can also be done with the real \id{Nat} inductive type, which @@ -1461,37 +1470,12 @@ 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$ needs to be erasable. -\subsection{Impredicative erasable universe polymorphism} +\subsection{EpCCω: 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 {(\kw{s}~\ell)}) & \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 EpCCω} - \label{fig:eagda} -\end{figure} - -With universe polymorphism sorts are not closed any more, so +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: +was 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}} @@ -1517,6 +1501,31 @@ 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. +\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 {(\kw{s}~\ell)}) & \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 EpCCω} + \label{fig:eagda} +\end{figure} + Figure~\ref{fig:eagda} describes the resulting calculus we call EpCCω, 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 @@ -1524,97 +1533,124 @@ third field. \subsection{Encoding System-F in EpCCω} -EpCCω 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. +EpCCω is basically a predicative version of CCω (hence the ``p'') to which +we added universe polymorphism and impredicative erasable universe +polymorphism (which motivated the ``E''). Contrary to the previous calculus +it does not have a base impredicative universe \kw{Prop}: its only source of +impredicativity is the $(\kw{e},l\:\kw{Ul},\Type{\ell},\Type{\Subst{\ell}{0}{l}})$ +rule which introduces the 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, and for that we start by showing how to +encode System-F. + +In order for our encoding function $\MetaFunction{}{\cdot}$ to be based purely +on the syntax of terms rather than the typing derivation, we take as input +a stratified version of System-F: +\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 \to e ~|~ e_1~e_2 ~|~ \lambda t\:* \to e ~|~ e~\tau + \end{array} +\end{displaymath} +To encode System-F, the only interesting part is the need to simulate +System-F's impredicative quantification over types. We can do that in the +same way \id{NatC} was generalized to \id{NatL}, i.e.~by replacing +``$(t:*)\to\tau$'' with ``$\Arw[e]{l}{\kw{Level}}{\Arw[n]{t}{\Type{l}}{\tau}}$''. + +The only tricky aspect of this encoding is that while in System-F all the +type variables (and more generally all the types) have the same kind $*$, +the encoding makes every type variable come with its own universe level, so +the encoding function needs to keep track of the level of each type in order +to know how to instantiate the $\Arw[e]{l}{\kw{Level}}{...}$ quantifiers. + +\newcommand\Ftoa{\MetaFunction{}} +The encoding function on types takes the form $\MetaFunction{\Delta}{\tau}$ where +$\Delta$ maps each type variable to its associated level variable, and it returns +a pair $\tau';\ell$ where $\ell$ is the universe level of $\tau'$: +\begin{displaymath} + \begin{array}{r@{~=~}ll} + \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}} + \end{array} +\end{displaymath} +Similarly the encoding function for terms takes the form +$\MetaFunction{\Delta}{e}$: +\begin{displaymath} + \begin{array}{r@{~=~}ll} + \MetaFunction{\Delta}{x} & x \\ + \MetaFunction{\Delta}{\lambda x\:\tau \to 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\:* \to 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 \to \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} +Finally we need to encode contexts as well, for which the encoding function +takes the form $\MetaFunction{}{\Gamma}$ and it returns a pair $\Gamma';\Delta$: +\begin{displaymath} + \begin{array}{r@{~=~}ll} + \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}\\ + %% \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} + \end{array} +\end{displaymath} + -\begin{theorem} - EpCCω 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 \to e ~|~ e_1~e_2 ~|~ \lambda t\:* \to e ~|~ e~\tau - \end{array} - \end{displaymath} - \newcommand\Ftoa{\MetaFunction{}} - Then we define the encoding $\MetaFunction{}{\cdot}$ from System-F to EpCCω: - \begin{displaymath} - \begin{array}{r@{~=~}ll} - %% 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}\\ - %% \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 \\ - \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'} - ~;~ \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 \\ - \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}} & - \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\:* \to 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 \to \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'}$ and +\begin{theorem}[EpCCω can encode System-F] + \mbox{} \\ + For any $\Jtype{e}{\tau}$ in System-F, we have $\Jtype[\Gamma']{e'}{\tau'}$ and $\Jtype[\Gamma']{\tau'}{\Type{\ell}}$ in EpCCω where $\Gamma';\Delta = \MetaFunction{}{\Gamma}$, $e' = \MetaFunction{\Delta}{e}$, and $\tau';\ell = \MetaFunction{\Delta}{\tau}$. +\end{theorem} +\begin{proof} + By structural induction on the type derivation. \end{proof} \subsection{The power of EpCCω} +%% FIXME: Expand on those positive examples! E.g. Show that it indeed covers +%% Chlipala's use of impredicativity. +%% FIXME: Can we show that it also covers the (or some) closure-conversion use +%% of impredicativity? EpCCω is flexible enough to cover the kind of impredicativity found in Church's encoding or in Chlipala's parametric higher-order abstract syntax~\cite{Chlipala08}. It does it without restricting impredicativity to @@ -1622,41 +1658,50 @@ a single universe, and moreover those encodings are more flexible in EpCCω since as we have seen they support the equivalent of strong elimination. So in this sense EpCCω is more powerful than systems like CCω. -Yet we have not been able to generalize the above System-F encoding to -encode System-F$_ω$ into EpCCω. For example, consider the following term: +Yet we have not even been able to generalize the above System-F encoding in +order to encode F$_ω$ into EpCCω. For example, consider the following F$_\omega$ +term: +\begin{displaymath} + λt_1\:* \to \lambda (t_2 \: *\to*) \to \lambda (x \: t_2~t_1) \to x +\end{displaymath} +A simple encoding into EpCCω could be: \begin{displaymath} - λt\:* \to \lambda (f \: *\to*) \to \lambda (x \: f~t) \to x + \Lam[e]{l}{\kw{Level}}{ + \Lam[n]{t_1}{\Type{l}}{ + \Lam[n]{(t_2}{\ArwS[n]{\Type{l}}{\Type{l}})}{ + \Lam[n]{x}{\App[n]{t_2}{t_1}}{x}}}} \end{displaymath} -The first two $\lambda$s should be impredicative, so the encoding should -presumably look like: +But it's not faithful to the original F$_ω$ term because it only +preserves the impredicativity of the first $\lambda$. In order to get an encoding +that can work for any F$_ω$ term, we hence need an encoding which looks like: \begin{displaymath} \Lam[e]{l_1}{\kw{Level}}{ - \Lam[n]{t}{\Type{l_1}}{ + \Lam[n]{t_1}{\Type{l_1}}{ \Lam[e]{l_2}{\kw{Level}}{ - \Lam[n]{f}{T_1}{ - \Lam[n]{x}{T_2}{ + \Lam[n]{t_2}{T_2}{ + \Lam[n]{x}{T_x}{ x}}}}} \end{displaymath} -We can then choose $T_1$ and $T_2$ as follows: +where $T_2$ refers to $l_2$. We can then choose $T_2$ and $T_x$ as follows: \begin{displaymath} \begin{array}{l@{~=~}l} - T_1 & \Arw[e]{l_3}{\kw{Level}}{\ArwS[n]{\Type{l_3}}{\Type{l_2}}} \\ - T_2 & \App[n]{\App[e]{f}{l_1}}{t} + T_2 & \Arw[e]{l_3}{\kw{Level}}{\ArwS[n]{\Type{l_3}}{\Type{l_2}}} \\ + T_x & \App[n]{\App[e]{t_2}{l_1}}{t_1} \end{array} \end{displaymath} This makes the term valid, but its semantics doesn't match that of the -original System-F$_\omega$ term since we cannot pass the identity function +original F$_\omega$ term since we cannot pass the identity function $\lambda{}t\:*\to{}t$ as $f$ any more: its encoding would now have type $\Arw[e]{l_3}{\kw{Level}}{\ArwS[n]{\Type{l_3}}{\Type{l_3}}}$ instead of the expected $\Arw[e]{l_3}{\kw{Level}}{\ArwS[n]{\Type{l_3}}{\Type{l_2}}}$. Similarly, we have not been able to adapt Hurkens's paradox to the EpCCω system either. Of course, all this says is that we do not know if EpCCω is -consistent, but it seems to indicate that this kind of impredicativity is -incomparable to the traditional form seen in CCω or $\lambda U^-$. +consistent, but at least it indicates that this kind of impredicativity is +probably incomparable to the traditional form seen in CCω or $\lambda U^-$. %% \begin{theorem} -%% EpCCω can encode System-F$_\omega$. +%% EpCCω can encode F$_\omega$. %% \end{theorem} %% \begin{proof} %% %% If we try to encode @@ -1667,7 +1712,7 @@ incomparable to the traditional form seen in CCω or $\lambda U^-$. %% %% (l₃) ≡> (tf: (l₄) ≡> (_ : Type l₄) -> (l₅) ≡> (_ : Type l₅) %% %% -> Type l₃) -> %% %% tf {l₁} t₁ {l₂} t₂ -%% We take as input a stratified version of System-F$_\omega$, so +%% We take as input a stratified version of F$_\omega$, so %% as to make an encoding based purely on the syntax rather than the typing %% derivation. %% \begin{displaymath} @@ -1683,7 +1728,7 @@ incomparable to the traditional form seen in CCω or $\lambda U^-$. %% \end{array} %% \end{displaymath} %% \newcommand\Ftoa{\MetaFunction{}} -%% Then we define the encoding $\MetaFunction{}{\cdot}$ from System-F$_\omega$ to EpCCω: +%% Then we define the encoding $\MetaFunction{}{\cdot}$ from F$_\omega$ to EpCCω: %% %% FIXME: %% %% What about Λt₁.Λt₂.id[t₁→t₂→t₁](λx:t₁→λy:t₂→x) ? %% %% That should turn into @@ -1755,7 +1800,7 @@ incomparable to the traditional form seen in CCω or $\lambda U^-$. %% \nocite{Firsov18} %Cedille %% FIXME: Relate to Andreas Abel's habilitation thesis where he talks about -%% erasure of type dependencies to bring LF to System F and CoC to Fω. +%% erasure of type dependencies to bring LF to System-F and CoC to Fω. %% FIXME: Relate to Thorsten Altenkirch's work (not sure which, tho). @@ -1768,25 +1813,33 @@ incomparable to the traditional form seen in CCω or $\lambda U^-$. \section{Conclusion} We have taken a tour of the interactions between impredicativity and -erasability of arguments in EPTS. We have shown that three of the most well -known systems that admit impredicativity do it in a way that constrains all -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. +erasability of arguments in EPTS. We have shown that three of the five most +well known systems that admit impredicativity do it in a way that constrains +all impredicative abstractions and fields to be erasable (and that the +remaining two almost do it as well). 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: the inconsistency of $\lambda\kw{e}U^-$ shows it's not sufficient, and +our inability to show that UTT's impredicative definitions are all erasable +suggests it's not necessary either. 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 -types without breaking consistency. +types without breaking consistency, and whether erasability as used in EpCCω +allows us to introduce a form of impredicativity applicable to all +universe levels without breaking consistency. \newenvironment{acks}{\subsection*{Acknowledgments}}{} %% \newcommand \grantsponsor[3] {#2 (#1)} %% \newcommand \grantnum[2] {#2} \begin{acks} + We would like to thank Chris League for his comments on earlier drafts of + the paper, as well as the anonymous reviewers. + This work was supported by the \grantsponsor{NSERC}{Natural Sciences and Engineering Research Council of Canada}{http://nserc-crsng.gc.ca/} grant - N$^o$~\grantnum{NSERC}{298311/2012}. Any opinions, findings, and + N$^o$~\grantnum{NSERC}{298311/2012} and \grantnum{NSERC}{RGPIN-2018-06225}. + Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the NSERC. \end{acks} View it on GitLab: https://gitlab.com/monnier/typer/commit/89b5f9db65d8aafa227778744ac365c4622… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/89b5f9db65d8aafa227778744ac365c4622… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/tcvi] -
by Stefan 24 Nov '19

24 Nov '19

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/b3a46643673194ec9e70b49ea8638282219… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/b3a46643673194ec9e70b49ea8638282219… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/tcvi] Getting there
by Stefan 23 Nov '19

23 Nov '19

Stefan pushed to branch report/tcvi at Stefan / Typer Commits: 68df8023 by Stefan Monnier at 2019-11-24T00:28:54Z Getting there - - - - - 2 changed files: - paper.tex - refs.bib Changes: ===================================== paper.tex ===================================== @@ -262,27 +262,10 @@ 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 \section{Introduction} -%% General plan: -%% -%% - Intro: describe the general landscape of impredicativity -%% (and erasable arguments) -%% - Background: Present EPTS -%% Maybe discuss the two conv rules -%% - Show System-F and show how to compile it to an EPTS -%% - Show CCω and show how to compile it to an EPTS -%% Discuss how the constraint that on the bottom is impredicative enters -%% into the picture. (e.g. my proof fails because the `x` can now appear -%% within arrows, and these would not be erasable, FIXME: does it break -%% elsewhere?). -%% Ideally explain the gist of Hurkens?! -%% - Show CIC and show how to compile it to an EPTS -%% Discuss how SELIT enters into the picture. -%% - Maybe discuss UTT and Coq and how they don't fit this model. - Diagonalization proofs and paradoxes such as ``This sentence is false'' show the dangers of self reference: admitting such propositions in a logic leads to inconsistencies. For this reason Russell introduced the concept of @@ -292,8 +275,8 @@ The stratification enforced by predicativity seems sufficient to protect us from such paradoxes, but it does not seem to be absolutely necessary either: systems such as System-F are not predicative yet they are generally believed to be consistent. Some people reject impredicativity outright, and indeed -systems like Agda~\cite{Bove09} demonstrate that impredicativity is not -indispensable to get a powerful logic. Yet, many popular systems, like +systems like Agda~\cite{Bove09} demonstrate that you can go a long way +without impredicativity. Yet, many popular systems, like Coq~\cite{Coq00}, do include some limited form of impredicativity, although those limits tend to feel somewhat ad-hoc, making the overall system more complex, with unsatisfying corner cases. For this reason we feel there @@ -481,8 +464,9 @@ erasability as follows: This version has 4 different abstractions, allowing both System-F's value abstractions $\lambda$ and type abstractions $\Lambda$ to be annotated as either erasable or normal. It is well known that System-F enjoys the phase -distinction~\cite{Cardelli88}, so we could also define an EPTS equivalent -to System-F with only 2 abstractions, using the following rules instead: +distinction~\cite{Cardelli88}, which means that all types can be erased +before evaluating the terms, so we could also define an EPTS equivalent to +System-F with only 2 abstractions, using the following rules instead: \begin{displaymath} \mathcal{R} = \MAlign{ @@ -497,9 +481,9 @@ Figure~\ref{fig:epts} shows the typing rules of our EPTS. Compared to a normal CPTS, the only difference is that the typing rule for functions is split into \textsc{n-Lam} and \textsc{e-Lam} where \textsc{e-Lam} includes the additional constraint $x \not\in \kw{fv}(\Ferase e)$ that enforces the -erasability of the argument. The expression ``$\Ferase e$'' is the \emph{erasure} of $e$, -where the erasure function $\Ferase{(\cdot)}$ erases type annotations as well as -all erasable arguments: +erasability of the argument. The expression ``$\Ferase e$'' is the +\emph{erasure} of $e$, where the erasure function $\Ferase{(\cdot)}$ erases type +annotations as well as all erasable arguments: \begin{displaymath} \begin{array}{l@{\;\;=\;\;}l} \Ferase s & s \\ @@ -512,6 +496,11 @@ all erasable arguments: \end{array} \end{displaymath} 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)$'' +rather than ``$\Ferase e$'' itself. Since the new \textsc{e-Lam} rule is strictly more restrictive than the normal one, it is trivial to show that every EPTS $S$, just like every CPTS, @@ -524,20 +513,6 @@ corresponding PTS is consistent, the EPTS is also consistent. \subsection{Kinds of erasability} -\FIXME{ - Talk a bit more about the different kinds of erasability: - \begin{itemize} - \item There's the one for Coq's Prop and sProp which is similar to "does - not affect the run-time". - \item There's the one that says that dependencies can be erased in CC - (mentioned in Abel's thesis, probably means that you can erase - them and still get a well-typed term). - \item There are more fine distinctions mention in the equality paper of - \cite{Abel12} where he distinguishes those where they can't be used - in a dependent way, and the one restricted to parametricity, etc... - \end{itemize} -} - The claim that arguments to impredicative functions can be erased could be considered as trivial if we consider that Coq's only impredicative universe is \kw{Prop} and that it is also the universe that gets erased during @@ -547,22 +522,28 @@ But the kind of erasability we use in this article is different from that offered by Coq's irrelevance of \kw{Prop}: on the one hand it's more restrictive since the only thing you can do with an erasable argument in an EPTS is to pass it around until you finally put it inside a type annotation, -on the other it's more flexible because any argument can be erasable, +but on the other it's more flexible because any argument can be erasable, regardless of its type. -On a related note, the rules of our EPTS are slightly different from those -of ICC~\cite{Miquel01} and ICC*\cite{Barras08}, in that our \textsc{Conv} -rule requires convertibility of the fully explicit types, whereas ICC and -ICC* use a rule where convertibility is checked after erasure: +In \cite{Abel12}, Abel discusses various other subtly different notions of +erasure. One of the differences he mentions is the difference between +internal and external erasure. The rules of our EPTS are different in this +respect from those of ICC~\cite{Miquel01} and ICC*\cite{Barras08}: our +\textsc{Conv} rule requires convertibility of the fully explicit types +(which corresponds to external erasure), whereas ICC and ICC* use a rule +where convertibility is checked after erasure (so-called internal erasure): \begin{displaymath} \Infer{\Jtype {e} {\tau_1} \\ \Jtype {\tau_2} s \\ \Ferase{\tau_1} \simeq \Ferase{\tau_2}} {\Jtype {e} {\tau_2}} \end{displaymath} -The rule we use is weaker but it is sufficient for our needs and makes it +We use the weaker rule because it is sufficient for our needs and makes it immediately obvious that every well-typed term $e$ in an EPTS $S$ has -a corresponding well-typed term $\Fforget e$ in $\Fforget S$.%% otherwise the +a corresponding well-typed term $\Fforget e$ in $\Fforget S$. +Our results likely carry over to systems with the stronger rule, of course. + +%% otherwise the %% consistency of the corresponding PTS might not automatically carry over to %% the EPTS. @@ -685,12 +666,14 @@ in order to lift the no-SELIT restriction. \subsection{Erasing impredicative arguments of CCω} -\FIXME{Abel mentions in~\cite{Abel13} that in the pure CoC, dependent - arguments are always erasable, but that this doesn't hold any more - once we add inductive types and ``recursion''. Not sure why/how} +%% \FIXME{Abel mentions in~\cite{Abel13} that in the pure CoC, dependent +%% arguments are always erasable, but that this doesn't hold any more +%% once we add inductive types and ``recursion''. Not sure why/how} -In this section we show that impredicative arguments in the calculus of +We will start by showing that impredicative arguments in the calculus of constructions extended with a tower of universes (CCω) are always erasable. +We use CCω because it is arguably the pure type system that is most closely +related to existing systems like Coq. The calculus we use for that can be described by the following EPTS: \newcommand \SMInsertBefore[1]{ @@ -745,7 +728,6 @@ second is redundant: $\tau_2 : \kw{Prop}$ and \ $\exists \ell'$ such that $\tau_1 : \Type {\ell'}$. \end{lemma} \begin{proof} - %% FIXME: Expand! By induction on the type derivation of $e$: \begin{itemize} \item Given $\tau_e : \kw{Prop}$, clearly $e$ is too small to be a type like @@ -829,9 +811,6 @@ as well. %% \JIstep {e}{e'} & \text{$e$ reduces to $e'$} %% \end{array} %% }} \hfill - %% FIXME: This presentation doesn't allow `Con(0,Nat)` but requires - %% substituting every `Nat` with its definition. - %% 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}{e}{x}}} @@ -861,7 +840,7 @@ as well. {\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}} + {\Jcic{\Case{\tau_r}{e}{\vec b}}{\App[n]{\AppM{\tau_r}{p\,}}e}} \Infer{\Jcic \tau s \\ \Jcic[\Gamma,x_f\:\tau] e \tau \\ @@ -874,11 +853,23 @@ as well. \label{fig:cic} \end{figure} -We now extend this result to a calculus of inductive constructions -(CIC). We reuse CCω as the base language and add inductive types to it. +We now extend this result to a calculus of inductive constructions (CIC). +We reuse CCω as the base language and add inductive types to it. The term +CIC has been used to refer to many different systems. Here we use it to +refer to a variant of the ``original'' CIC from 1994, which only had +3 universes, in which we collapsed \kw{Set} and \kw{Prop} into a single +universe (which we call \kw{Prop} even though it is not restricted to be +proof irrelevant like Coq's \kw{Prop}; for readers more familiar with Coq, +our CIC's \kw{Prop} is more like Coq's impredicative \kw{Set}). Note also +that our CIC does have a tower of universes, like Coq, but its inductive +types only exist in the bottom universe, as was the case in the +original CIC. + We mostly follow the presentation of \citet{Gimenez94} for the syntax of inductive types but we extend its rules according to the -presentation of \citet{Werner94} which adds a strong elimination. +presentation of \citet{Werner94} which adds a strong elimination, i.e.~the +ability to compute a type by cases analysis on an inductive type, which is +needed for many proofs, even simple ones. %% The syntax of terms is extended as follows: \begin{displaymath} @@ -1041,7 +1032,7 @@ such as the following to ``smuggle'' a value of universe $\Type \ell$ in a box of universe \kw{Prop}: \begin{verbatim} Inductive Box (t : Type): Prop := - | box : t -> Prop. + | box : t -> Box. Definition unbox (t : Type) (x : Box t) := match x with | box x' => x' end. @@ -1056,22 +1047,23 @@ universes. This was first shown to be inconsistent in \cite{Coquand86b}. This restriction makes the system more complex since elimination is allowed from any inductive type to any universe except for the one special case of strong elimination of large inductive types (SELIT). It also significantly -weakens the system. For example while we can define in Coq a large -inductive type like: +weakens the system. For example, in Coq with the \texttt{-{}-impredicative-set} +option, we can define a large inductive type like: \begin{verbatim} Inductive Ω : Set := | int : Ω | arw : Ω -> Ω -> Ω | all : forall k:Set, (k -> Ω) -> Ω. \end{verbatim} -we cannot prove properties such as the following (which we needed +But we cannot prove properties such as the following (which we needed while working on~\cite{Monnier07}): \begin{verbatim} forall k₁ k₂ f₁ f₂ p, all k₁ f₁ = all k₂ f₂ -> p k₁ f₁ -> p k₂ f₂. \end{verbatim} In practice, this important restriction significantly reduces the -applicability of large inductive types. +applicability of large inductive types (which is arguably part of the reason +why Coq does not allow them in \kw{Set} any more by default). \begin{figure}[bt] \begin{displaymath} @@ -1101,7 +1093,7 @@ applicability of large inductive types. {\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}} + {\Jcic{\Case{\tau_r}{e}{\vec b}}{\App[n]{\AppM{\tau_r}{p\,}}e}} \end{mathpar} \caption{Rules of the ECIC system} \label{fig:ecic} @@ -1200,7 +1192,7 @@ Here is an example of code which relies on this possibility: {\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}} + {\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} @@ -1237,11 +1229,13 @@ eCoq is left for future work. \section{Universe-agnostic impredicativity} -Like all known consistent type systems that support impredicative -definitions, CCω accepts them only in the bottom universe, called \kw{Prop}. -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 \citet{Hurkens95}. +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 +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 +\citet{Hurkens95}. In this section we investigate the use of an erasability constraint in order to lift this restriction and thus allow impredicative definitions in higher @@ -1365,29 +1359,29 @@ not in general sufficient to tame the excesses of impredicativity. \subsection{Inductive types: Impredicative and universe polymorphic?} -\FIXME{ - Look at Nuyts's work on parametricity and impredicativity - %% There is appendix C in the extended version of our own paper: - %% https://people.cs.kuleuven.be/~andreas.nuyts/paper-reldtt.pdf - %% (Warning: the paper itself is extremely dense.) - %% However I was hesitant to pass this immediately as a reference because we - %% are by no means the inventors of this approach and maybe the appendix - %% doesn't emphasize that enough. - - %% Doing dependent elimination of Church encodings (ignoring predicativity - %% issues) WITHIN dependent type theory seems to be possible since the - %% work of Guilhem Moulin - see his PhD thesis: - %% https://www.chalmers.se/en/staff/Pages/guilhem-moulin.aspx - %% - though it seems he was so occupied by cracking the technical problem of - %% having internal parametricity operators that he didn't get around to - %% explaining how to use them. So in this sense I think we *may* be the - %% first ones to spell out how to do this within DTT. - - %% However, similar ideas can be found in earlier work using predicate logic - %% over simple type systems. For example Wadler has some stuff to say about - %% induction on the natural numbers: - %% https://doi.org/10.1016/j.tcs.2006.12.042 -} +%% \FIXME{ +%% Look at Nuyts's work on parametricity and impredicativity +%% %% There is appendix C in the extended version of our own paper: +%% %% https://people.cs.kuleuven.be/~andreas.nuyts/paper-reldtt.pdf +%% %% (Warning: the paper itself is extremely dense.) +%% %% However I was hesitant to pass this immediately as a reference because we +%% %% are by no means the inventors of this approach and maybe the appendix +%% %% doesn't emphasize that enough. + +%% %% Doing dependent elimination of Church encodings (ignoring predicativity +%% %% issues) WITHIN dependent type theory seems to be possible since the +%% %% work of Guilhem Moulin - see his PhD thesis: +%% %% https://www.chalmers.se/en/staff/Pages/guilhem-moulin.aspx +%% %% - though it seems he was so occupied by cracking the technical problem of +%% %% having internal parametricity operators that he didn't get around to +%% %% explaining how to use them. So in this sense I think we *may* be the +%% %% first ones to spell out how to do this within DTT. + +%% %% However, similar ideas can be found in earlier work using predicate logic +%% %% over simple type systems. For example Wadler has some stuff to say about +%% %% induction on the natural numbers: +%% %% https://doi.org/10.1016/j.tcs.2006.12.042 +%% } While paradoxes like Hurkens's suggest that it is impossible to have impredicative definitions in more than one universe without losing @@ -1554,13 +1548,6 @@ can try and compare it to existing systems. \end{displaymath} \newcommand\Ftoa{\MetaFunction{}} Then we define the encoding $\MetaFunction{}{\cdot}$ from System-F to EpCCω: - %% 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 \\ ===================================== refs.bib ===================================== @@ -230,7 +230,7 @@ } @article{Abel12, - author = {Andreas Abel and}, + author = {Andreas Abel and Gabriel Scherer}, journal = {Logical Methods in Computer Science}, number = {1:29}, pages = {1-36}, @@ -285,68 +285,6 @@ more accurate way.}, } -@phdthesis{Abel13, - author = {Andreas Abel}, - month = mar, - school = {Institut für Informatik, - Ludwig-Maximilians-Universität}, - type = {Habilitation thesis}, - title = {Normalization by Evaluation: Dependent Types and - Impredicativity}, - year = {2013}, - abstract = {Normalization by evaluation (NbE) is a technique to - compute the normal form of a lambda-term, i.e., an - expression of a pure functional programming language. - While evaluation is only concerned with computing - closed expressions, normalization also applies to - function bodies, thus, needs to compute with open - expressions containing free variables. NbE reduces - normalization to evaluation of expressions in a - residualizing model, i.e., a computational structure - that has extra base values which are unknowns or - computations blocked by unknowns. Normalization by - evaluation, while not under this name, has been used - by Martin-Löf [1975] to prove normalization and - decidability of type checking for his predicative - intuitionistic type theory with a weak notion of term - equality that is not closed under function - abstraction. Independently, normalization by - evaluation has been discoverd by Berger and - Schwichtenberg [1991] as a tool to implement a - normalizer for simply-typed lambda-calculus with a - strong (extensional, “η”) notion of term - equality. Normalization invokes the evaluator of the - host programming language, leading to a concise and - efficient normalization procedure. In this thesis, we - join the two strands of research by developing NbE - for dependent type theory with extensional term - equality that does consider normalization of function - bodies. Further, we extend NbE to impredicative type - systems such as System F, Fω, and the Calculus of - Constructions. As NbE is a tool to connect syntax - (terms) to semantics (values), the study of NbE - enables us to semantically prove meta-theoretical - properties of the considered type systems such as - decidability of term equality, which entails the - decidability of type checking in the presence of - dependent types. For dependent types with universes - and extensional (η) equality at the level of types, - this is a novel result. The study of NbE provides us - with new insights into the nature of η-expansion - which we apply to dependent type theory with - singleton types. Further, we formulate the concept of - candidate space to equip semantic types with extra - structure that allows us to show the correctness of - NbE. Finally, we introduce typed Kripke structures to - unify semantic arguments by logical relations. The - results underlying this thesis were obtained partly - in collaboration with Klaus Aehlig, Thierry Coquand, - Peter Dybjer, and Miguel Pagano, as far as the design - of the NbE algorithm and its application to - predicative type theory are concerned.}, - url = {http://www.cse.chalmers.se/~abela/habil.pdf}, -} - @techreport{Gimenez94, author = {Eduardo Giménez}, institution = {École Normale Supérieure de Lyon}, @@ -447,6 +385,33 @@ \kw{cast} more obvious.}, } +@inproceedings{Geuvers07, + author = {Herman Geuvers}, + booktitle = {Types for Proofs and Programs}, + key = {TYPES'06}, + pages = {140-159}, + series = {Lecture Notes in Computer Science}, + title = {(In)consistency of Extensions of Higher Order Logic + and Type Theory}, + volume = {4502}, + year = {2006}, + abstract = {It is well-known, due to the work of Girard and + Coquand, that adding polymorphic domains to higher + order logic, HOL, or its type theoretic variant + λHOL, renders the logic inconsistent. This is known + as Girard’s paradox, see [4]. But there is also + another presentation of higher order logic, in its + type theoretic variant called λPREDω, to which + polymorphic domains can be added safely, Both λHOL + and λPREDω are well-known type systems and in this + paper we study why λHOL with polymorphic domains is + inconsistent and why nd λPREDω with polymorphic + domains remains consistent. We do this by describing + a simple model for the latter and we show why this + can not be a model of the first.}, + url = {https://www.cs.ru.nl/~herman/PUBS/inconsist-hol.pdf}, +} + @phdthesis{Girard72, author = {J. Y. Girard}, school = {University of Paris VII}, @@ -557,6 +522,15 @@ year = {1986}, } +@proceedings{TYPES06, + booktitle = {Types for Proofs and Programs}, + key = {TYPES'06}, + series = {Lecture Notes in Computer Science}, + title = {Types for Proofs and Programs}, + volume = {4502}, + year = {2006}, +} + @proceedings{TLCA95, booktitle = {International conference on Typed Lambda Calculi and Applications}, View it on GitLab: https://gitlab.com/monnier/typer/commit/68df8023cc3829519383a617ce38057096a… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/68df8023cc3829519383a617ce38057096a… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/tcvi] WIP
by Stefan 23 Nov '19

23 Nov '19

Stefan pushed to branch report/tcvi at Stefan / Typer Commits: fd3ca2cb by Stefan Monnier at 2019-11-23T19:45:15Z WIP - - - - - 2 changed files: - paper.tex - refs.bib Changes: ===================================== paper.tex ===================================== @@ -264,8 +264,6 @@ might still enjoy consistency. %% a quick overview of the structure. Should be removed before submission. \newpage \tableofcontents -\FIXME{Improve structure} - \section{Introduction} %% General plan: @@ -305,12 +303,12 @@ should look like. Let's disappoint the optimistic reader right away: this paper does not solve this problem. But during the design of our experimental language Typer~\cite{Monnier19}, we noticed an interesting property shared by several -existing impredicative systems which are believed to be consistent, that -seemed to link impredicativity and erasability. Some mathematicians, such -as Carnap~\cite{Fruchart96}, have argued that impredicative quantification -might be acceptable as long as those arguments are not used in what we could -describe as a ``significant'' way, so we investigate here whether -erasability might be such a notion of ``insignificance''. +existing impredicative systems, that seemed to link impredicativity and +erasability. Some mathematicians, such as Carnap~\cite{Fruchart96}, have +argued that impredicative quantification might be acceptable as long as +those arguments are not used in what we could describe as a ``significant'' +way, so in a sense this article investigates here whether erasability might +be such a notion of ``insignificance''. The two main instances of impredicativity in modern type theory are probably Coq's \kw{Prop} universe, which is designed to be erasable, @@ -322,22 +320,31 @@ 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. -Coq and the propositional resizing axiom basically link impredicativity -to the concept of erasure usually called \emph{proof irrelevance}, where an -argument is deemed erasable if its type has at most one inhabitant. In the -following sections, we show an affinity between impredicativity and the -somewhat different notion of erasability found in systems like ICC* and -EPTS~\cite{Barras08,MishraLinger08}, where an argument is deemed erasable if -the function only uses it in type annotations. +Coq and the propositional resizing axiom basically link impredicativity to +the concept of erasure usually called \emph{proof irrelevance}, where an +argument is deemed erasable if its type has at most one inhabitant. +In Section~\ref{sec:prop}, we show a strong affinity between the popular +forms of impredicativity and the somewhat different notion of erasability +found in systems like ICC* and EPTS~\cite{Barras08,MishraLinger08}, where an +argument is deemed erasable if the function only uses it in +type annotations. More specifically, we take various impredicative systems and refine them 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 a few other forms of -impredicativity that are known to break consistency and argue that they look -like nails: by restricting those forms of impredicativity to be erasable we -may be able to recover consistency.%% While there is admittedly ample room in +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. + +%% a few other forms of impredicativity that are known to break consistency and +%% argue that they look like nails: by restricting those forms of +%% impredicativity to be erasable we may be able to recover consistency.%% +%% While there is admittedly ample room in %% the margins, in order not to spoil their pleasure, we carefully leave it as %% an exercise for the readers to prove (or disprove) the consistency of some %% of the resulting extensions. @@ -350,16 +357,18 @@ 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 proposal for how to extend CIC with strong elimination of large - inductive types that might plausibly preserve consistency. -\item A proof that the same idea does not allow impredicativity in more than - one universe. +\item A new calculus ECIC which 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 + which allows more powerful forms of impredicativity, such as a Church + encoding with strong elimination. \item As needed for some of the above contributions, we sketch a calculus with both inductive types and erasability annotations. While this is - straightforward, we do not know of such a system published so far, the - closest we found being the one described by Bernardo~\citet{Bernardo09}. -%% \item The observation that ICC's stronger conversion rule may not be as -%% strong as it seems. \FIXME{really?} + relatively straightforward, we do not know of such a system published so + far, the closest we found being the one described by + Bernardo~\citet{Bernardo09}. \end{itemize} \iflongversion @@ -666,7 +675,15 @@ a corresponding well-typed term $\Fforget e$ in $\Fforget S$.%% otherwise the %% and erasable applications, so to show that they are related would require %% using x_R in the final result type!? -\section{Erasing impredicative arguments of CCω} +\section{Erasable impredicativity in \kw{Prop}} +\label{sec:prop} + +In this section we show that the impredicative quantification in the bottom +universe \kw{Prop} is almost always erasable and armed with this observation +along with some circumstantial evidence, we propose to rely on this property +in order to lift the no-SELIT restriction. + +\subsection{Erasing impredicative arguments of CCω} \FIXME{Abel mentions in~\cite{Abel13} that in the pure CoC, dependent arguments are always erasable, but that this doesn't hold any more @@ -784,7 +801,7 @@ This shows that the erasability of System-F's impredicative type abstractions can be extended to all of CCω's impredicative abstractions as well. -\section{Erasing impredicative arguments of CIC} +\subsection{Erasing impredicative arguments of CIC} \label{sec:cic} \newcommand \Ind[3] {\kw{Ind}(#1\:#2)\langle#3\rangle} @@ -931,10 +948,10 @@ Two important details are worth pointing out: to be in \kw{Prop}: just like in the original CIC we only allow inductive types in our bottom universe, contrary to what systems like Coq~\cite{Coq00} and UTT~\cite{Luo92} allow. -\item In the \kw{Case} rule we have the condition that when the - result of the case analysis is not in \kw{Prop}, i.e.~when this is a form - of strong elimination, the inductive type must be small, meaning that all - its fields must be in \kw{Prop}. This restriction is taken from +\item In the \kw{Case} rule we have the condition that when the result of + the case analysis is not in \kw{Prop}, i.e.~when this is a form of strong + elimination, the inductive type must be small, meaning that all its fields + must be in \kw{Prop}. This ``no-SELIT'' restriction is taken from \citet{Werner94}, with a slightly different presentation because he splits the \kw{Case} rule into two: one for weak elimination and one for strong elimination. @@ -1015,7 +1032,7 @@ abstractions can be extended not only to all of CCω's impredicative abstractions but also to CIC's impredicative abstractions and impredicative inductive types. -\section{Strong elimination of large inductive types} +\subsection{Strong elimination of large inductive types} The reason behind the $\Jsmall e$ special constraint on strong eliminations of CIC in Figure~\ref{fig:cic} is pretty @@ -1038,9 +1055,9 @@ universes. This was first shown to be inconsistent in \cite{Coquand86b}. This restriction makes the system more complex since elimination is allowed from any inductive type to any universe except for the one special case of -strong elimination of large inductive types. It also significantly weakens -the system. For example while we can define in Coq a large inductive type -like: +strong elimination of large inductive types (SELIT). It also significantly +weakens the system. For example while we can define in Coq a large +inductive type like: \begin{verbatim} Inductive Ω : Set := | int : Ω @@ -1050,8 +1067,8 @@ like: we cannot prove properties such as the following (which we needed while working on~\cite{Monnier07}): \begin{verbatim} - forall K₁ K₂ F₁ F₂ P, - all K₁ F₁ = all K₂ F₂ -> P K₁ F₁ -> P K₂ F₂. + forall k₁ k₂ f₁ f₂ p, + all k₁ f₁ = all k₂ f₂ -> p k₁ f₁ -> p k₂ f₂. \end{verbatim} In practice, this important restriction significantly reduces the applicability of large inductive types. @@ -1093,8 +1110,8 @@ applicability of large inductive types. While the $\Jsmall e$ constraint was added to avoid an inconsistency, this same $\Jsmall e$ is also the key to making our proof of erasability of impredicative arguments work for CIC: it is the detail which makes it -possible to erase all the large fields of impredicative inductive -definitions, as we saw in the previous section. +possible to mark all the large fields of impredicative inductive +definitions as erasable, as we saw in the previous section. This might be a coincidence, of course, yet it suggests a close alignment between the needs of consistency and the need to keep impredicative elements erasable. @@ -1105,9 +1122,9 @@ ECIC is more elegant and regular than CIC thanks to the absence of this special corner case, and it allows typing more terms than \kw{e}CIC and hence CIC. For instance in ECIC we can define the above $\Omega$ inductive type with an erasable $k$ and then prove the mentioned property (again with erasable -$K_1$ and $K_2$). +$k_1$ and $k_2$). -Note also that the lack of a $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ rule, +Note also that the lack of an $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ rule, means we cannot define a \texttt{box} as above in this system; instead we are limited to making its content erasable. This in turn prevents us from defining \texttt{unbox} since the \texttt{x'} would now be erasable so it @@ -1120,7 +1137,7 @@ circumstantial evidence, we venture to state the following: The ECIC system is consistent. \end{conjecture} -\section{Non-erasable impredicativity in Coq and UTT} +\subsection{Erasing impredicativity in Coq and UTT} 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 @@ -1218,15 +1235,22 @@ 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} +\section{Universe-agnostic impredicativity} + +Like all known consistent type systems that support impredicative +definitions, CCω accepts them only in the bottom universe, called \kw{Prop}. +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 \citet{Hurkens95}. + +In this section we investigate the use of an erasability constraint in order +to lift this restriction and thus allow impredicative definitions in higher +universes as well. -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 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: +\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: \begin{displaymath} \begin{array}{lcl} \mathcal{S} &=& \{~ *,~\square,~\mathrm{\Delta} ~\} \\ @@ -1335,11 +1359,11 @@ 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 +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} +\subsection{Inductive types: Impredicative and universe polymorphic?} \FIXME{ Look at Nuyts's work on parametricity and impredicativity @@ -1464,7 +1488,7 @@ the universe level parameter $\ell$ needs to be erasable. 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} + \caption{Informal rules of EpCCω} \label{fig:eagda} \end{figure} @@ -1497,20 +1521,21 @@ 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. +Figure~\ref{fig:eagda} describes the resulting calculus we call EpCCω, +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} +\subsection{Encoding System-F in EpCCω} -EAgda is basically a predicative calculus of constructions, with a tower of +EpCCω 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. + EpCCω can encode System-F. \end{theorem} \begin{proof} We take as input a stratified version of System-F, so @@ -1524,11 +1549,11 @@ can try and compare it to existing systems. %% ~|~ \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 + x ~|~ \lambda x\:\tau \to e ~|~ e_1~e_2 ~|~ \lambda t\:* \to e ~|~ e~\tau \end{array} \end{displaymath} \newcommand\Ftoa{\MetaFunction{}} - Then we define the encoding $\MetaFunction{}{\cdot}$ from System-F to EAgda: + Then we define the encoding $\MetaFunction{}{\cdot}$ from System-F to EpCCω: %% FIXME: %% What about Λt₁.Λt₂.id[t₁→t₂→t₁](λx:t₁→λy:t₂→x) ? %% That should turn into @@ -1540,7 +1565,7 @@ can try and compare it to existing systems. \begin{array}{r@{~=~}ll} \MetaFunction{}{\bullet} & \bullet~;~\bullet \\ \MetaFunction{}{\Gamma,x\:\tau} & - \Gamma',x\:\MetaFunction{}{\tau} ~;~ \Delta& + \Gamma',x\:\MetaFunction{\Delta}{\tau} ~;~ \Delta& \text{where }\Gamma';\Delta = \MetaFunction{}{\Gamma}\\ %% \MetaFunction{s}{\Gamma,t\:\kappa} & %% \MetaFunction{s}{\Gamma},t\:\MetaFunction{s}{\kappa} \\ @@ -1562,12 +1587,12 @@ can try and compare it to existing systems. \text{ and } \ell' = \Tlub{1\!\!}{\!\!\Subst{\ell}{0}{l}} \medskip \\ \MetaFunction{\Delta}{x} & x \\ - \MetaFunction{\Delta}{\lambda x\:\tau . e} & + \MetaFunction{\Delta}{\lambda x\:\tau \to 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} & + \MetaFunction{\Delta}{\lambda t\:* \to e} & \Lam[e]{l}{\kw{Level}}{ \Lam[n]{t}{\Type{l}}{ \MetaFunction{\Delta,t:l}{e}}} \\ @@ -1578,7 +1603,7 @@ can try and compare it to existing systems. \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} & + %% \MetaFunction{s}{\lambda t\:\kappa \to \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}} \\ @@ -1586,11 +1611,144 @@ can try and compare it to existing systems. \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}$, + for any $\Jtype{e}{\tau}$ in System-F, we have $\Jtype[\Gamma']{e'}{\tau'}$ and + $\Jtype[\Gamma']{\tau'}{\Type{\ell}}$ in EpCCω where $\Gamma';\Delta = \MetaFunction{}{\Gamma}$, $e' = \MetaFunction{\Delta}{e}$, and $\tau';\ell = \MetaFunction{\Delta}{\tau}$. \end{proof} +\subsection{The power of EpCCω} + +EpCCω is flexible enough to cover the kind of impredicativity found in +Church's encoding or in Chlipala's parametric higher-order abstract +syntax~\cite{Chlipala08}. It does it without restricting impredicativity to +a single universe, and moreover those encodings are more flexible in EpCCω +since as we have seen they support the equivalent of strong elimination. +So in this sense EpCCω is more powerful than systems like CCω. + +Yet we have not been able to generalize the above System-F encoding to +encode System-F$_ω$ into EpCCω. For example, consider the following term: +\begin{displaymath} + λt\:* \to \lambda (f \: *\to*) \to \lambda (x \: f~t) \to x +\end{displaymath} +The first two $\lambda$s should be impredicative, so the encoding should +presumably look like: +\begin{displaymath} + \Lam[e]{l_1}{\kw{Level}}{ + \Lam[n]{t}{\Type{l_1}}{ + \Lam[e]{l_2}{\kw{Level}}{ + \Lam[n]{f}{T_1}{ + \Lam[n]{x}{T_2}{ + x}}}}} +\end{displaymath} +We can then choose $T_1$ and $T_2$ as follows: +\begin{displaymath} + \begin{array}{l@{~=~}l} + T_1 & \Arw[e]{l_3}{\kw{Level}}{\ArwS[n]{\Type{l_3}}{\Type{l_2}}} \\ + T_2 & \App[n]{\App[e]{f}{l_1}}{t} + \end{array} +\end{displaymath} +This makes the term valid, but its semantics doesn't match that of the +original System-F$_\omega$ term since we cannot pass the identity function +$\lambda{}t\:*\to{}t$ as $f$ any more: its encoding would now have type +$\Arw[e]{l_3}{\kw{Level}}{\ArwS[n]{\Type{l_3}}{\Type{l_3}}}$ instead of +the expected $\Arw[e]{l_3}{\kw{Level}}{\ArwS[n]{\Type{l_3}}{\Type{l_2}}}$. + +Similarly, we have not been able to adapt Hurkens's paradox to the EpCCω +system either. Of course, all this says is that we do not know if EpCCω is +consistent, but it seems to indicate that this kind of impredicativity is +incomparable to the traditional form seen in CCω or $\lambda U^-$. + +%% \begin{theorem} +%% EpCCω can encode System-F$_\omega$. +%% \end{theorem} +%% \begin{proof} +%% %% If we try to encode +%% %% +%% %% Λ(t:*).Λ(tf:*→*).λ(x:tf t).x +%% %% +%% %% (l₁) ≡> (t₁:Type l₁) -> (l₂) ≡> (t₂:Type l₂) -> +%% %% (l₃) ≡> (tf: (l₄) ≡> (_ : Type l₄) -> (l₅) ≡> (_ : Type l₅) +%% %% -> Type l₃) -> +%% %% tf {l₁} t₁ {l₂} t₂ +%% We take as input a stratified version of System-F$_\omega$, so +%% as to make an encoding based purely on the syntax rather than the typing +%% derivation. +%% \begin{displaymath} +%% \begin{array}{lccl} +%% \textsl{(kinds)} & \kappa &::=& * ~|~ \kappa_1\to\kappa_2 %% ~|~ (x\:\tau) \to \kappa +%% \\ +%% \textsl{(types)} & \tau &::=& +%% t ~|~ \tau_1\to\tau_2 ~|~ (t\:\kappa)\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\:\kappa.e ~|~ e~\tau +%% \end{array} +%% \end{displaymath} +%% \newcommand\Ftoa{\MetaFunction{}} +%% Then we define the encoding $\MetaFunction{}{\cdot}$ from System-F$_\omega$ to EpCCω: +%% %% 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'}$ and +%% $\Jtype[\Gamma']{\tau'}{\Type{\ell}}$ in EpCCω where $\Gamma';\Delta = \MetaFunction{}{\Gamma}$, $e' +%% = \MetaFunction{\Delta}{e}$, and $\tau';\ell = \MetaFunction{\Delta}{\tau}$. +%% \end{proof} + %% \section{Related work} %% \nocite{Gimenez94} ===================================== refs.bib ===================================== @@ -481,6 +481,42 @@ year = {1995}, } +@inproceedings{Chlipala08, + address = {Victoria, BC}, + author = {Adam Chlipala}, + booktitle = {International Conference on Functional Programming}, + key = {ICFP'08}, + month = sep, + title = {Parametric Higher-Order Abstract Syntax for + Mechanized Semantics}, + year = {2008}, + abstract = {We present parametric higher-order abstract syntax + (PHOAS), a new approach to formalizing the syntax of + programming languages in computer proof assistants + based on type theory. Like higher-order abstract + syntax (HOAS), PHOAS uses the meta language's binding + constructs to represent the object language's binding + constructs. Unlike HOAS, PHOAS types are definable in + general-purpose type theories that support + traditional functional programming, like Coq's + Calculus of Inductive Constructions. We walk through + how Coq can be used to develop certified, executable + program transformations over several statically-typed + functional programming languages formalized with + PHOAS; that is, each transformation has a + machine-checked proof of type preservation and + semantic preservation. Our examples include CPS + translation and closure conversion for simply-typed + lambda calculus, CPS translation for System F, and + translation from a language with ML-style pattern + matching to a simpler language with no variable-arity + binding constructs. By avoiding the syntactic hassle + associated with first-order representation + techniques, we achieve a very high degree of proof + automation.}, + url = {http://adam.chlipala.net/papers/PhoasICFP08/}, +} + @proceedings{FOSSACS08, address = {Budapest, Hungary}, booktitle = {Conference on Foundations of Software Science and @@ -505,6 +541,15 @@ year = {2009}, } +@proceedings{ICFP08, + address = {Victoria, BC}, + booktitle = {International Conference on Functional Programming}, + key = {ICFP'08}, + month = sep, + title = {International Conference on Functional Programming}, + year = {2008}, +} + @proceedings{LICS86, booktitle = {Annual Symposium on Logic in Computer Science}, key = {LICS'86}, View it on GitLab: https://gitlab.com/monnier/typer/commit/fd3ca2cbc8058bdd07348fa294bcec1786d… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/fd3ca2cbc8058bdd07348fa294bcec1786d… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/tcvi] Develop the universe polymorphism a bit more
by Stefan 23 Nov '19

23 Nov '19

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/6c93de259ce482e25b433b2f51ee2defa8c… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/6c93de259ce482e25b433b2f51ee2defa8c… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/tcvi] WIP
by Stefan 22 Nov '19

22 Nov '19

Stefan pushed to branch report/tcvi at Stefan / Typer Commits: 76029de4 by Stefan Monnier at 2019-11-22T16:49:35Z WIP - - - - - 2 changed files: - paper.tex - refs.bib Changes: ===================================== paper.tex ===================================== @@ -314,8 +314,8 @@ describe as a ``significant'' way, so we investigate here whether erasability might be such a notion of ``insignificance''. The two main instances of impredicativity in modern type theory are probably -the typical Coq's \kw{Prop} universe, which is designed to be erasable, -and the propositional resizing axiom~\cite{HoTT} which allows +Coq's \kw{Prop} universe, which is designed to be erasable, +and the propositional resizing axiom~\cite{HoTT} which allows the use of impredicativity for all \emph{mere propositions}, i.e.~types whose 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 @@ -323,7 +323,7 @@ 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. -Coq and and the propositional resizing axiom basically link impredicativity +Coq and the propositional resizing axiom basically link impredicativity to the concept of erasure usually called \emph{proof irrelevance}, where an argument is deemed erasable if its type has at most one inhabitant. In the following sections, we show an affinity between impredicativity and the @@ -426,18 +426,6 @@ Here we present the notion of erasability we use in the rest of the paper. \label{fig:epts} \end{figure}} -\FIXME{ - Talk a bit more about the different kinds of erasability - %% - There's the one for Coq's Prop and sProp which is similar to "does - %% not affect the run-time". - %% - There's the one that says that dependencies can be erased in CC - %% (mentioned in Abel's thesis, probably means that you can erase - %% them and still get a well-typed term). - %% - There are more fine distinctions mention in the equality paper of Abel - %% where he distinguishes those where they can't be used in a dependent - %% way, and the one restricted to parametricity, etc... -} - The calculi we use in this paper are erasable pure type systems (EPTS) \cite{MishraLinger08}, which are pure type systems (PTS)~\cite{Barendregt91b} extended with a notion of erasability. We use @@ -528,6 +516,20 @@ corresponding PTS is consistent, the EPTS is also consistent. \subsection{Kinds of erasability} +\FIXME{ + Talk a bit more about the different kinds of erasability: + \begin{itemize} + \item There's the one for Coq's Prop and sProp which is similar to "does + not affect the run-time". + \item There's the one that says that dependencies can be erased in CC + (mentioned in Abel's thesis, probably means that you can erase + them and still get a well-typed term). + \item There are more fine distinctions mention in the equality paper of + \cite{Abel12} where he distinguishes those where they can't be used + in a dependent way, and the one restricted to parametricity, etc... + \end{itemize} +} + The claim that arguments to impredicative functions can be erased could be considered as trivial if we consider that Coq's only impredicative universe is \kw{Prop} and that it is also the universe that gets erased during @@ -1424,6 +1426,8 @@ 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? +In the rest of this section we will consider one hypothesis, which is that +the universe level parameter $\ell$ is erasable. %% \section{Related work} ===================================== refs.bib ===================================== @@ -229,6 +229,32 @@ year = {1988}, } +@article{Abel12, + author = {Andreas Abel and}, + journal = {Logical Methods in Computer Science}, + number = {1:29}, + pages = {1-36}, + title = {On Irrelevance and Algorithmic Equality in + Predicative Type Theory}, + volume = {8}, + year = {2012}, + abstract = {Dependently typed programs contain an excessive + amount of static terms which are necessary to please + the type checker but irrelevant for computation. To + separate static and dynamic code, several static + analyses and type systems have been put forward. We + consider Pfenning’s type theory with irrelevant + quantification which is compatible with a type-based + notion of equality that respects η-laws. We extend + Pfenning’s theory to universes and large + eliminations and develop its meta-theory. Subject + reduction, normalization and consistency are obtained + by a Kripke model over the typed equality judgement. + Finally, a type-directed equality algorithm is + described whose completeness is proven by a second + Kripke model.}, +} + @inproceedings{Miquel01, author = {Alexandre Miquel}, booktitle = {International conference on Typed Lambda Calculi and @@ -348,6 +374,8 @@ 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/76029de422a039decf30ac7f724b4a4ac5d… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/76029de422a039decf30ac7f724b4a4ac5d… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/tcvi] Add a few FIXMEs while I have them in mind
by Stefan 21 Nov '19

21 Nov '19

Stefan pushed to branch report/tcvi at Stefan / Typer Commits: 67371831 by Stefan Monnier at 2019-11-21T16:29:56Z Add a few FIXMEs while I have them in mind - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -426,6 +426,18 @@ Here we present the notion of erasability we use in the rest of the paper. \label{fig:epts} \end{figure}} +\FIXME{ + Talk a bit more about the different kinds of erasability + %% - There's the one for Coq's Prop and sProp which is similar to "does + %% not affect the run-time". + %% - There's the one that says that dependencies can be erased in CC + %% (mentioned in Abel's thesis, probably means that you can erase + %% them and still get a well-typed term). + %% - There are more fine distinctions mention in the equality paper of Abel + %% where he distinguishes those where they can't be used in a dependent + %% way, and the one restricted to parametricity, etc... +} + The calculi we use in this paper are erasable pure type systems (EPTS) \cite{MishraLinger08}, which are pure type systems (PTS)~\cite{Barendregt91b} extended with a notion of erasability. We use @@ -1328,6 +1340,30 @@ not in general sufficient to tame the excesses of impredicativity. \section{Universe polymorphism} +\FIXME{ + Look at Nuyts's work on parametricity and impredicativity + %% There is appendix C in the extended version of our own paper: + %% https://people.cs.kuleuven.be/~andreas.nuyts/paper-reldtt.pdf + %% (Warning: the paper itself is extremely dense.) + %% However I was hesitant to pass this immediately as a reference because we + %% are by no means the inventors of this approach and maybe the appendix + %% doesn't emphasize that enough. + + %% Doing dependent elimination of Church encodings (ignoring predicativity + %% issues) WITHIN dependent type theory seems to be possible since the + %% work of Guilhem Moulin - see his PhD thesis: + %% https://www.chalmers.se/en/staff/Pages/guilhem-moulin.aspx + %% - though it seems he was so occupied by cracking the technical problem of + %% having internal parametricity operators that he didn't get around to + %% explaining how to use them. So in this sense I think we *may* be the + %% first ones to spell out how to do this within DTT. + + %% However, similar ideas can be found in earlier work using predicate logic + %% over simple type systems. For example Wadler has some stuff to say about + %% induction on the natural numbers: + %% https://doi.org/10.1016/j.tcs.2006.12.042 +} + 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. @@ -1366,8 +1402,10 @@ type system could be described as the following EPTS: 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 +So it 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 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 @@ -1386,6 +1424,8 @@ 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/67371831c77e631c217f3847ba774e09032… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/67371831c77e631c217f3847ba774e09032… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/tcvi] Started the new section on universe polymorphism
by Stefan 20 Nov '19

20 Nov '19

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/9341af95a82fef6cd3a75e93d18918edda8… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/9341af95a82fef6cd3a75e93d18918edda8… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/tcvi] Improve the UTT part
by Stefan 20 Nov '19

20 Nov '19

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/02f30d158a65d4acf393494a75748c18865… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/02f30d158a65d4acf393494a75748c18865… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/tcvi] -
by Stefan 20 Nov '19

20 Nov '19

Stefan pushed to branch report/tcvi at Stefan / Typer Commits: 3bd4089e by Stefan Monnier at 2019-11-20T06:43:56Z - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -357,7 +357,7 @@ The contributions of this work are: \item As needed for some of the above contributions, we sketch a calculus with both inductive types and erasability annotations. While this is straightforward, we do not know of such a system published so far, the - closest we found being the one described by~\citet{Bernardo09}. + closest we found being the one described by Bernardo~\citet{Bernardo09}. %% \item The observation that ICC's stronger conversion rule may not be as %% strong as it seems. \FIXME{really?} \end{itemize} @@ -674,14 +674,14 @@ The calculus we use for that can be described by the following EPTS: (\Type \ell : \Type {\ell+1}) ~~|~~ \ell\in\mathbb{N} ~\} \\ \mathcal{R} &=& \begin{array}[t]{@{}l@{~~|~~}l} - \{~ (k, \kw{Prop}, s, s) - & k \in \{\kw{n},\kw{e}\}, s \in \mathcal{S} ~\} \\ + \{~ (k, \kw{Prop}, s, s) & + k \in \{\kw{n},\kw{e}\}, s \in \mathcal{S} ~\} \\ \SMInsertBefore{\ensuremath{\cup ~}}\{~ - (k, \Type {\ell}, \kw{Prop}, \kw{Prop}) - & k \in \{\kw{n},\kw{e}\}, \ell \in \mathbb{N} ~\} \\ + (k, \Type {\ell}, \kw{Prop}, \kw{Prop}) & + k \in \{\kw{n},\kw{e}\}, \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} ~\} + (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} @@ -739,13 +739,17 @@ second is redundant: \vspace{-\baselineskip} \end{proof} +Let's call \kw{e}CCω the restriction of CCω where all arguments to +impredicative functions are erasable, +i.e.~$(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ is removed. + \begin{theorem}[Erasability of impredicative arguments in CCω] \mbox{} \\ \normalfont %% - CCω's rule $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ is redundant since for any - derivation $\Jtype e \tau$ in CCω there is a corresponding derivation $\Jtype[\Gamma'] - {e'} {\tau'}$ in CCω$'$ which does not use that rule and where - $\Fforget{\Jtype e \tau} = \Fforget{\Jtype[\Gamma'] {e'} {\tau'}}$ + CCω's rule $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ is redundant since for + any derivation $\Jtype e \tau$ in CCω there is a corresponding derivation + $\Jtype[\Gamma'] {e'} {\tau'}$ in \kw{e}CCω such that $\Fforget{\Jtype e \tau} = + \Fforget{\Jtype[\Gamma'] {e'} {\tau'}}$ \end{theorem} \begin{proof} By induction on the type derivation of $e$ where we systematically replace @@ -816,7 +820,7 @@ as well. {\Jcic{\Ind{x}{\tau}{\vec a}}{\tau}} \Infer{\Jcic e {\AppM{\tau_I}{p}} \\ - \tau_I = \Ind{x}{\ArwM{z}{\tau_z}{\kw{Prop}}}{\vec a} \\ + \tau_I = \Ind{x}{\ArwM{z}{\tau_z}{{Prop}}}{\vec a} \\ \Jcic {\tau_r}{\ArwM{z}{\tau_z}{\Arw[n]{\_}{\AppM{\tau_I}{z}}s}} \\\\ \forall i. \\ a_i = {\ArwM[\ensuremath{c}]{y}{\tau_y}{\AppM{x}{p'}}} \\ @@ -917,7 +921,7 @@ Two important details are worth pointing out: result of the case analysis is not in \kw{Prop}, i.e.~when this is a form of strong elimination, the inductive type must be small, meaning that all its fields must be in \kw{Prop}. This restriction is taken from - \citet{Werner94} who presents it slightly differently because he splits + \citet{Werner94}, with a slightly different presentation because he splits the \kw{Case} rule into two: one for weak elimination and one for strong elimination. \end{itemize} @@ -928,16 +932,17 @@ that recursive calls are made on structurally smaller terms. Their definition is not affected by the presence of erasability annotations and does not impact our work here. -To show that the $(\kw{n}, s, \kw{Prop}, \kw{Prop})$ rule of non-erasable +To show that the $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ rule of non-erasable impredicativity is still redundant in this new system, we proceed in the same way: \begin{lemma}[Confinement of impredicativity in CIC] \label{lem:erasable-cic} \mbox{} \\ \normalfont %% FIXME: Make it a bit more formal? - In CIC, if $\Jtype{x}{\tau_x : \Type \ell}$ and + In CIC, if $\Jtype{x}{\tau_x:\Type{\ell}}$ and $\Jtype[\Gamma,x\:\tau_x,\Gamma']{e}{\tau_e:\kw{Prop}}$, then $x$ can only appear in - $\Ferase e$ within arguments of function calls where the function has type - $(y\:\tau_1) \TEarw \tau_2$ where $\tau_1 : \Type {\ell'}$ and $\tau_2 : \kw{Prop}$. + $\Ferase e$ within arguments to functions of type + $(y\:\tau_1) \TEarw \tau_2$ where $\tau_2:\kw{Prop}$ and $\exists \ell'$ such that + $\tau_1:\Type{\ell'}$. \end{lemma} \begin{proof} The proof stays the same, with the following additional cases: @@ -955,20 +960,26 @@ way: $b_i$ are as well, hence we can also invoke the induction hypothesis on every $b_i$. %% \qed \end{itemize} + \vspace{-\baselineskip} \end{proof} + +Let's call \kw{e}CIC the restriction of CIC where all arguments to +impredicative functions and all large fields of inductive definitions are +erasable, i.e.~$(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ is removed. + \begin{theorem}[Erasability of impredicative arguments in CIC] \mbox{} \\ \normalfont %% - CIC's rule $(\kw{n}, s, \kw{Prop}, \kw{Prop})$ is redundant since for any + CIC's rule $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ is redundant since for any derivation $\Jtype e \tau$ in CIC there is a corresponding derivation $\Jtype[\Gamma'] - {e'} {\tau'}$ in CIC$'$ which does not use that rule and where + {e'} {\tau'}$ in \kw{e}CIC such that $\Fforget{\Jtype e \tau} = \Fforget{\Jtype[\Gamma'] {e'} {\tau'}}$ \end{theorem} \begin{proof} As before, by induction on the type derivation of $e$ where we systematically replace $\kw{n}$ with $\kw{e}$ on all functions, arrows, - and applications that previously relied on the rule $(\kw{n}, s, - \kw{Prop}, \kw{Prop})$. + and applications that previously relied on the rule + $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$. The interesting new case is when $e$ is of the form $\Case{\tau_r}{e'}{\vec b}$: as mentioned, the vector $\vec c$ of erasability annotations placed on a given constructor $a_i$ must match the erasability @@ -981,8 +992,8 @@ way: for functions in \kw{Prop} can only be annotated as erasable. And when $s$ is a higher universe the property is also verified because the $\Jsmall {\vec {\tau_y}}$ constraint imposes that none of the arguments are - in higher universes so they don't use the $(\kw{n}, s, \kw{Prop}, - \kw{Prop})$ rule. %% \qed + in higher universes so they don't use the + $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ rule. %% \qed \end{proof} This shows that the erasability of System-F's impredicative type @@ -994,7 +1005,7 @@ inductive types. The reason behind the $\Jsmall e$ special constraint on strong eliminations of CIC in Figure~\ref{fig:cic} is pretty -straightforward: without this restriction, we could use an Inductive type +straightforward: without this restriction, we could use an inductive type such as the following to ``smuggle'' a value of universe $\Type \ell$ in a box of universe \kw{Prop}: \begin{verbatim} @@ -1009,7 +1020,7 @@ constraint rejects the \texttt{unbox} definition. If we remove the $\Jsmall e$ constraint, the effect of such a \texttt{box}/\texttt{unbox} pair would be to lower any value of a higher universe to the \kw{Prop} universe and would hence defeat the purpose of the stratification introduced by the tower of -universes. This was first shown to be inconsistent by \citet{Coquand86b}. +universes. This was first shown to be inconsistent in \cite{Coquand86b}. This restriction makes the system more complex since elimination is allowed from any inductive type to any universe except for the one special case of @@ -1035,13 +1046,16 @@ applicability of large inductive types. \begin{displaymath} \begin{array}{lcl} \mathcal{R} &=& - \MAlign{ - \{~ (k, \kw{Prop}, s, s); - (\kw{e}, s, \kw{Prop}, \kw{Prop}) ~|~ s \in \mathcal{S} ~\} \\ - \cup ~\{~ - (k, \Type {\ell_1}, \Type {\ell_2}, \Type {\Tmax{\ell_1}{\ell_2}}) - ~|~ \ell_1,\ell_2 \in\mathbb{N} ~\} - } + \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}) & + k \in \{\kw{n},\kw{e}\}, \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} @@ -1063,28 +1077,27 @@ applicability of large inductive types. \end{figure} While the $\Jsmall e$ constraint was added to avoid an inconsistency, this -same $\Jsmall e$ is also the key to making it possible to erase all the -large fields of impredicative inductive definitions, as we saw in the -previous section. - -Figure~\ref{fig:ecic} shows a refinement of CIC we call ECIC: just like -CIC$'$, it only has the $(\kw{e},s,\kw{Prop},\kw{Prop})$ rule and not the -$(\kw{n},s,\kw{Prop},\kw{Prop})$ rule, meaning that impredicativity can only -be used with erasable arguments and fields. But additionally it has -a further difference to CIC and CIC$'$ which is that its \kw{Case} rule does -not have the $\Jsmall e$ constraint. - +same $\Jsmall e$ is also the key to making our proof of erasability of +impredicative arguments work for CIC: it is the detail which makes it +possible to erase all the large fields of impredicative inductive +definitions, as we saw in the previous section. +This might be a coincidence, of course, yet it suggests a close alignment +between the needs of consistency and the need to keep impredicative +elements erasable. + +Figure~\ref{fig:ecic} shows a refinement of \kw{e}CIC we call ECIC whose +\kw{Case} rule does not have the $\Jsmall e$ constraint. ECIC is more elegant and regular than CIC thanks to the absence of this -special corner case, and it allows typing more terms than CIC$'$ and hence +special corner case, and it allows typing more terms than \kw{e}CIC and hence CIC. For instance in ECIC we can define the above $\Omega$ inductive type with an erasable $k$ and then prove the mentioned property (again with erasable $K_1$ and $K_2$). -Note also that the lack of a $(\kw{n},s,\kw{Prop},\kw{Prop})$ rule, means we -cannot define a \texttt{box} as above in this system; instead we are limited -to making its content erasable. This in turn prevents us from defining -\texttt{unbox} since the \texttt{x'} would now be erasable so it cannot be -returned as-is from the elimination form. In other words, forcing +Note also that the lack of a $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ rule, +means we cannot define a \texttt{box} as above in this system; instead we +are limited to making its content erasable. This in turn prevents us from +defining \texttt{unbox} since the \texttt{x'} would now be erasable so it +cannot be returned as-is from the elimination form. In other words, forcing impredicative fields to be erasable also avoids this source of inconsistency usually avoided with the $\Jsmall e$ constraint. Based on this circumstantial evidence, we venture to state the following: @@ -1093,11 +1106,56 @@ circumstantial evidence, we venture to state the following: The ECIC system is consistent. \end{conjecture} +\section{Non-erasable impredicativity in Coq and UTT} + +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: +\begin{verbatim} + Inductive Ω : Type := + | int : Ω + | arw : Ω -> Ω -> Ω + | all : forall k:Type, (k -> Ω) -> Ω. +\end{verbatim} + +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: + + \section{Multiple levels of impredicativity} -CCω accepts impredicative definitions but only in the bottom universe. -This is a restriction shared by all systems that support impredicative -definitions. This is a direct consequence of various paradoxes formalized +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 \citet{Hurkens95}. The last two showed a paradox in the system $\lambda U^-$ @@ -1108,16 +1166,18 @@ which can be defined as an EPTS as follows: \mathcal{A} &=& \{~ (*,~\square), (\square,~\mathrm{\Delta}) ~\} \\ \mathcal{R} &=& \{~ \MAlign{ - (k,*,*,*),~(k,\square,*,*),~(k,\mathrm{\Delta},*,*), \\ + (k,*,*,*),~(k,\square,*,*),~%% ~(k,\mathrm{\Delta},*,*), + %% \\ (k,\square,\square,\square),~(k,\mathrm{\Delta},\square,\square) \hspace{40pt}~|~ k \in \{\kw{n},\kw{e}\} ~\} } \end{array} \end{displaymath} -Of the five pairs of rules, three are impredicative: $(k,\square,*,*)$, -$(k,\mathrm{\Delta},*,*)$, and $(k,\mathrm{\Delta},\square,\square)$, but since $*$ is the bottom -universe and hence corresponds to \kw{Prop} in CCω, the first two are -generally considered safe and are included in CCω. The new one is +Of the four pairs of rules, two are impredicative: $(k,\square,*,*)$ %% , +%% $(k,\mathrm{\Delta},*,*)$, +and $(k,\mathrm{\Delta},\square,\square)$, but since $*$ is the bottom +universe and hence corresponds to \kw{Prop} in CCω, the first is +generally considered safe and is included in System-F and CCω. The new one is $(k,\mathrm{\Delta},\square,\square)$ which introduces impredicativity in the second universe, $\square$. @@ -1127,16 +1187,15 @@ be shown. The statement of the lemma would look like the following: \label{lem:erasable-lU} \mbox{} \\ \normalfont In $\lambda U^-$, if $\Jtype{x}{\tau_x : s_1}$ and $\Jtype[\Gamma,x\:\tau_x,\Gamma']{e}{\tau_e:s_2}$ and $s_1 > s_2$, then $x$ can only - appear in $\Ferase e$ within arguments to functions of type $(y\:\tau_1) - \TEarw \tau_2$ where $\tau_1 : s_3$ and $\tau_2 : s_4$ and $s_3 > s_4$. + appear in $\Ferase e$ within arguments to functions of type + $(y\:\tau_1)\TEarw \tau_2$ where $\tau_1 : s_3$ and $\tau_2 : s_4$ and $s_3 > s_4$. \end{lemma} -When we attempt to adapt the earlier proof for CCω, most of the proof works -largely unchanged, except when we get to the case where $e$ is of the form -$\Arw{y}{\tau_1}{\tau_2}$: we can invoke the induction hypothesis on $\tau_2$ because -it necessarily lives in the same universe as $e$, but we cannot invoke the -induction hypothesis on $\tau_1$ if $x$ is in the universe $\mathrm{\Delta}$, -because $\tau_1$ might itself also be in the universe $\mathrm{\Delta}$ because of -the $(k,\mathrm{\Delta},\square,\square)$ rule. +When we attempt to adapt the earlier proof for CCω, is breaks down when $e$ +is of the form $\Arw{y}{\tau_1}{\tau_2}$: we can invoke the induction hypothesis +on $\tau_2$ because it necessarily lives in the same universe as $e$, but we +cannot invoke the induction hypothesis on $\tau_1$ if $x$ is in the universe +$\mathrm{\Delta}$, because $\tau_1$ might itself also be in the universe +$\mathrm{\Delta}$ because of the $(k,\mathrm{\Delta},\square,\square)$ rule. \begin{figure}[tb] \begin{displaymath} @@ -1172,15 +1231,15 @@ the $(k,\mathrm{\Delta},\square,\square)$ rule. \label{fig:hurkens} \end{figure} -Following the same idea as in the previous section where we relied on -erasability to avoid inconsistency, we could thus define a new $\lambda EU^-$ -calculus that only allows the use of impredicativity with erasable +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 abstractions: \begin{displaymath} \begin{array}{lcl} \mathcal{R} &=& \{~ \MAlign{ - (k,*,*,*),~(\kw{e},\square,*,*),~(\kw{e},\mathrm{\Delta},*,*), \\ + (k,*,*,*),~(\kw{e},\square,*,*),~%% (\kw{e},\mathrm{\Delta},*,*), \\ (k,\square,\square,\square),~(\kw{e},\mathrm{\Delta},\square,\square) \hspace{40pt}~|~ k \in \{\kw{n},\kw{e}\} ~\} } @@ -1194,14 +1253,14 @@ this is not the case: $\lambda EU^-$ is not consistent. \end{theorem} \begin{proof} - The proof is the same as the proof of inconsistency of $\lambda U^-$ shown by + 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 impredicative abstractions can be annotated as erasable. For that, it - suffices to know that the integers are variable names, the two - impredicative abstractions in $*$ are introduced by \kw{let}, the two - corresponding applications are denoted with $\langle e_1~e_2\rangle$, the + suffices to know that the integers are variable names, the + impredicative abstraction in $*$ is introduced by \kw{let}, the + corresponding application is denoted with $\langle e_1~e_2\rangle$, the impredicative abstraction in $\square$ is introduced by $\Lambda$, and the corresponding application is denoted with $\{e_1~e_2\}$: by inspection we can see that all the arguments introduced by impredicative abstractions @@ -1209,25 +1268,6 @@ this is not the case: impredicative functions. %% \qed \end{proof} -\section{Non-erasable impredicativity} - -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. 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 (at least not in the sense we use -here), showing clearly that while impredicativity and erasability seem to be -correlated, erasability is not a necessary condition for impredicativity to -be consistent. - %% \section{Related work} %% \nocite{Gimenez94} View it on GitLab: https://gitlab.com/monnier/typer/commit/3bd4089e00cfe9f7c6495e792f8171c2d66… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/3bd4089e00cfe9f7c6495e792f8171c2d66… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Novembre 2019