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... -- View it on GitLab: https://gitlab.com/monnier/typer/commit/49863db00820bc83dded791ecc8e3082af34... You're receiving this email because of your account on gitlab.com.