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/76029de422a039decf30ac7f724b4a4ac5d1...