Stefan pushed to branch report/tcvi at Stefan / Typer

Commits: f634006a by Stefan Monnier at 2019-11-19T20:02:24Z Tweak the abstract

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -242,11 +242,15 @@ \begin{abstract} Of all the threats to the consistency of a type system, such as side effects and recursion, impredicativity is arguably the least understood. In this -paper, we revisit several type systems which do include some form of -impredicativity and show that they can be refined to equivalent systems -where impredicative quantification can be erased, in a stricter sense than -the kind of proof irrelevance notion used for example for \kw{Prop} terms in -systems like Coq. +paper, we try to investigate it using a kind of blackbox reverse-engineering +approach to map the landscape. We look at it with a particular focus on +its interaction with the notion of erasability. + +More specifically, we revisit several type systems believed to be consistent +and which do include some form of impredicativity and show that they can be +refined to equivalent systems where impredicative quantification can be +marked as erasable, in a stricter sense than the kind of proof irrelevance +notion used for example for \kw{Prop} terms in systems like Coq.

We hope these observations will lead to a better understanding of why and when impredicativity can be sound. As a first step in this direction, we @@ -679,7 +683,7 @@ And we will now show that the second is redundant: 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_1 : \Type {\ell'}$ and $\tau_2 : \kw{Prop}$. + $\tau_2 : \kw{Prop}$ and \ $\exists \ell'$ such that $\tau_1 : \Type {\ell'}$. \end{lemma} \begin{proof} %% FIXME: Expand! @@ -764,7 +768,8 @@ as well. \Jcic e \tau} {\Jcic{\Con{i}{e}}{\Subst{a_i}{x}{e}}}

- \Infer{\forall i. \ \Jtype {\tau} {\tau_i} \ \Jtype {\tau_i} {\kw{Prop}}} + \Infer{\forall i. %% \ \Jtype {\tau} {\tau_i} + \ \Jtype {\tau_i} {\kw{Prop}}} {\Jsmall {\vec \tau}}

%% Actual typing rules

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