Stefan pushed to branch report/jfla-2019 at Stefan / Typer

Commits: 49863db0 by Stefan Monnier at 2018-11-08T02:50:12Z -

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -709,14 +709,14 @@ termination of elaboration anyway.

\section{Core language}

-\newcommand \TErase[1] {{#1*}} +\newcommand \Ferase[1] {{#1*}} \newcommand \TEarw[1][\ensuremath{k}] {\stackrel{\kw{#1}}{\to}} \newcommand \TEapp[2][\ensuremath{k}] {#2@^{\kw{#1}}}

-Typer's core language is based on ICC*~\cite{Barras08}. We start with -a $\lambda$-calculus that is a sort of pure type system (PTS)~\cite{Barendregt91b} -extended with annotations to indicate which arguments are -\Char{\kw{n}}ormal and which are \Char{\kw{e}}rasable: +Typer's core language is based on ICC*~\cite{Barras08,MishraLinger08}. +We start with a $\lambda$-calculus that is a sort of pure type system +(PTS)~\cite{Barendregt91b} extended with annotations to indicate which +arguments are \Char{\kw{n}}ormal and which are \Char{\kw{e}}rasable: \begin{displaymath} \begin{array}{lccl} \textsl{(level)} & \ell &\in& \mathbb{N} \ @@ -757,22 +757,22 @@ erasable functions: \begin{displaymath} \Infer{\Jtyper {\tau_1} s \ \Jtyper[\Gamma,x:\tau_1] e {\tau_2} \ - x \not\in \kw{fv}(\TErase e)} + x \not\in \kw{fv}(\Ferase e)} {\Jtyper{\lambda x : \tau_1 \TEarw[e] e}{(x : \tau_1) \TEarw[e] \tau_2}} \end{displaymath} The difference compared to the rule for \emph{normal} functions is the -addition of the test that $x$ doesn't appear in $\TErase e$ which is the -\emph{erasure} of $e$. The erasure function $\TErase{(\cdot)}$ erases type +addition of the test that $x$ doesn't appear in $\Ferase e$ which is the +\emph{erasure} of $e$. The erasure function $\Ferase{(\cdot)}$ erases type annotations as well as all erasable arguments: \begin{displaymath} \begin{array}{l@{;;=;;}l} - \TErase s & s \ - \TErase x & x \ - \TErase {((x:\tau_1)\TEarw\tau_2)} & (x:\TErase {\tau_1})\TEarw\TErase{\tau_2} \ - \TErase {(\lambda x:\tau\TEarw[n]e)} & \lambda x \to \TErase{e} \ - \TErase {(\lambda x:\tau\TEarw[e]e)} & \TErase{e} \ - \TErase {(\TEapp[n]{e_1}{e_2})} & {\TErase{e_1}}@\TErase{e_2} \ - \TErase {(\TEapp[e]{e_1}{e_2})} & \TErase{e_1} + \Ferase s & s \ + \Ferase x & x \ + \Ferase {((x:\tau_1)\TEarw\tau_2)} & (x:\Ferase {\tau_1})\TEarw\Ferase{\tau_2} \ + \Ferase {(\lambda x:\tau\TEarw[n]e)} & \lambda x \to \Ferase{e} \ + \Ferase {(\lambda x:\tau\TEarw[e]e)} & \Ferase{e} \ + \Ferase {(\TEapp[n]{e_1}{e_2})} & {\Ferase{e_1}}@\Ferase{e_2} \ + \Ferase {(\TEapp[e]{e_1}{e_2})} & \Ferase{e_1} \end{array} \end{displaymath} This expresses the fact that erasable arguments do not influence evaluation. @@ -798,14 +798,14 @@ a ``hardcoded'' combination of a sum of products: %% \begin{displaymath} \begin{array}{llcl} - &\TErase {(\kw{con}(e,l))} &=& \kw{con}(\TErase e,l) \ - &\TErase {(\kw{ind}~\overrightarrow{l \mapsto \overrightarrow{x:^k\tau}})} &=& - \kw{ind}~\overrightarrow{l \mapsto \overrightarrow{x:^k\TErase \tau}} \ - &\TErase {(\kw{fix}~\overrightarrow{x : \tau = e}~\kw{in}~e)} &=& - \kw{fix}~\overrightarrow{x = \TErase e}~\kw{in}~\TErase e \ - &\TErase {(\kw{case}~e~\kw{in}~\overrightarrow{l~y~\vec{x^k} \Rightarrow e_l})} &=& - \kw{case}~\TErase e~\kw{in}~\overrightarrow{l~\vec{x}' - \Rightarrow \TErase {e_l}} \hfill\hspace{20pt} + &\Ferase {(\kw{con}(e,l))} &=& \kw{con}(\Ferase e,l) \ + &\Ferase {(\kw{ind}~\overrightarrow{l \mapsto \overrightarrow{x:^k\tau}})} &=& + \kw{ind}~\overrightarrow{l \mapsto \overrightarrow{x:^k\Ferase \tau}} \ + &\Ferase {(\kw{fix}~\overrightarrow{x : \tau = e}~\kw{in}~e)} &=& + \kw{fix}~\overrightarrow{x = \Ferase e}~\kw{in}~\Ferase e \ + &\Ferase {(\kw{case}~e~\kw{in}~\overrightarrow{l~y~\vec{x^k} \Rightarrow e_l})} &=& + \kw{case}~\Ferase e~\kw{in}~\overrightarrow{l~\vec{x}' + \Rightarrow \Ferase {e_l}} \hfill\hspace{20pt} \text{where }\vec x' \text{ only includes the } x_i^{\kw{n}} \ \end{array} \end{displaymath} @@ -952,7 +952,7 @@ redundant in ICC*. More specifically: \begin{lemma}[Erasability of impredicative arguments] \label{lem:erasable} In ICC*, if $\Jtyper x {\tau_x : \kw{Type}~\ell}$ and $\Jtyper e {\tau_e : - \kw{Prop}}$, then $x$ can only appear in $\TErase e$ within arguments + \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 $\tau_1 : \kw{Type}~_$. \end{lemma}

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