Stefan pushed to branch report/itd at Stefan / Typer

Commits: b2853156 by Stefan Monnier at 2018-11-13T14:16:06Z -

- - - - -

2 changed files:

- GNUmakefile - paper.tex

Changes:

===================================== GNUmakefile ===================================== @@ -2,7 +2,8 @@ GLOBALREFS=~/share/misc/all LOCALREFS=refs.bib PAPER=paper

-${LOCALREFS}: ${PAPER}.aux ${GLOBALREFS}.bib +# Apparently other options are "bibextract/citetags/citefind" and "bibtool" +${LOCALREFS}: ${PAPER}.aux ${GLOBALREFS}.bib GNUmakefile @# The -r option breaks with names with slashes :-( ! @# bibexport -r ${GLOBALREFS} -o $@ ${PAPER}.aux @sed 's|^\bibdata{.*}|\bibdata{${GLOBALREFS}}|' <${PAPER}.aux >${PAPER}.tmp.aux

===================================== paper.tex ===================================== @@ -40,19 +40,22 @@ %% FIXME: I hate the way this bibliography looks because I find it %% ridiculously hard to find the entry corresponding to a reference %% like (Blume 2006) in the text. -\newcommand \citet \cite + %% \bibliographystyle{ACM-Reference-Format} %% Citation style %% Note: author/year citations are required for papers published as an %% issue of PACMPL. %% \citestyle{acmauthoryear} %% For author/year citations

+\newcommand \citet \cite + \usepackage[utf8]{inputenc} \usepackage{amsmath,amssymb,mathtools,stmaryrd} \usepackage{mathpartir} \usepackage{mdframed,empheq} \usepackage{parskip} \usepackage{fancybox} %For \ovalbox +\usepackage{natbib} \renewcommand \cite \citep

\DeclareUnicodeCharacter{03B1}{\ensuremath{\alpha}} \DeclareUnicodeCharacter{2203}{\ensuremath{\exists}} @@ -148,6 +151,9 @@

%% \input{commands}

+%% FIXME: I'd like to plug more union-themed elements, like say contracts, +%% negotiations, strikes, lockouts, empowerment, NLRB, ... or something. + \begin{abstract} Algebraic data types and inductive types like those of the Calculus of Inductive Constructions (CIC) are the bread and butter of statically typed @@ -221,8 +227,8 @@ single-constructor datatypes is not really problematic in terms of type definition or tuple construction, it becomes annoying when extracting data out of those tuples: every field access becomes a \kw{case} statement with a single branch that extracts each and every field of the tuple even if only -a single field is needed. So a simple field selection becomes an operation -of size proportional to the tuple's size. +a single of those fields is needed. So a simple field selection becomes an +operation of size proportional to the tuple's size.

We could easily solve this by providing additional ad-hoc support for tuples, but that goes against our ideal of a minimal core language since we @@ -250,7 +256,7 @@ The contributions of this article are: \begin{itemize} \item The CUC language, which provides separately sum types, recursive types, and tuple types, and where they can be combined without loss of - efficiency to provide the usual functionality traditionally provided by + efficiency to provide the functionality traditionally provided by algebraic data types or inductive types, making it better suited as a compiler intermediate language. \item A kind of case-analysis construct where the default branch also gets @@ -298,7 +304,7 @@ a single field from a large tuple, such as a tuple holding all the definitions exported from a module. For this reason, we want to introduce tuples separately from inductive types.

-To do that, we will deconstruct inductive types into their constituting +To do that, we will deconstruct inductive types into their constitutive elements: recursive types, sum types, tuple types, and indexed type families.

