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%7D, -} - @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%7D, +} + @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/68df8023cc3829519383a617ce38057096a2...