Stefan pushed to branch report/scheme-2017 at Stefan / Typer

Commits: c7b5dc18 by Stefan Monnier at 2017-05-23T02:34:18-04:00 -

- - - - -

2 changed files:

- paper.tex - refs.bib

Changes:

===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -184,146 +184,110 @@ knowing what role they will play. \renewcommand \shortauthors { P. Delaunay, V. Archambault-Bouffard, and S. Monnier}

-\TODO{Cite \cite{Culpepper10, Burmako13}} - -\section{New Introduction} +\section{Introduction}

The defining feature of languages from the Lisp family of languages has been their exclusive reliance on a very simple and regular base syntax, basically composed of atomic elements like symbols, strings, and numbers, and -parenthesized subtrees. While this limitations is what makes Lisp -unpalatable to some programmers, it is also the fundamental element that -gives Lisp its unequaled power for metaprogramming. +parenthesized and prefixed subtrees. While this limitations is what makes +Lisp unpalatable to some programmers, it is also the fundamental element +that gives Lisp its unequaled power for metaprogramming.

Attempts to add comparable macro systems to languages with a richer syntax -invariably face the need to introduce a lot of complexity. Some of that -complexity comes from the need to expose how that richer syntax gets mapped -to some data representation. Some comes from the presence of various -syntactic categories (such as expressions, instructions, types annotations, -or declarations) which not only makes the macro system more complex in -itself but can also make it less convenient to use because the macro's -argument might end up parsed using the ``wrong'' syntactic category. - -In Typer we wanted to benefit from a Lisp-style simple yet all-powerful -macro system, but without giving up on the more traditional infix notation. -Most language from the Lisp family use various ad-hoc exceptions to (which -you might call extensions of) the base syntax, such the use of the -traditional `\texttt{`}', and `\texttt{,}' prefix symbols for -quasi-quoting, the use of ``\textsl{var}:\textsl{syntaxclass}'' shorthand -in Racket's \texttt{syntax-parse}, or the use of \texttt{{}} - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -\section{Introduction} - -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~\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 -hierarchy of languages when it comes to its support for macro processing. -Yet, as far as we can tell, this flexibility has stayed confined to -dynamically typed languages (with the notable exception of Typed -Racket~\cite{Felleisen11}). - -The design of Typer aims to preserve and even extend the expressive power of -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, 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} +invariably face the need to introduce a lot of complexity. There are 2 main +sources of complexity: Some of that complexity comes from the need to expose +how that richer syntax gets mapped to some data representation. But the +main source is the presence of various syntactic categories (such as +expressions, instructions, types annotations, or declarations) which not +only makes the macro system more complex in itself but can also make it less +convenient to use because the parser needs to decide early on which syntactic +category to use to parse each macro call's actual arguments. + +There is clearly a desire to extend Lisp with a richer syntax, as evidenced +by the various ad-hoc exceptions (which you might call extensions) to the +base parenthesized-prefix syntax present in languages from the Lisp family, +such as the use of the traditional `\texttt{`}', and `\texttt{,}' prefix +symbols for quasi-quoting, Common-Lisp's ``\textsl{pkg}:\textsl{id}'' +qualified identifiers or ``\textsl{var} \texttt{in} \textsl{exp}'' in +the \kw{loop} macro, Racket's \texttt{syntax-parse}'s +``\textsl{var}:\textsl{syntaxclass}'' shorthand~\cite{Culpepper10}, +TypedRacket's ``\texttt{[}\textsl{var} \texttt{:} \textsl{type}\texttt{]}'' +in formal arguments~\cite{Felleisen08}, or Clojure's destructuring +``\texttt{[}\textsl{pattern} \texttt{:as} \textsl{var}\texttt{]}'' +pattern~\cite{Clojure}. + +%% Indeed, when designing Typer, a statically typed language, we found +%% Lisp-style parenthesized prefix notation unpalatable. +In Typer we decided to generalize this to a more conventional infix +notation, while still keeping as much as possible of Lisp's simple yet +all-powerful macro system. We do this in two ways: first, we define the +infix syntax as mere syntactic sugar, second we stick to a single syntactic +category. Just as in Lisp, the parser building the S-expression (i.e. the +\emph{reader}) does not need to know if it's parsing an instruction, or an +expression, or a type annotation, because they are all parsed in the +same way. + +The result is a syntax which superficially looks like ML, but whose +underlying structure is that of Lisp. Some of the motivation behind this is +to have an ML-style language with the superior Lisp-style support for +embedded DSLs, as well as the desire like in Scheme to define as much of the +language as possible in the form of libraries layered on top of +a minimalist core. + +%% 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~\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 +%% hierarchy of languages when it comes to its support for macro processing. +%% Yet, as far as we can tell, this flexibility has stayed confined to +%% dynamically typed languages (with the notable exception of Typed +%% Racket~\cite{Felleisen11}). + +%% The design of Typer aims to preserve and even extend the expressive power of +%% 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, 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 -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 -making it possible for some of the new syntax to introduce new syntactic -categories, such as patterns. Finally, we think the third goal might come -out for free if the second is satisfied well-enough. - -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 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. -More specifically, its core language is similar to that of proof assistants -such as Coq~\cite{Coq00} and can also be used to write logical propositions -and proofs. So beside being used for syntactic extensions, Typer macros may -be used to automate the construction of proofs, similar to what is done -with tactic languages~\cite{Delahaye00, Ziliani13}. +This means we should be able to define constructs such as +``$\kw{if}~e_1~\kw{then}~e_2~\kw{else}~e_3$'' in the language itself, or +that compilation of pattern matching is implemented in a library rather than +inside 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 making it possible for some of +the +%% new syntax to introduce new syntax classes, such as patterns. +%% Finally, we think the third goal might come out for free if the second is +%% satisfied well-enough. + +%% 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, while more complex than that of Lisp, is still very primitive, +since it uses an \emph{operator precedence grammar}~\cite{Floyd63}. This is +the sweet spot which gives us just enough power to handle a syntax that +should feel familiar to ML and Haskell users, while still being able to +parse the code without needing to know if it's in the middle of a type +annotation, function declaration, or some as-yet unknown DSL syntax. + +%% Typer's core language is based on a Pure Type System \cite{Barendregt91b}, +%% so as to use a single syntax class for both types and expressions. +%% More specifically, its core language is similar to that of proof assistants +%% such as Coq~\cite{Coq00} and can also be used to write logical propositions +%% and proofs. So beside being used for syntactic extensions, Typer macros +%% should ultimately be used to automate the construction of proofs, similar to +%% what is done with tactic languages~\cite{Delahaye00, Ziliani13}, although +%% this is not currently supported.

In Sec.~\ref{sec:background}, we begin by giving some background on Lisp's macro system; in Sec~\ref{sec:primer} we give a short Typer primer; in @@ -1043,6 +1007,8 @@ to write and manipulate propositions and proofs. \section{Related work} \label{sec:related}

+\TODO{Cite \cite{Culpepper10, Burmako13, Rafkind12}} + \subsection{Template Haskell}

Template Haskell~\cite{Sheard02} is an extension of Haskell to allow

===================================== refs.bib ===================================== --- a/refs.bib +++ b/refs.bib @@ -5244,6 +5244,24 @@ toiti year = 1993 }

+@InProceedings{Rafkind12, + author = {Jon Rafkind and}# Flatt, + title = {Honu: A Syntactically Extensible Language}, + journal = {Proceedings Generative Programming and Component + Engineering}, + year = 2012, + crossref = {GPCE12}, + abstract = {Honu is a new language that fuses traditional algebraic + notation (e.g., infix binary operators) with Scheme-style + language extensibility. A key element of Honu’s design is + an enforestation parsing step, which converts a flat + stream of tokens into an S-expression-like tree, in + addition to the initial “read” phase of parsing and + interleaved with the “macro-expand” phase. We present the + design of Honu, explain its parsing and macro-extension + algorithm, and show example syntactic extensions.} +} + @TechReport{Ramsey98, author = Ramsey #{and}# Simon, title = {Exceptions Need Not Be Exceptional},

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

--- View it on GitLab: https://gitlab.com/monnier/typer/commit/c7b5dc18fb67232a579471ab8be1e8023c7f... You're receiving this email because of your account on gitlab.com.