Nathaniel pushed to branch bosn at Stefan / Typer
Commits: 7d665323 by nbos at 2018-07-24T08:18:21Z Contextualized notation for Typer's compound terms and CCw
- - - - -
1 changed file:
- doc/formal/typer_theory.tex
Changes:
===================================== doc/formal/typer_theory.tex ===================================== @@ -77,7 +77,9 @@ Because of the impredicativity of the erasable part of Typer, we need to define \end{figure}
\subsection{ICC in Typer} -Typer provides distinction between three kinds of terms to simplify both the writing and execution of programs. \emph{Explicit} terms are the usual expression that are written by the user and then executed. \emph{Implicit} terms are also used during execution, but Typer is able to infer them during elaboration such that they do not need to be written by the user. \emph{Erasable} terms are neither written by the user nor executed; they are inferred during elaboration, participate in type checking and are then erased before execution. The notation we adopt for compound terms are the following: +Typer manipulates three separate kinds of terms to simplify both the writing and execution of programs. \emph{Explicit} terms are the usual expression that are written by the user and then executed. \emph{Implicit} terms are also used during execution, but Typer is able to infer them during elaboration such that they do not need to be written by the user. \emph{Erasable} terms are neither written by the user nor executed; they are inferred during elaboration, participate in type checking and are then erased before execution. + +The notation we adopt in this document is meant to both allow for the distinction between the three kinds of terms and to evoke actual Typer source code. Thus, the traditional explicit lambda term $\la(x:A).b$ will here be written $\la(x:A)\explicit b$ and similarly the product type $\Pi(x:A).B$ will be written $(x:A)\explicit B$. The type of arrow used will convey the kind of term being defined. Thus, compound terms of our calculus will all take one of the following forms:
\begin{center} \begin{tabular}[h]{rclll} @@ -368,7 +370,7 @@ In this section we will prove that the erasable terms of Typer allow for a repre
Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, but with an added infinite hierarchy of universes above the impredicative $\mathsf{Prop}$. They are arranged in the series: $$\Prop : \Type_1 : \Type_2 : \Type_3 : \Type_4...$$
-\CC's PTS definition is shown in Figure X. The typing rules for \CC\ are shown in Figure X. The structure of the PTS is derived from Luo's own extention of CC (ECC) \cite{luo}, but the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\Prop,\Type_i,\Type_i)$ and $(\Type_i, \Type_j, (\Type_i\cup\Type_j))$. This is because we do not have access to ECC's cumulativity and \emph{lift} operator, which would usually permit us to derive the sort of a type constructed from the abstraction of a variable in one universe over a term in another universe (i.e. dependent types and polymorphic functions). +\CC's PTS definition is shown in Figure X. The typing rules for \CC\ are shown in Figure X. The structure of the PTS is derived from Luo's own extention of CC (ECC) \cite{luo}, but the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\Prop,\Type_i,\Type_i)$ and $(\Type_i, \Type_j, (\Type_i\cup\Type_j))$. This is because we do not have access to ECC's cumulativity and \emph{lift} operator, which would usually permit us to derive the sort of a type constructed from the abstraction of a variable in one universe over a term in another universe (i.e. dependent types and polymorphic functions). Our definition of \CC\ will therefore behave differently than, for example, Miquel's definition of \CC\ \cite{miquel}. \subsection{Translation} By induction on typing derivation steps. \textsc{CC-Wf-E} and \textsc{CC-Var} both directly translate to \textsc{Wf-E} and \textsc{Var} respectively since they introduce nothing new. Because \textsc{CC-Sort} and \textsc{CC-Wf-S} call upon $\A_{CC}$ and $\S_{CC}$, we make a mapping between the universe hierarchies $\S_{CC} \to \S$:
View it on GitLab: https://gitlab.com/monnier/typer/commit/7d6653236691d857e2c2c6e7e445db744045...
Afficher les réponses par date