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

Commits: c5308705 by Stefan Monnier at 2017-02-04T22:19:49-05:00 -

- - - - -

2 changed files:

- paper.tex - refs.bib

Changes:

===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -26,7 +26,8 @@

\usepackage{amsfonts}

-\usepackage{todonotes} +\usepackage{todonotes} \newcommand \TODO {\todo[inline]} + %% \usepackage{natbib} \renewcommand \cite \citep

@@ -318,7 +319,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}). +(\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 @@ -473,8 +475,10 @@ defined as follows: in (uquote body))) in return code; \end{verbatim} -% TODO: I thought you ought to define (or at least reference) -% the quote/uquote... but check this for accuracy please: +\TODO{ + I thought you ought to define (or at least reference) + the quote/uquote... but check this for accuracy please +} where the \id{quote} and \id{uquote} correspond respectively to the backquote and comma in Common Lisp macros.

@@ -486,6 +490,11 @@ 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} @@ -516,6 +525,11 @@ tokenizing later.

\subsection{Operator precedence grammar}

+\TODO{ + better explain the stuff about inserting parentheses; explain + the notation ``kw1 e kw2''; Give an example right away +} + Typer's external notion of S-expression is more flexible than Lisp's, since it allows infix notation. It relies on operator precedence grammars (OPG)~\cite{Floyd63} for that. An OPG is a very restrictive subset of @@ -875,9 +889,11 @@ to write and manipulate propositions and proofs. \label{sec:related}

