Stefan pushed to branch report/els-2017 at Stefan / Typer
Commits: 5b9a1670 by Stefan Monnier at 2017-02-05T17:45:08-05:00 Try and clarify OPG as well as grammar-vs-macros
- - - - -
2 changed files:
- paper.tex - refs.bib
Changes:
===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -1,4 +1,4 @@ -\documentclass[sigplan, review, 10pt]{acmart} +\documentclass[sigplan, review]{acmart}
\usepackage[utf8]{inputenc}
@@ -42,6 +42,7 @@ \newcommand \OR {~|~} \renewcommand - {!-!} \renewcommand : {!:!} +\newcommand \Char [1] {`\texttt{#1}'}
%% Rule names \newcommand \RR [1] {r_{\textsl{#1}}} @@ -167,7 +168,7 @@ of syntactic categories and generally make ``everything'' first-class. </ccs2012> \end{CCSXML}
-\ccsdesc[500]{Software and its engineering~\Functional languages} +\ccsdesc[500]{Software and its engineering~Functional languages} \ccsdesc[500]{Software and its engineering~Extensible languages} \ccsdesc[300]{Software and its engineering~Control structures} \ccsdesc[300]{Software and its engineering~Syntax} @@ -184,7 +185,7 @@ of syntactic categories and generally make ``everything'' first-class. Almost all programming languages support one form or another of meta-programming via macros that get expanded during compilation. And for those rare exceptions which resist the temptation, their users often resort -to generic macro processors such as CPP and M4~\cite{M4}. There is +to generic macro processors such as CPP~\cite{CPP} and M4~\cite{M4}. There is hence no doubt that macros are an important functionality of a language.
The Lisp family of languages reigns as the undisputed king at the top of the @@ -198,17 +199,17 @@ Lisp's macros, but adapting it to the context of a statically typed functional language in the tradition of ML~\cite{Milner84}. More specifically, while designing Typer, we had the following goals: \begin{itemize} -\item The language should be functional, statically typed, with - a syntax similar to that of ML or Haskell. +\item The language should be functional, statically typed, and with + a syntax reminiscent of that of ML or Haskell. \item There should be a minimal core language, such that extra features can be added on top via libraries. \item Good support to define embedded DSLs. \end{itemize} - +%% The first goal means we want to support infix notation and that we need to support type expressions in the language. The second goal means for example that we should be able to define constructs such as -$\kw{if}~e_1~\kw{then}~e_2~\kw{else}~e_3$ in a library, or that compilation +``$\kw{if}~e_1~\kw{then}~e_2~\kw{else}~e_3$'' in a library, or that compilation of pattern matching is implemented in a library rather than by the compiler. This in turns requires the ability to extend the syntax of the language, including adding new infix or mixfix~\cite{Danielsson08} constructs and @@ -220,7 +221,7 @@ The result is a language with a syntactic structure fundamentally similar to that of Lisp, yet superficially much less regular, thanks to the use of mixfix elements. The parser is still very primitive, since it uses an operator precedence grammar~\cite{Floyd63}, but is already powerful enough -to handle a syntax that will feel familiar to ML and Haskell users. +to handle a syntax that should feel familiar to ML and Haskell users.
Typer's core language is based on a Pure Type System~\cite{Barendregt91b}, so as to use a single syntactic category for types and expressions. @@ -247,6 +248,7 @@ The power of Lisp's macros relies on the following: \item Macro calls look just like normal function calls. \item A macro's expansion can be defined as the result of an arbitrary computation, itself defined in Lisp. +\item Macro arguments are unaffected by syntactic categories. \end{itemize}
\subsection{S-expressions} @@ -319,8 +321,8 @@ syntactic category. For example, Common Lisp \cite{Steele90} provides separate macros for the syntactic category of symbols (\kw{symbol-macrolet}) and lvalues (\kw{defsetf}), and Emacs Lisp similarly uses separate macros to define new patterns -(\kw{pcase-defmacro}) and new context specializers on \kw{defmethod} -(\kw{cl-generic-define-context-rewriter}). +(\kw{pcase-defmacro}). %% and new context specializers on \kw{defmethod} +%% (\kw{cl-generic-define-context-rewriter})
Languages like Dylan do not try to unify all syntactic categories and instead provide separate macros for use in contexts such as definitions or @@ -336,9 +338,9 @@ more generally useful. \subsection{No special syntax for macro calls}
The basic syntax of Lisp macros is indistinguishable from the basic -syntax of primitive syntactic forms. This means that the user does not +syntax of primitive syntactic forms. This means that the user does not need to know if \kw{cond} is implemented as a primitive or as a macro -that expands to a bunch of \kw{if} expressions, or vice versa. This is +that expands to a bunch of \kw{if} expressions, or vice versa. This is a very important property in order to make the language truly extensible.
@@ -363,9 +365,33 @@ arbitrary code, sending my deepest secrets to my arch enemy. It also means that compiling a program may fail to terminate. We believe the benefits largely outweigh those costs.
+\subsection{Macro arguments and syntactic categories} + +Anyone who forgot the proverbial parenthesis in a C macro has experienced +the interaction between macros and syntactic categories. When parsing +a macro call, a language has to choose how to parse the arguments, such as: +\begin{itemize} +\item Keep them as a stream of tokens (CPP) or even characters (M4). + This option's lack of structure makes it generally undesirable. +\item Parse them as ``the main syntactic category'', typically + as expressions. This restricts the set of possible macro arguments, + making some macros inconvenient to use. +\item Lookup the macro's definition to find which category to use for each + argument. This requires that the parser has access to the compiler's + symbol table. E.g. it typically implies that macros cannot be used in the + file where they're defined, and makes it virtually impossible to + support lexically scoped macros, like Common Lisp's \id{macrolet}. +\end{itemize} +%% +Lisp's use of S-expressions means that at that stage of parsing, there is +really only one syntactic category, so it can take the second option without +it imposing any restriction on its macros's arguments. + \section{A Typer primer} \label{sec:primer}
+Before getting to Typer's macro system, we'll give a short overview of what +the language looks like. To a first approximation Typer is very similar to other languages in the ML family. It is a statically typed (pure) functional language, with basically two core elements: functions and datatypes. To define a function which adds @@ -485,16 +511,11 @@ backquote and comma in Common Lisp macros. Being purely functional, Typer resorts to the usual monadic technique to get access to a side effecting world, just as is done in Haskell. In the above code, \id{ME} is the macro-expansion monad, used for the same purpose as the -one used in Template Haskell and \id{return} is the unit of that monad. +one used in Template Haskell, and \id{return} is the unit of that monad.
\section{Parsing into S-expressions} \label{sec:parsing}
-\TODO{ - Clarify how/when the grammar is defined, e.g. the fact that macros do not - modify the grammar. -} - \newcommand \FigTyperSexp { \begin{figure} \begin{displaymath} @@ -515,6 +536,7 @@ one used in Template Haskell and \id{return} is the unit of that monad. Like Lisp, Typer's parsing is done in 3 steps: the first turns the input into a stream of tokens; the second turns this stream into an S-expression tree; and the third finally recognizes the actual language's constructs. + Fig.~\ref{fig:Typer-Sexp} shows how Typer's S-expressions are represented internally. This is very similar to Lisp's representation except that the \id{cons} constructor is replaced by a \id{node} constructor which @@ -523,12 +545,16 @@ basically enforces that sub-lists are \emph{proper} lists. We will first look at the actual syntax analysis step, and we will return to tokenizing later.
-\subsection{Operator precedence grammar} +In order to support user-defined infix and mixfix notations, the +S-expressions parser in Typer (i.e.~the \emph{reader}) is parameterized by +a grammar. An important detail to remember: just like with Lisp's +S-expressions, this parsing is independent from the macros. The reader does +not know what is a macro call and what isn't; and similarly defining a new +infix operator has nothing to do with defining a new macro: the first +modifies the grammar (and can't affect the nearby code that's already been +parsed into an S-expression), while the second modifies the symbol table.
-\TODO{ - better explain the stuff about inserting parentheses; explain - the notation ``kw1 e kw2''; Give an example right away -} +\subsection{Operator precedence grammar}
Typer's external notion of S-expression is more flexible than Lisp's, since it allows infix notation. It relies on operator precedence grammars @@ -537,9 +563,27 @@ context free grammars, much more restrictive than LALR, for example.
You can think of the job of an OPG parser as trying to add parentheses to recover the document's structure: whenever the parser sees something of the -form ``$\id{kw}_1~e~\id{kw}_2$'', it just needs to decide whether that -should be ``$\id{kw}_1~(e~\id{kw}_2$'' or ``$\id{kw}_1~e)~\id{kw}_2$''. -What sets OPG apart here is that it makes this choice without considering +form ``$\id{kw}_1~e~\id{kw}_2$'' (where $\id{kw}_1$ and $\id{kw}_3$ are +keywords and $e$ is a sequence of non-keyword tokens or fully +parenthesized sub-trees), it just needs to decide whether that should be +parenthesized as ``$\id{kw}_1~(e~\id{kw}_2$'' or +``$\id{kw}_1~e)~\id{kw}_2$''. For example, when starting with: +\begin{verbatim} + ... g + f(5) * 6 - x ... +\end{verbatim} +The parser will look at ``\texttt{+ f(5) *}'' and add the open paren: +\begin{verbatim} + ... g + (f(5) * 6 - x ... +\end{verbatim} +then it will see ``\texttt{* 6 -}'' and add the close paren: +\begin{verbatim} + ... g + (f(5) * 6) - x ... +\end{verbatim} +Then it will consider ``\texttt{+ (f(5) * 6) -}'' and add the open paren: +\begin{verbatim} + ... g + ((f(5) * 6) - x ... +\end{verbatim} +What sets OPG apart here is that it makes these choices without considering $e$ nor the surrounding context: instead, it bases its decision only on the pair of keywords.
@@ -563,10 +607,11 @@ choice of an OPG parser was not efficiency but rather the following aspects: stream of tokens will be parsed in the same way regardless of the surrounding context. \end{itemize} +%% The second point is what makes them particularly suitable for S-expressions, since at the time of parsing, we do not know yet what role a given S-expression will play: we do not yet know if it is a type, a pattern, an -expression, or anything else for that matter since it depends on the +expression, an lvalue, or anything else for that matter since it depends on the definition of the macros in which it appears.
For example, in OCaml the following piece of code: @@ -586,7 +631,7 @@ the parser would need to know that this is a macro call and would need to decide if the macro's argument should be parsed as a declaration or as an expression. We did not want to make the parser depend so tightly on the semantics of the language: by restricting ourselves to an OPG grammar, we do -not need to know what is a macro call let alone figure out what is that +not need to know what is a macro call, let alone figure out what is that macro's definition.
\subsection{Typer's OPG} @@ -602,7 +647,7 @@ the user can write _=_ x (_+_ (_*_ a b) c) \end{verbatim} and these two notations result in identical S-expressions, just like in -Lisp, expressions like \texttt{(a . (b))} and \texttt{(a b)} cannot be +Lisp expressions like \texttt{(a . (b))} and \texttt{(a b)} cannot be distinguished.
While restrictive, OPG grammars can express a wide variety of constructs, @@ -613,6 +658,7 @@ thanks to two more rules: \item A keyword can have a ``nil'' precedence on the left or on the right, meaning that it is a prefix or (respectively) postfix operator. \end{itemize} +%% So, if the tokens ``['' and ``]'' are given precedences respectively $(\id{nil}, 0)$ and $(0, \id{nil})$, they will be treated as the usual balanced pair, so that the following holds: @@ -638,9 +684,10 @@ Finally, Typer adds the following ad-hoc rules: we call it \emph{associative} and sequences of it get collapsed. We use this for example for the ``;'' operator. \end{itemize} +%% So instead of \begin{displaymath} - \begin{array}{r@{\hspace{10pt}\equiv\hspace{10pt}}l} + \begin{array}{r@{\hspace{10pt}\not\equiv\hspace{10pt}}l} \texttt{((a) + b)} & \texttt{(_) (_+_ ((_) a) b)} \ \texttt{d1; d2; d3} & @@ -654,21 +701,24 @@ we have \texttt{d1; d2; d3} & \texttt{_;_ d1 d2 d3} \end{array} \end{displaymath} -To give a more concrete example, the definition of \kw{List} shown earlier +To give a more concrete example, the definition +\begin{verbatim} + type List (a : Type) + | nil + | cons a (List a) +\end{verbatim} is parsed into the following S-expression: \begin{verbatim} type_ (_|_ (List (_:_ a Type)) nil (cons a (List a))) \end{verbatim} -Because \id{type} is defined as a prefix operator, and $\mid$ is defined as -an associative infix operator. +Because ``\kw{type}'' is defined as a prefix operator, and ``$\mid$'' is +defined as an associative infix operator.
\subsection{Two-level tokenizing}
-\newcommand \Char [1] {`\texttt{#1}'} - Following the Lisp tradition, Typer's lexical rules allow identifiers to be composed of almost any character. The exceptions are: \begin{itemize} @@ -685,25 +735,28 @@ as 3 separate tokens. If the user wants to write the single ``\texttt{_;_}'' token, she needs to escape the semi-colon with a backslash: ``\verb+_;_+''.
-But these lexical rules pose a problem in our quest to have an ML-style -syntax with a minimalist core: we want to be able to define a module system -outside of the core language, and we also want to be able to use a syntax -such as \texttt{String.concat} to refer to the \id{concat} function of the -\id{String} module. Yet, we can't simply define \Char{.} to be -a \emph{single-char token} character and then define it as an infix -operator, because that would give us +With these rules and an appropriate precedence table, we were able to define +a satisfactory syntax for Typer. We just found one remaining wrinkle in our +quest to have an ML-style syntax with a minimalist core: we want to be able +to define a module system outside of the core language, and we also want to +be able to use a syntax such as \texttt{String.concat} to refer to the +\id{concat} function of the \id{String} module. Yet, we can't simply define +\Char{.} to be a \emph{single-char token} character and then define it as an +infix operator, because that would give us \begin{displaymath} \begin{array}{r@{\hspace{10pt}\equiv\hspace{10pt}}l} \verb+String.concat a b+ & \verb+_._ String (concat a b)+ \end{array} \end{displaymath} -We could try to extend out OPG parser so as to allow infix operators to bind +We could try to extend our OPG parser so as to allow infix operators to bind more tightly than the ``space'', but instead we decided to do a two-level tokenization: after splitting tokens according to the above rules, each token is \emph{parsed} using a grammar, even more limited than the OPG grammar presented earlier, where \Char{.} can be given the status of infix operator. We can again override this special handling of a given character -by escaping it. So, the following equalities hold: +by escaping it. Just like with the normal infix operators, these +\emph{inner infix} operators also have a non-infix syntax, but using double +underscores instead of single underscores. E.g., the following equalities hold: \begin{displaymath} \begin{array}{r@{\hspace{10pt}\equiv\hspace{10pt}}l} \texttt{String.concat} & \verb+__.__ String concat+ \ @@ -794,7 +847,7 @@ recursive functions: type (an \id{Lexp}), and returns the elaborated form, of type \id{Lexp}. \end{itemize} The type environment carries the type of every variable in scope, of course, -but it also carries the definition of all the variable in scope which were +but it also carries the definition of all the variables in scope which were defined via a \id{let} binding.
The complete presentation of the type checker is out of scope of this @@ -827,14 +880,17 @@ a \id{node}, they do the following: \kw{let} and \kw{case}. \item If the returned type is \id{Macro}, then it is a macro call, and we expand it, as detailed below. -\item Otherwise, it should be a function call so we do as outlined above. +\item Otherwise, it should be a function call so we do as outlined in the + previous subsection. \end{enumerate} - +%% Note that at step 2 above, we have to double check that the head is -a \id{prim}, because in case of a source code such as -``\verb|(if x then let_in_ else case_) 42|'' the head is a valid -expression of type \id{Special-Form} but is not a primitive, so we have to -reject such meaningless code. +a \id{prim}, because the source code could be +\begin{verbatim} + (if x then let_in_ else case_) 42 +\end{verbatim} +in which case the head is a valid expression of type \id{Special-Form} but +is not a primitive, so we have to reject such meaningless code.
So the way keywords like \id{let_in_} get their special meaning is simply by binding them to the corresponding special form primitive in the initial
===================================== refs.bib ===================================== --- a/refs.bib +++ b/refs.bib @@ -1855,14 +1855,6 @@ toiti time-ordered normalization.} }
-@misc{de2003camlp4, - title={Camlp4 reference manual}, - author={de Rauglaudre, Daniel}, - howpublished = "\url{https://github.com/ocaml/camlp4%7D", - year={2003}, - note = "[Accessed 5-February-2017]" -} - @Article{DeBruijn72, author = DeBruijn, title = {Lambda-calculus Notation with Nameless Dummies, a Tool for @@ -5241,6 +5233,14 @@ toiti address = {Boston, Massachusetts, United States}, }
+@Book{CPP, crossref={Ritchie88}} +@Book{Ritchie88, + author = Ritchie #{and}# Kernighan, + title = {The C Programming Language}, + publisher = {Prentice-Hall}, + year = 1988 +} + @TechReport{Rose93, author = {Kristoffer Høgsbro Rose}, title = {Explicit Cyclic Substitutions}, @@ -5695,7 +5695,7 @@ toiti Engineering}, year = 2004, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.101.8265%7D, - note = {accessed 4-Feb-2017} + note = {[accessed 4-Feb-2017]} }
@InProceedings{Smith00, @@ -6677,6 +6677,14 @@ toiti pages = "145-156" }
+@misc{de2003camlp4, + title = {Camlp4 reference manual}, + author = {de Rauglaudre, Daniel}, + url = {https://github.com/ocaml/camlp4%7D, + year = 2003, + note = "[Accessed 5-Feb-2017]" +} + @phdthesis{girard72, author = "J. Y. Girard", title = "Interpr{'e}tation Fonctionnelle et {'E}limination des
View it on GitLab: https://gitlab.com/monnier/typer/commit/5b9a16706103bddc525c7a0768f1f28ce1ba...
Afficher les réponses par date