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/%7D 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/89b5f9db65d8aafa227778744ac365c4622c...