[Git][monnier/typer][report/tcvi] - - Typer

15 Nov 2018


      Stefan pushed to branch report/tcvi at Stefan / Typer
Commits:
64359fcf by Stefan Monnier at 2018-11-15T22:33:09Z
-
- - - - -
2 changed files:
- paper.tex
- refs.bib
Changes:
=====================================
paper.tex
=====================================
@@ -58,21 +58,22 @@
 \renewcommand \cite \citep
\DeclareUnicodeCharacter{03A9}{\ensuremath{\Omega}}
+\DeclareUnicodeCharacter{03B1}{\ensuremath{\alpha}}
+\DeclareUnicodeCharacter{03BB}{\ensuremath{\lambda}}
+\DeclareUnicodeCharacter{03C3}{\ensuremath{\sigma}}
+\DeclareUnicodeCharacter{03C4}{\ensuremath{\tau}}
 \DeclareUnicodeCharacter{03C9}{\ensuremath{\omega}}
-\DeclareUnicodeCharacter{2203}{\ensuremath{\exists}}
-\DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}}
-\DeclareUnicodeCharacter{21DB}{\ensuremath{\Rrightarrow}}
-\DeclareUnicodeCharacter{2980}{\ensuremath{|||}}
+\DeclareUnicodeCharacter{0394}{\ensuremath{\Delta}}
 \DeclareUnicodeCharacter{2081}{\ensuremath{_1}}
 \DeclareUnicodeCharacter{2082}{\ensuremath{_2}}
 \DeclareUnicodeCharacter{21D2}{\ensuremath{\Rightarrow}}
+\DeclareUnicodeCharacter{21DB}{\ensuremath{\Rrightarrow}}
 \DeclareUnicodeCharacter{2200}{\ensuremath{\forall}}
-\DeclareUnicodeCharacter{03C3}{\ensuremath{\sigma}}
-\DeclareUnicodeCharacter{03BB}{\ensuremath{\lambda}}
-\DeclareUnicodeCharacter{03C4}{\ensuremath{\tau}}
-\DeclareUnicodeCharacter{0394}{\ensuremath{\Delta}}
-\DeclareUnicodeCharacter{1D4C5}{\ensuremath{\wp}}
+\DeclareUnicodeCharacter{2203}{\ensuremath{\exists}}
+\DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}}
+\DeclareUnicodeCharacter{2980}{\ensuremath{|||}}
 \DeclareUnicodeCharacter{1D4B0}{\ensuremath{\mathcal{U}}}