\subsection{Operator precedence grammars} +\TODO{Maybe there's nothing to say, here.} Operator precedence grammars~\cite{Floyd63}

\subsection{Template Haskell} + Template Haskell~\cite{Sheard02} is an extension of Haskell to allow compile time metaprogramming. One of the main contribution of Template Haskell is to implement a metaprogramming system on top of a strongly @@ -893,12 +909,13 @@ can be used for introducing domain specific languages but again their use in the source file is not transparent to the programmer.

\subsection{Agda} + Agda's~\cite{Bove09} syntax is similar to Haskell's syntax with the possibility of adding mixfix and not just infix operators. Their use -of mifix operators like \id{if_then_else} as a way to add new +of mixfix operators like \id{if_then_else_} as a way to add new syntactic form is what gave us the idea of adding mixfix to S-expression in Typer. For a more detailed and formal discussion on -mixfix operators and Agda, see Danielsson~\cite{Danielsson08}. +mixfix operators and Agda, see~\citet{Danielsson08}.

Agda doesn't have a macro system and up to our knowledge nothing in theory prevents Agda from having a one. Although Typer's syntax is @@ -909,7 +926,7 @@ for Agda. \subsection{Coq} Coq~\cite{Coq00} has both mixfix and a metaprogramming language known as Ltac. Coq mixfix are similar to Typer's mixfix a can be declared -via \id{Notation} statement. But Coq's metaprogramming language is a +via \kw{Notation} statement. But Coq's metaprogramming language is a separate language that is very different from Coq core language Gallina. This is a key difference between Coq and Typer. Lisp and Scheme have already demonstrated the benefits of having the same @@ -917,26 +934,33 @@ language for both programming and metaprogramming and Typer aims to keep those advantages.

\subsection{Typed Racket} -At first look one might see Typer as a dependently typed Typed -Racket. Indeed both have a powerful macro system and a static type -system. But there are some important differences. The first difference -directly related to this article is that Typed Racket lacks built-in -support for mixfix. - -Another important difference is that Typed Racket macros ala Scheme -are hygienic while Typer's macro ala Lisp are not. Typer is still in -its infancy and hygienic macros is future work. Also, Typer's macros -are intended to work with dependently typed piece of code and -mathematical proofs and thus require access to the environment at the -expansion site. Typed Racket and more generally Scheme macros, on the -other hand, do not have access to the environment at the expansion -site and only to their arguments. - -Futhermore, Typed Racket is an extension of Racket with polymorphic -types and by design aims to be compatible with Racket, a dynamically -typed language. Thus Typed Racket lacks algebraic datatypes, its -variables are mutable and is impure. In that regard, Typer is closer -to Coq core language Gallina than Typed Racket. + +Typed Racket~\cite{Felleisen11} uses an extension of Scheme's macro system +to implement a statically typed variant of Racket as a sort of embedded DSL, +thus implementing the type checker as part of a macro. It shares with Typer +the characteristic of mixing Lisp-style macros and static typing. But its +syntax is based on traditional Lisp-style parenthesized S-expressions. + +%% At first look one might see Typer as a dependently typed Typed +%% Racket. Indeed both have a powerful macro system and a static type +%% system. But there are some important differences. The first difference +%% directly related to this article is that Typed Racket lacks built-in +%% support for mixfix. + +Another important difference is that Typed Racket macros ala Scheme are +hygienic while Typer's macros currently do not support hygiene. +%% Typer is still in its infancy and hygienic macros is future work. +Also, Typer's macros are intended to work with dependently typed pieces of +code and mathematical proofs and thus require access to the type environment +at the expansion site. Typed Racket and more generally Scheme macros, on +the other hand, do not have access to the lexical environment at the +expansion site. + +%% Furthermore, Typed Racket is an extension of Racket with polymorphic +%% types and by design aims to be compatible with Racket, a dynamically +%% typed language. Thus Typed Racket lacks algebraic datatypes, its +%% variables are mutable and is impure. In that regard, Typer is closer +%% to Coq core language Gallina than Typed Racket.

\subsection{Dylan} Dylan~\cite{Dylan,Backrach99} @@ -945,35 +969,58 @@ Dylan~\cite{Dylan,Backrach99} Pre Processor Pretty Printer

\subsection{Nemerle} -Nemerle~\cite{skalski2004meta} is a statically typed language targeting -the .Net platform with a C# like syntax and has a rich macro -system. Like in Typer, Nemerle macros can add new syntax with the -construct \id{Syntax}. Nemerle can achieve mixfix syntax like -\id{if_then_else} with this construct. In fact most structured + +\TODO{ + Actually, in Typer we currently can't add new syntax, and there's no + reason why it should be strictly linked to the definition of new macros. +} +Nemerle~\cite{Skalski2004meta} is a statically typed language targeting +the {.Net} platform with a C# like syntax and has a rich macro +system. +Like in Typer, Nemerle macros can add new syntax with the +construct \id{Syntax}. Nemerle can achieve mixfix syntax like +\id{if_then_else_} with this construct. In fact most structured programming construct like \id{while}, \id{for}, \id{foreach}, \id{using} are macros in Nemerle.

+ +\TODO{ + I don't see these syntax details described in \cite{Skalski2004meta}. + Also I can't see where this article was published (some references say + GPCE'04, but Springer-Verlag's list of contents for GPCE'04 doesn't + include anything about Nemerle). +} To avoid ambiguities with the basic language syntax the \id{Syntax} -construct imposes a few restrictions. The programmer can only declare -a sequence of text literal and macro parameters. In a macro call, +construct imposes a few restrictions. The programmer can only declare +a sequence of text literal and macro parameters. In a macro call, anything between parenthesis or braces is considered as list of tokens -and attributed to one parameter. In many regards, \id{Syntax} if very +and attributed to one parameter. In many regards, \id{Syntax} if very similar to Lisp macros where subexpressions must also be between -parenthesis and some part of the syntax can be considered keywords. For example, the -below is the \id{if_then_else} construct from Nemerle's macro tutorial. -\begin{verbatim} -macro @if (cond, e1, e2) -syntax ("if", "(", cond, ")", e1, Optional (";"), - "else", e2) -{ ... -} - -if (a == 123) -{ def msg = " 'a' has value 123"; ...; } -else { ... } -\end{verbatim} - -Another part of Nemerle macros similar to Typer's macro system is his program analysis capabilities. Nermerle macros have access to the compiler API and can request for example the type (if known to the compiler) of a piece of code received as an argument. This functionality is similar to Typer's macros who also have access to the environment at the expansion site. +parenthesis and some part of the syntax can be considered keywords. + +%% FIXME: I commented this out because I don't think it's needed. It just +%% shows what is the syntax of Nemerle's macro declarations, which is not +%% under discussion here. +%%For example, the below is the \id{if_then_else_} construct from +%%Nemerle's macro tutorial. +%%\begin{verbatim} +%%macro @if (cond, e1, e2) +%%syntax ("if", "(", cond, ")", e1, Optional (";"), +%% "else", e2) +%%{ ... +%%} + +%%if (a == 123) +%%{ def msg = " 'a' has value 123"; ...; } +%%else { ... } +%%\end{verbatim} + +Another part of Nemerle macros similar to Typer's macro system is his +program analysis capabilities. Nermerle macros have access to the compiler +API and can request for example the type (if known to the compiler) of +a piece of code received as an argument. This functionality is similar to +Typer's macros who also have access to the environment at the +expansion site.

\section{Conclusion and future work} \label{sec:conclusion}

===================================== refs.bib ===================================== --- a/refs.bib +++ b/refs.bib @@ -5677,12 +5677,16 @@ toiti type-inference algorithms. } }

-@article{skalski2004meta, - title={Meta-programming in Nemerle}, - author={Skalski, Kamil and Moskal, Michal and Olszta, Pawel}, - journal={Proceedings Generative Programming and Component Engineering}, - year={2004}, - publisher={Citeseer} +@article{Skalski2004meta, + title = {Meta-programming in Nemerle}, + author = {Skalski, Kamil and Moskal, Michal and Olszta, Pawel}, + Xnote = {It's usually cited as being in GPCE04, but the contents of + Springer's GPCE04 proceedings doesn't include it!}, + Xjournal = {Proceedings Generative Programming and Component + Engineering}, + year = 2004, + url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.101.8265%7D, + note = {accessed 4-Feb-2017} }

@InProceedings{Smith00,

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