Stefan pushed to branch report/itd at Stefan / Typer
Commits: f1dee9f9 by Stefan Monnier at 2018-10-09T19:59:58Z -
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -53,6 +53,8 @@ \usepackage{parskip} \usepackage{fancybox} %For \ovalbox
+\DeclareUnicodeCharacter{2203}{\ensuremath{\exists}} + %% The doc says `vcenter` should work, but I get an error :-( %% \newcommand \Infer[1][] [\inferrule*[vcenter,right=#1]] \newcommand \Infer[1][] {\inferrule*[right=#1]} @@ -153,7 +155,7 @@ %% ... \end{CCSXML}
-%%\keywords{keyword1, keyword2, keyword3} %% \keywords are mandatory in final +\keywords{Inductive types, compilation, union types}
%% Note: \begin{abstract}...\end{abstract} environment must come %% before \maketitle command @@ -165,126 +167,184 @@
\section{Introduction}
-Typer is a language in the tradition of Coq, Lean, and Agda, but focusing on -programs more than proofs, like Idris, F-star~\cite{Swamy16}, and ATS. +Typer is a functional language based on a pure type system, in the tradition +of Coq~\cite{Coq00}, Lean, and Agda~\cite{Bove09}, but focusing on programs +more than proofs, like Idris~\cite{Brady13}, F-star~\cite{Swamy16}, +Zombie~\cite{Casinghino14}, and many others before. Its design follows that +of Scheme, in the sense that it intends to provide a minimalist core +language on top of which a nice language can be built by metaprogramming.
-Typer needs a good target language: +So the focus of Typer's design is on providing a good core language which is +the target of the metaprogramming facilities. Some of the design goal of +this language are: \begin{itemize} -\item Clean, simple, elegant -\item Economy of concepts -\item High-level enough to be convenient to build on top of it -\item Low-level so more optimizations can be implemented via Typer's - metaprogramming rather than hardcoded in the compiler -\item Efficient implementation shouldn't require excessive efforts +\item We want this core language to be usable both to write proofs and to + write programs. +\item We want an economy of concepts, in other words a simple and + clean language. This is desirable not only for aesthetic reasons, but + also for pragmatic reasons such as making the soundness proof + hopefully simpler. +\item High-level enough to be convenient to build on top of it. +\item Yet we also want it to be low-level so the language itself does not + impose unneeded inefficiencies which the compiler then needs to eliminate. +\item A reasonably efficient implementation shouldn't require excessive efforts. \end{itemize} - -Inductive type options: -\begin{itemize} -\item Impredicative encoding: algorithmically inefficient, inability to - eliminate to different universe levels, inability to perform dependent - elimination (aka ``induction''). -\item Cedille's encoding: still problems with universe levels, - a straightforward implementation is algorithmically efficient but - recovering ML-style efficiency seems to require non-trivial - optimization efforts. -\item SML-style sum types: cleanly separates sums and products, but - dependent elimination is clumsy to specify, %% FIXME: Really? - and the representation tends to impose an additional indirection. -\item Either type: Dependent elimination is simpler to specify, - %% FIXME: `Either` looks very much like SML-style, so the above simplicity - %% may not be apparent, but indeed dependent - %% elimination is simpler in the sense that the "default" branch is known - %% to be "the other" branch, so there's really no default branch! - but it imposes an indirection like the SML-style, and the overhead grows - with the number of alternatives. -\item Haskell-style data types and Coq inductive types: tuples need to be - represented as degenerate sum types and eliminated with `case`, so record - selection like $x.l$ really expands to an expression of size proportional - to the number of fields of the record. Field extraction can't be - separated from case analysis. Dependent elimination is clumsy to specify - (especially for the default case). -\item Sigma type $\Sigma \id{tag}: \kw{bool} . \Tif {\id{tag}} {\tau_1} {\tau_2}$. - Elegant because it provides both pairs and sums at the same time. - Builds on booleans (or other datatypes) for the tags, so there's - a bootstrap (or duplication) problem; not sure how it can handle dependent - elimination either. -\end{itemize} - -Contributions: +The Calculus of Constructions satisfies the first two points above, but +falls short on the efficiency side when it comes to representing data +structures. The Calculus of Inductive Constructions (CIC)~\cite{Paulin93} +solves most of those issues, especially in the form presented +by~\citet{Gimenez94}. It is nicely minimalist, its inductive definitions +providing at once sums types, tuples types, recursive types, etc... For +these reasons Typer's core language derives directly from the CIC. + +Yet, early experience with it made us feel that it was still a bit too +high-level, introducing inefficiencies in some places. The main problem +appears in code that wants to manipulate tuples: while defining tuples as +single-constructor datatypes is not really problematic in terms of type +definition or tuple construction, it becomes annoying when the time comes to +get data out 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. + +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 +would then have two different ways to define tuples. What we want instead +is to define inductive types on top of tuple types rather than other +way around. + +In the rest of this paper, we hence present the design of the Calculus of +United Constructions (CUC) where sums, recursive types, and tuples are +provided as separate elements, which together can be used to define our +beloved inductive types but can also be used separately. The main new +primitive is the introduction of a \kw{switch} construct, which only looks +at an object's tag to transfer control to the appropriate branch but doesn't +extract any further data, reflecting instead into the type context the +knowledge about which tag was found. An important feature of this +\kw{switch} construct is that it fully supports default branches, also +reflecting into the type context the fact that some branches were considered +but not taken. + +Of course, we still want our CUC language to enjoy the same meta-theoretic +properties as the CIC, which we verify in Section~\ref{sec:equivalence} by +showing that the two language are equivalent. + +The contributions of this article are: \begin{itemize} -\item A lower-level presentation of the Calculus of Inductive Constructions - (CIC) better suited as intermediate language. -\item A \kw{case} expression where the default branch also gets refined type - information witnessing in an efficient way precise information about the - branches already tested. +\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 functionally 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 + refined type information witnessing in an efficient way precise + information about the branches already tested. +\item A proof of equivalence of this language with the Calculus of Inductive + Constructions, showing it enjoys the same meta-theoretic properties. \end{itemize}
-%% \begin{figure}[h] -%% \ \ \ \ \fbox{ -%% \begin{mathpar} -%% \ -%% \infer -%% {\ } -%% {\emptyctx ~} -%% \textsc{ (Wf-E)} -%% \and %-------------------- -%% \infer -%% {\Ga ~ T:s \ s \in \S \ x \notin \dv{\Ga}} -%% {\Ga , x:T ~} -%% \textsc{ (Wf-S)} -%% \and %-------------------- -%% \infer -%% {\Ga ~ \ (s_1:s_2) \in \A} -%% {\Ga ~ s_1:s_2} -%% \textsc{ (Sort)} -%% \and %-------------------- -%% \infer -%% {\Ga ~ \ (x:T) \in \Ga} -%% {\Ga ~ x:T} -%% \textsc{ (Var)} -%% \and %-------------------- -%% \\ -%% \infer -%% {\Ga ~ T:s_1 \ \Ga, x:T ~ U:s_2 \ (s_1,s_2,s_3) \in \R} -%% {\Ga ~ (x:T) \explicit U : s_3} -%% \textsc{ (X-Prod)} -%% \and %-------------------- -%% \infer -%% {\Ga, x:T ~ M:U \ \Ga ~ (x:T) \explicit U : s} -%% {\Ga ~ \la(x:T) \explicit M : (x:T) \explicit U} -%% \textsc{ (X-Lam)} -%% \and %-------------------- -%% \infer -%% {\Ga ~ M : (x:T) \explicit U \ \Ga ~ N:T} -%% {\Ga ~ M|N : U{N/x}} -%% \textsc{ (X-App)} -%% \\ -%% \infer -%% {\Ga ~ T:s_1 \ \Ga, x:T ~ U:s_2 \ (s_1,s_2,s_3) \in \R_e} -%% {\Ga ~ (x:T) \erasable U : s_3} -%% \textsc{ (E-Prod)} -%% \and %-------------------- -%% \infer -%% {\Ga, x:T ~ M:U \ \Ga ~ (x:T) \erasable U : s \ x \notin \fv{M^*}} -%% {\Ga ~ \la(x:T) \erasable M : (x:T) \erasable U} -%% \textsc{ (E-Lam)} -%% \and %-------------------- -%% \infer -%% {\Ga ~ M : (x:T) \erasable U \ \Ga ~ N:T} -%% {\Ga ~ M|||N : U{N/x}} -%% \textsc{ (E-App)} -%% \ -%% \end{mathpar} -%% } -%% \caption{Typer's Typing Rules from ICC} -%% \label{fig:Typing-rules} -%% \end{figure} - -%% There are two notable differences between explicit and erasable typing rules: -%% \begin{enumerate} -%% \item In the erasable product rule \textsc{E-Prod}, the set of rules is the impredicative $\R_e$ instead of $\R$ -%% \item In the erasable abstraction rule \textsc{E-Lam}, erasable abstraction are conditional on the bound variable not being free in the expression after erasure ($x \notin \fv{M^*}$). This ensures that the variable is only used in ``erasable'' ways inside the expression such that we are not left with new free terms after erasure. -%% \end{enumerate} +\section{Background} + +In this section, we briefly present the two problems our design aims to address. + +\subsection{Native tuples} + +Proving algebraic data types and tuples without overlap is not a new +problem, and Standard ML~\cite{Milner97} solved it years ago by restricting +its datatype constructors to carry exactly one element, no more no less. +In other words, SML's datatype only provides sum types and recursive types, +and tuples are provided separately. While it is elegant, this solution +suffers from an inefficiency we wanted to avoid. For example, with +a datatype like: +\begin{verbatim} + datatype 'a list = + | cons of 'a * 'a list + | nil +\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}. + +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} +\end{verbatim} +So 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 +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 +them into the object header that is required for the needs of the memory +management, for example. Basically, the language becomes too low-level, too +close to machine language, tying the hands of the compiler too tightly for +our needs. + +%% Inductive type options: +%% \begin{itemize} +%% \item Impredicative encoding: algorithmically inefficient, inability to +%% eliminate to different universe levels, inability to perform dependent +%% elimination (aka ``induction''). +%% \item Cedille's encoding: still problems with universe levels, +%% a straightforward implementation is algorithmically efficient but +%% recovering ML-style efficiency seems to require non-trivial +%% optimization efforts. +%% \item SML-style sum types: cleanly separates sums and products, but +%% dependent elimination is clumsy to specify, %% FIXME: Really? +%% and the representation tends to impose an additional indirection. +%% \item Either type: Dependent elimination is simpler to specify, +%% %% FIXME: `Either` looks very much like SML-style, so the above simplicity +%% %% may not be apparent, but indeed dependent +%% %% elimination is simpler in the sense that the "default" branch is known +%% %% to be "the other" branch, so there's really no default branch! +%% but it imposes an indirection like the SML-style, and the overhead grows +%% with the number of alternatives. +%% \item Haskell-style data types and Coq inductive types: tuples need to be +%% represented as degenerate sum types and eliminated with `case`, so record +%% selection like $x.l$ really expands to an expression of size proportional +%% to the number of fields of the record. Field extraction can't be +%% separated from case analysis. Dependent elimination is clumsy to specify +%% (especially for the default case). +%% \item Sigma type $\Sigma \id{tag}: \kw{bool} . \Tif {\id{tag}} {\tau_1} {\tau_2}$. +%% Elegant because it provides both pairs and sums at the same time. +%% Builds on booleans (or other datatypes) for the tags, so there's +%% a bootstrap (or duplication) problem; not sure how it can handle dependent +%% elimination either. +%% \end{itemize} + +\subsection{Typing the default branch} + +When performing case analysis in Coq and other languages of the family, the +default branch does not get any typing refinement. More specifically, let's +consider the following example where \texttt{e} is assumed to be a list: +\begin{verbatim} + match e with + | nil => exp1 + | _ => exp2 +\end{verbatim} +The typing of \texttt{exp1} can take advantage of the fact the we know +\texttt{e} was found to be equal to \texttt{nil}, but the typing of +\texttt{exp2} has no such benefit: it cannot take advantage of the fact that +we have found \texttt{e} to be different from \texttt{nil}. + +It would not be difficult to change Coq such that default branches get +additional typing information, either providing them with a proof that the +match target is different from all the mentioned branches (i.e.~a proof that +``\texttt{not (e = nil)}'' in the above example), or providing them with +a proof that the match target is equal to one of the remaining possibilities +(i.e.~a proof that ``\texttt{∃x,y. e = cons x y}'' in the above +example). The problem here is that those additional proofs would tend to +grow fairly large, imposing a cost that is difficult to justify since +experience shows that such a refined information is not often useful. + +This last point argues that this is not an important problem to solve, and +we partly agree: it was not the primary motivation for our design. Still: our +design provides us with that kind of refinement at a much lower cost, making +it practical to provide this feature even if it is not used very often.
\section{Base calculus}
@@ -680,6 +740,7 @@ In this section, we show that it is indeed the case, by defining an erasure function and showing that the evaluation and the erasure commute.
\section{Equivalence} +\label{sec:equivalence}
Now that we have defined a calculus which provides us with the intended run time cost, we show that this calculus shares all the other desirable @@ -995,6 +1056,8 @@ $\Ftocic \bot = \bot$. \Ftocuc {\Tarw{x}{\tau_1}{\tau_2}} & \Tarw{x}{\Ftocuc {\tau_1}}{\Ftocuc {\tau_2}} \ \Ftocuc {\TUnion{\tau_1}{\tau_2}} & \TIeither{\Ftocuc {\tau_1}}{\Ftocuc {\tau_2}} \ \Ftocuc {\Jsubtype{\tau_1}{\tau_2}} & \Tsarw{\Ftocuc {\tau_1}}{\Ftocuc {\tau_2}} \ + \Ftocuc {\id{Sub.refl}{e}} & \Tapp{\Ftocuc {P}}{\Ftocuc {e}} \ + \Ftocuc {\TUweaken{P}{e}} & \Tapp{\Ftocuc {P}}{\Ftocuc {e}} \ \end{array} \end{displaymath} Inductive types get turned into tuples, tags, explicit equality proofs, @@ -1025,7 +1088,10 @@ judgments into the logic:
\section{Related works}
-\nocite{Gimenez94,Blume06,Castagna16,Levitation} +\nocite{Gimenez94} +\nocite{Blume06,Castagna16} %Union types and extensible sums +\nocite{Chapman10} %Levitation +\nocite{Christiansen16} %Idris's use in elaboration
\section{Conclusion}
View it on GitLab: https://gitlab.com/monnier/typer/commit/f1dee9f9a4f0fa35eb3c9e5decf5fec04a4f...
Afficher les réponses par date