+\DeclareUnicodeCharacter{1D4C5}{\ensuremath{\wp}}
%% The doc says `vcenter` should work, but I get an error :-(
 %% \newcommand \Infer[1][] [\inferrule*[vcenter,right=#1]]
@@ -140,7 +141,7 @@
 %%                                   %% can be repeated if necessary;
 %%                                   %% contents suppressed with 'anonymous'
-\author{Stefan Monnier}
+\author{Stefan Monnier\inst{1} \and  Nathaniel Bos\inst{2}}
 %% \affiliation{
 %%   %% \department{DIRO}
 %%   \institution{Université de Montréal - DIRO}
@@ -150,6 +151,9 @@
 \institute{
   Université de Montréal - DIRO \
   \email{monnier@iro.umontreal.ca}
+  \and
+  McGill University - SCS \
+  \email{nathaniel.bos@mail.mcgill.ca}
 }
%% \author{Other author}
@@ -217,7 +221,7 @@ might still enjoy consistency.
 %%   Discuss how SELIT enters into the picture.
 %% - Maybe discuss UTT and Coq and how they don't fit this model.
-Propositions such as ``This is a lie!'' and other diagonalization proofs
+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
 \emph{type} as well as \emph{predicativity} (and its inverse).
@@ -248,12 +252,12 @@ then show that all places that make use of impredicativity can be annotated
 as erasable.
Armed with this proverbial hammer, we then look at a few other forms of
-impredicativity that break consistency and argue that they 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) that the resulting extensions are
-indeed consistent.
+impredicativity that 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.
The contributions of this work are:
 \begin{itemize}
@@ -376,10 +380,10 @@ erasability as follows:
   \end{array}
 \end{displaymath}
 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 \emph{phase distinction},
-so we could also define an EPTS equivalent to System-F with only
-2 abstractions, using the following rules instead:
+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:
 \begin{displaymath}
     \mathcal{R} =
         \MAlign{
@@ -394,7 +398,7 @@ 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.  ``$\Ferase e$'' is the \emph{erasure} of $e$,
+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}
@@ -445,7 +449,7 @@ every well-typed term $e$ in an EPTS $S$ has a corresponding well-typed term
 $\Fforget e$ in $\Fforget S$, so the consistency of the corresponding PTS
 would not automatically carry over to the EPTS.
-\citet{Barras08} argues in favor of using such a stronger rule by showing
+\citet{Barras08} argue in favor of using such a stronger rule by showing
 some example applications where it is able to equate more terms by erasing
 (and hence ignoring) some proofs, in a sense internalizing a form of proof
 irrelevance similar to that of Coq.  But those examples all rely on
@@ -564,27 +568,30 @@ The calculus we use for that can be described by the following EPTS:
     \mathcal{S} &=& {~ \kw{Prop}; \Type \ell ~|~ \ell\in\mathbb{N} ~} \
     \mathcal{A} &=&
         {~ (\kw{Prop} : \Type 0);
-        (\Type \ell : \Type {\ell+1}) ~|~ \ell\in\mathbb{N} ~} \
+        (\Type \ell : \Type {\ell+1}) ~~|~~ \ell\in\mathbb{N} ~} \
     \mathcal{R} &=&
         \MAlign{
           {~ (k, \kw{Prop}, s, s);
-          (k, s, \kw{Prop}, \kw{Prop}) ~|~ s \in \mathcal{S} ~} \
+          (k, s, \kw{Prop}, \kw{Prop})
+          ~~|~~ s \in \mathcal{S}, k \in {\kw{n},\kw{e}} ~} \
           \cup ~{~
-          (k, \Type {\ell_1}, \Type {\ell_2}, \Type {\ell_1 \sqcup \ell_2})
-          ~|~ \ell_1,\ell_2 \in\mathbb{N} ~}
+          (k, \Type {\ell_1}, \Type {\ell_2}, \Type {\Tmax{\ell_1}{\ell_2}})
+          ~~|~~ \ell_1,\ell_2 \in\mathbb{N}, k \in {\kw{n},\kw{e}} ~}
         }
   \end{array}
 \end{displaymath}
 This calculus follows the tradition of having a special impredicative
 \kw{Prop} universe with a tower of predicative universes named $\Type \ell$.
+$\Tmax{\ell_1}{\ell_2}$ denotes simply the least upper bound of $l_1$ and $l_2$.
The calculus $\Fforget{\text{CCω}}$ we get by removing the erasability
-annotations is sometimes also called CCω.  And indeed the two are
-equivalent: we can see that any well-typed term $e$ in $\Fforget{\text{CCω}}$
-has a corresponding well-typed term $\lceil e\rceil$ in CCω such that $\Fforget{\lceil e\rceil}
-= e$ by simply making $\lceil\cdot\rceil$ add \kw{n} annotations everywhere.
-Our calculus CCω is incidentally almost identical to the ICC* calculus of
-\citet{Barras08} (except for the \textsc{Conv} rule, as discussed above).
+annotations is sometimes also called CCω in the literature.  And indeed the
+two are equivalent: we can see that any well-typed term $e$ in
+$\Fforget{\text{CCω}}$ has a corresponding well-typed term $\lceil e\rceil$ in CCω
+such that $\Fforget{\lceil e\rceil} = e$ by simply making $\lceil\cdot\rceil$ add \kw{n} annotations
+everywhere.  Our calculus CCω is incidentally almost identical to the ICC*
+calculus of \citet{Barras08} (except for the \textsc{Conv} rule, as
+discussed above).
With respect to impredicativity, the relevant rule in CCω is: $(k, s,
 \kw{Prop}, \kw{Prop})$ which allows functions in \kw{Prop} to take arguments
@@ -625,7 +632,7 @@ And we will now show that the second is redundant:
   %%
   CCω's rule $(\kw{n}, s, \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