@@ -318,20 +324,23 @@ with a datatype like: \end{verbatim} an object like \texttt{cons(1, nil)} will generally have to be represented as two heap objects: one containing the \texttt{(1, nil)} tuple and another -containing \texttt{cons(<pointer>)}. A sufficiently smart compiler may -be able to eliminate this indirection, of course, but it can be -surprisingly complicated~\cite{Shao97,Leroy92,Leroy97}. +containing the \texttt{cons} tag and a pointer to the tuple. A sufficiently +smart compiler may be able to eliminate this indirection, of course, but it +can be surprisingly complicated and costly~\cite{Shao97,Leroy92,Leroy97}.

%% FIXME: Example/description is hard to follow! +%% These are basically sigma types! Another approach is to let the user manipulate tags explicitly, so we can have code like: \begin{verbatim} type T = { field0 : tag; field1 : f1 field0; - field2 : f2 field0} + field2 : f2 field0 } \end{verbatim} where the type of the fields depends on the tag stored in the first field, and after a case analysis on \texttt{e.field0} the type of the subsequent fields +%% FIXME: can we do dependent-elimination with this? +%% FIXME: the different types of fieldN have to belong to the same universe! becomes known. This approach can indeed be used to solve our problem but we rejected it for the following reason: by making tags first class, they become more expensive, for example because it is then difficult to combine @@ -413,6 +422,7 @@ it practical to provide this feature even if it is not used very often. \textsl{(ctxt)} & \Gamma,\Delta &::=& \EmptyCtx ~|~ \Gamma,x:\tau \ \textsl{(sort)} & s &::=& \Type \ell \ %% FIXME: Already give the full syntax here! + %% FIXME: Or maybe not, since this same base language is used for CIC! \textsl{(term)} & e,\tau &::=& s ~|~ x ~|~ \Tlam x \tau e ~|~ \Tapp{e_1}{e_2} ~|~ \Tarw x {\tau_1} {\tau_2} \end{array} @@ -468,15 +478,15 @@ it practical to provide this feature even if it is not used very often.

Just like the full CIC, our new calculus is fairly large, so we present it in several steps: the base calculus, the tuples, the equality type, the -sums, and finally the recursive definitions. Those parts are not completely -independent from each other, which largely dictates the order in which they -are presented, but to a large extent the base calculus can be replaced with -any other lambda calculus. - -Figure~\ref{fig:ccw} shows our base language \CCw{} as a pure type system -(PTS)~\cite{Barendregt91b}. It is a variant of CoC with a tower of universes -à la ECC~\cite{Luo89}. - +sums, and finally the recursive definitions. Figure~\ref{fig:ccw} shows our +%% FIXME: After adding the rest of the syntax, we'll need to update this. +base language \CCw{} as a pure type system (PTS)~\cite{Barendregt91b}. +It is a variant of CoC with a tower of universes à la ECC~\cite{Luo89}. + +The different parts are not completely independent from each other, which +largely dictates the order in which they are presented, but to a first +approximation the base calculus can be replaced with any other +lambda calculus. %% FIXME: The issue is much more serious, since impredicativity almost %% ends up introducing restrictions which prevent defining π₁ and/or π₂ %% on impredicative sums, so it's far from clear how to turn a `case` into @@ -494,7 +504,7 @@ of extensions. The typing judgment of the base language is usually denoted $\Jtyper e \tau$, and we will annotate it as $\Jcuc e \tau$ or $\Jcic e \tau$ when we talk about the typing derivation of CUC resp.~CIC. Similarly, while the base language's reduction rule is usually written $e\leadsto e'$, we will write it -as $e\stackrel{U}{\leadsto} e'$ or $e\stackrel{U}{\leadsto} e'$ when we talk about the +as $e\stackrel{U}{\leadsto} e'$ or $e\stackrel{I}{\leadsto} e'$ when we talk about the reduction rule for CUC resp.~CIC.

\Comment{ @@ -1734,7 +1744,7 @@ judgments into the logic: author and do not necessarily reflect the views of the NSERC. \end{acks}

-\bibliographystyle{alpha} +\bibliographystyle{plainnat} %% \bibliography{typer_theory} \bibliography{refs} \end{document}

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