+  {e'} {\tau'}$ in CCω$'$ which does not use that rule and where
   $\Fforget{\Jtype e \tau} = \Fforget{\Jtype[\Gamma'] {e'} {\tau'}}$
 \end{theorem}
 \begin{proof}
@@ -633,7 +640,7 @@ And we will now show that the second is redundant:
   $\kw{n}$ with $\kw{e}$ on all functions, arrows, and applications that
   previously relied on the rule $(\kw{n}, s, \kw{Prop}, \kw{Prop})$.
   Since the erasability annotation is only used in the typing rule of
-  $\lambda$-abstractions, the proof follows trivial for all cases except this one.
+  $\lambda$-abstractions, the proof follows trivially for all cases except this one.
   For $\lambda$-abstractions that had an \kw{n} annotation that we need to convert
   to \kw{e}, we need to satisfy the additional condition that $x \not\in
   \kw{fv}(\Ferase e)$, which follows from Lemma~\ref{lem:erasable}: In the
@@ -757,6 +764,7 @@ handle those additional terms:
     \Ferase {\Con{i}{e}} & \ConE{i} \
     \Ferase {\Case{\tau_r}{e}{\vec b}} &
         \CaseE{\Ferase e}{\overrightarrow {\Ferase b}} \
+    %% FIXME: Dropping the $i$ makes the reduction semantics tricky.
     \Ferase {(\Fix{i}{x}{\tau}{e})} & \FixE{x}{\Ferase e}
   \end{array}
 \end{displaymath}
@@ -788,15 +796,15 @@ annotations placed on a given constructor $a_i$ must match the erasability
 annotations of the arguments expected by the corresponding branch $b_i$.
 Two important details are worth pointing out:
 \begin{itemize}
-\item First, in the rule for \kw{Ind} the type of constructors is restricted
-  to be in \kw{Prop}: just like in CIC we only allow inductive types in our
-  bottom universe, contrary to what systems like Coq~\cite{Coq00} and
-  UTT~\cite{Luo92} allow.
-\item Second in the \kw{Case} rule we have the condition that when the
+\item In the rule for \kw{Ind} the type of constructors is restricted
+  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
-  \citet{Werner94} which presents it slightly differently because he splits
+  \citet{Werner94} who presents it slightly differently because he splits
   the \kw{Case} rule into two: one for weak elimination and one for
   strong elimination.
 \end{itemize}
@@ -808,7 +816,7 @@ 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
-impredicativity is still redundant in this new system, we proceed in the say
+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} \ \normalfont
@@ -828,9 +836,9 @@ way:
   \item If $e$ is of the form $\Fix{i}{x}{\tau}{e'}$, then $\tau$ does not matter
     because it's erased, and we can invoke the inductive hypothesis on $e'$.
   \item If $e$ is of the form $\Case{\tau_r}{e'}{\vec b}$, then $\tau_r$ does not
-    matter because it's erased,  Also we know $e'$ is in $\kw{Prop}$ since
+    matter because it's erased.  Also we know $e'$ is in $\kw{Prop}$ since
     all our inductive types are in $\kw{Prop}$, so we can invoke the
-    inductive hypothesis on $e'$.  Also since $e$ in is $\kw{Prop}$, all
+    inductive hypothesis on $e'$.  Also since $e$ is in $\kw{Prop}$, all
     $b_i$ are as well, hence we can also invoke the induction hypothesis on
     every $b_i$. \qed
   \end{itemize}
@@ -840,7 +848,7 @@ way:
   %%
   CIC's rule $(\kw{n}, s, \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 CIC$'$ which does not use that rule and where
   $\Fforget{\Jtype e \tau} = \Fforget{\Jtype[\Gamma'] {e'} {\tau'}}$
 \end{theorem}
 \begin{proof}
@@ -849,7 +857,7 @@ way:
   and applications that previously relied on the rule $(\kw{n}, s,
   \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
+  as mentioned, the vector $\vec c$ of erasability
   annotations placed on a given constructor $a_i$ must match the erasability
   annotations of the arguments expected by the corresponding branch $b_i$.
   Since our inductive types all live in \kw{Prop}, it means all fields that
@@ -918,7 +926,7 @@ applicability of large inductive types.
             {~ (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 {\ell_1 \sqcup \ell_2})
+            (k, \Type {\ell_1}, \Type {\ell_2}, \Type {\Tmax{\ell_1}{\ell_2}})
             ~|~ \ell_1,\ell_2 \in\mathbb{N} ~}
           }
     \end{array}
@@ -947,14 +955,14 @@ 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
+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
+a further difference to CIC and CIC$'$ which is that its \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 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$).
@@ -993,7 +1001,7 @@ which can be defined as an EPTS as follows:
         }
   \end{array}
 \end{displaymath}
-Of the five sets of rules, three are impredicative: $(k,\square,*,*)$,
+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
@@ -1017,7 +1025,7 @@ 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}
+\begin{figure}[tb]
   \begin{displaymath}
     \begin{array}{c}
       \begin{array}{l@{;;=;;}l}
@@ -1095,7 +1103,7 @@ 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 of the outlawing of
+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.
@@ -1118,10 +1126,10 @@ be consistent.
 \section{Conclusion}
We have taken a tour of the interactions between impredicativity and
-erasability of arguments in EPTS.  We have shown that 3 of the most well
-known systems that admit impredicativity do it in a way to constrains all
+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
-while impredicativity and erasability seem to be correlated, erasability is
+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.
@@ -1134,9 +1142,6 @@ types without breaking consistency.
 \newcommand \grantsponsor[3] {#2 (#1)}
 \newcommand \grantnum[2] {#2}
 \begin{acks}
-  Thanks to Nathaniel who completed an earlier version of the proof
-  of erasability of impredicative arguments in CCω.
-
   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
=====================================
refs.bib
=====================================
@@ -24,7 +24,7 @@
                    Instead it has an Emacs-based interface which allows
                    programming by gradual refinement of incomplete
                    type-correct terms.},
-  url =           {http://www.cse.chalmers.se/~ulfn/papers/tphols09/
+  url =           {http://www.cse.chalmers.se/%5C~%7B%7Dulfn/papers/tphols09/
                   tutorial.pdf},
 }
@@ -95,7 +95,7 @@
                    into the implicit calculus helps to reflect the
                    computational meaning of the underlying terms in a
                    more accurate way.},
-  url =           {https://www.fing.edu.uy/~amiquel/publis/tlca01.pdf%7D,
+  url =           {https://www.fing.edu.uy/%5C~%7B%7Damiquel/publis/tlca01.pdf%7D,
 }
@inproceedings{Barras08,
@@ -128,8 +128,8 @@
                    static information. We also illustrate the main
                    features of ICC∗ on classical examples of
                    dependently typed programs.},
-  url =           {http://www.lix.polytechnique.fr/~bernardo/writings/barras-
-                  bernardo-icc-fossacs08.pdf},
+  url =           {http://www.lix.polytechnique.fr/%5C~%7B%7Dbernardo/writings/
+                  barras-bernardo-icc-fossacs08.pdf},
 }
@inproceedings{MishraLinger08,
@@ -244,6 +244,13 @@
   url =           {http://doi.acm.org/10.1017/S0956796812000056%7D,
 }
+@misc{Cardelli88,
+  author =        {Luca Cardelli},
+  howpublished =  {DEC-SRC manuscript},
+  title =         {Phase Distinctions in Type Theory},
+  year =          {1988},
+}
+
 @techreport{Gimenez94,
   author =        {Eduardo Giménez},
   institution =   {École Normale Supérieure de Lyon},
@@ -290,7 +297,7 @@
   title =         {A unifying theory of dependent types: the schematic
                    approach},
   year =          {1992},
-  url =           {http://www.cs.rhul.ac.uk/~zhaohui/TVER92.ps%7D,
+  url =           {http://www.cs.rhul.ac.uk/%5C~%7B%7Dzhaohui/TVER92.ps%7D,
 }
@inproceedings{Coquand86b,
@@ -381,7 +388,7 @@
   pages =         {266-278},
   title =         {A simplification of {G}irard's paradox},
   year =          {1995},
-  url =           {http://www.cs.cmu.edu/~kw/scans/hurkens95tlca.pdf%7D,
+  url =           {http://www.cs.cmu.edu/%5C~%7B%7Dkw/scans/hurkens95tlca.pdf%7D,
 }
@proceedings{FOSSACS08,
View it on GitLab: https://gitlab.com/monnier/typer/commit/64359fcfeb0448a4ba345294e53cb230b0f7...
-- 
View it on GitLab: https://gitlab.com/monnier/typer/commit/64359fcfeb0448a4ba345294e53cb230b0f7...
You're receiving this email because of your account on gitlab.com.



    