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

Commits: b43f0045 by Stefan Monnier at 2017-02-05T20:46:56-05:00 -

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -501,12 +501,15 @@ 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 -} -where the \id{quote} and \id{uquote} correspond respectively to the -backquote and comma in Common Lisp macros. +%% FIXME: The definition of `quote` is too long for this article, +%% and I'm not sure what more we could say about it. In Common-Lisp +%% the backquote is also defined as a macro. +%% \TODO{ +%% I thought you ought to define (or at least reference) +%% the quote/uquote... but check this for accuracy please +%% } +where \id{quote} is a macro which (with \id{uquote}) corresponds to the +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 @@ -949,15 +952,15 @@ to write and manipulate propositions and proofs. 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 -typed purely functional language. For such purpose, our use of a -monadic technique in Typer comes from Template Haskell. +typed purely functional language. %% For such purpose, our use of a +%% monadic technique in Typer comes from Template Haskell.

-But Typer and Template Haskell differs on how the macros are used by +But Typer and Template Haskell differ on how the macros are used by the programmer. In Template Haskell, macro calls are made explicit in the source file by preceding them with a $ sign. Also Template -Haskell is not meant to add new binding form to the language. Typer on +Haskell is not meant to add new binding forms to the language. Typer on the other hand can easily introduce new binding forms and domain -specific languages and macro calls look just like normal function calls. +specific languages, and macro calls look just like normal function calls.

Template Haskell also interleaves the type checking and template expansion phase. Templates are typed checked before expansion and the @@ -970,29 +973,15 @@ type safety.

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 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 using operator precedence grammar. For a more +of mixfix operators like \id{if_then_else_} as a way to add new +syntactic forms is what gave us the idea of adding mixfix to +S-expressions in Typer using operator precedence grammar. For a more detailed and formal discussion on mixfix operators and Agda, see~\cite{Danielsson08}.

-Agda doesn't have a macro system and up to our knowledge nothing in -theory prevents Agda from having one. We think our work with Typer -can showcase the potential of a macro system for Agda. - -\subsection{Coq} -Coq~\cite{Coq00} has both mixfix and a metaprogramming language known -as Ltac~\cite{Delahaye00}. Coq mixfix are similar to Typer's -mixfix a can be declared via \id{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. We wish for Typer to have the same language for both -purposes as Lisp and Scheme have already demonstrated the benefits of -having the same language for both. - -Nonetheless, it remains to be shown that macros are as user-friendly -to automate mathematical proofs as tactics written in Ltac which is a -domain specific language tailored for this task. +%% Agda doesn't have a macro system and up to our knowledge nothing in +%% theory prevents Agda from having one. We think our work with Typer +%% can showcase the potential of a macro system for Agda.

\subsection{Typed Racket}

@@ -1019,21 +1008,20 @@ expansion site.

\subsection{Dylan} Dylan~\cite{Dylan,Backrach99} is a functional and object-oriented -programming language with a macro system created in the early '90s. At +programming language with a macro system created in the early '90s. At first it had a prefix syntax like Lisp but Dylan changed its syntax to infix syntax a few years later.

-Thus, just like our work with Typer, Dylan had to deal with Lisp -macros in a infix syntax settings. Dylan infix syntax included among -other definitions, expressions and statements. The solution -implemented by Dylan to avoid syntax ambiguities was to offer three -kinds of macros. Defining macros for definition, statement macros and -function macros for expressions. +Dylan's syntax includes separate categories for definitions, expressions, +and statements, among others. The solution implemented by Dylan to avoid +syntax ambiguities was to offer three kinds of macros, one for definitions, +one for expressions, and one for statements, where the syntactic category of +each argument of a macro is specified by type.

-Typer tries to avoid as much a possible having many kinds of macros by -minimizing the number of syntactic categories. Also, the -S-expressions are still part of Typer's syntax so it is always -possible for the programmer to fall back to Lisp style use of macros. +%% Typer tries to avoid as much a possible having many kinds of macros by +%% minimizing the number of syntactic categories. Also, the +%% S-expressions are still part of Typer's syntax so it is always +%% possible for the programmer to fall back to Lisp style use of macros.

\subsection{Nemerle} @@ -1043,14 +1031,11 @@ possible for the programmer to fall back to Lisp style use of macros. % Vincent : In Typer if_then_else and for_each can be added as macros (or functions) % with operators. This is what I mean by new syntax.

-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} are -macros in Nemerle. - +Nemerle~\cite{Skalski2004meta} is a statically typed language targeting the +{.Net} platform with a C# like syntax and a rich macro system, as well as +extensible syntax, explicitly associated to specific macros. In fact most +structured programming construct like \id{while}, \id{for}, \id{foreach} are +defined as macros in Nemerle.

% \TODO{ % I don't see these syntax details described in \cite{Skalski2004meta}. @@ -1064,8 +1049,11 @@ macros in 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, -anything between parenthesis or braces is considered as list of tokens and attributed to one parameter. +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. So macro arguments are only parsed in a coarse way, +somewhat similar to Lisp's S-expressions. + % For example, the % below is the \id{if_then_else} construct from Nemerle's macro tutorial. % \begin{verbatim} @@ -1080,57 +1068,80 @@ anything between parenthesis or braces is considered as list of tokens and attri % else { ... } % \end{verbatim}

-The down side of this approach is that Nemerle macros have to parse -the list of tokens themselves if they are to implement new syntactic -form. Typer's on the other hand with its use of operator precedence -grammar, while not as rich as C# syntax, will parse the string of -tokens to an AST before sending it to the macro and avoids the -programmer the struggle of parsing the input by hand. +%% The down side of this approach is that Nemerle macros have to parse +%% the list of tokens themselves if they are to implement new syntactic +%% form. Typer's on the other hand with its use of operator precedence +%% grammar, while not as rich as C# syntax, will parse the string of +%% tokens to an AST before sending it to the macro and avoids the +%% programmer the struggle of parsing the input by hand.

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. - -\subsection{OCaml, CamlP4 and Extension Points} -Camlp4~\cite{de2003camlp4} stands for Caml Preprocessor and -Pretty-Printer. Much like a macro system, it allows the programmer to -describe an extension to the OCaml syntax or even a domain specific -language. The job of CamlP4 is to convert those extensions to standard -OCaml AST and feed it to the compiler. The syntax -extension is transparent to the programmer. But CamlP4 is a separate -tool from the compiler and the drawback of this approach is that, -unlike Nemerle or Typer, syntactic extensions do not have access to the -full compiler API. This is one of the main reasons why Typer adopts a -macro system which is build-in with the compiler. +program analysis capabilities. Nermerle macros have access to the compiler +API and can ask the compiler to elaborate one of its arguments for example +to find its type (if known to the compiler). %% This functionality is similar +%% to Typer's macros who also have access to the environment at the +%% expansion site. + +\subsection{OCaml} + +The OCaml language offers extensible syntax via its +Camlp4~\cite{de2003camlp4} system where the ``P4'' stands for PreProcessor +and Pretty-Printer. Much like a macro system, it allows the programmer to +describe an extension to the OCaml parser. The job of CamlP4 is to convert +those extensions to standard OCaml's AST. The syntax extension is transparent +to the programmer. But CamlP4 is a separate tool from the compiler and the +drawback of this approach is that, unlike Nemerle or Typer, syntactic +extensions do not have access to typing information. %% This is one of the +%% main reasons why Typer adopts a macro system which is build-in with +%% the compiler.

%ToDo : Find article/citation for Alain Frisch extension points (if any) -But CamlP4 has been replaced by extension points in recent versions of -OCaml (after version 4.01.0). Extension points work like macros, by -mapping OCaml AST to OCaml AST. The grammar now accepts annotations to -the source file and a special construct, extension nodes, for syntax -extension. When the compiler encounters an annotated branch in the AST -or an extension nodes in an expression it calls the macro associated -with the annotation. Like Template Haskell, annotations make it clear -that the programmer is using a syntax extension. Extension points -shows that it is possible to recover most of Lisp macros flexibility -in a language with a richer syntax modulo program annotations. - -In a language like Typer, where the philosophy is to push most -constructs out of the compiler and into libraries such method would -result in the source file being fully annotated everywhere. For -example, \id{if_then_else} and many other constructs are part of the -OCaml syntax and would require annotation in Typer if we were to use -such strategy. We therefore think Typer has hit a sweet spot between -Lisp and OCaml. +Recent versions of OCaml (after version 4.01.0) also come with +\emph{extension points}, which work like macros, by mapping OCaml AST to +OCaml AST. The grammar now accepts annotations to the source file and +a special construct, extension nodes, for syntax extension. When the +compiler encounters an annotated branch in the AST or an extension nodes in +an expression it calls the macro associated with the annotation. Of course, +as in the case of Template Haskell, this means that uses of those extensions +have to use a special syntax and hence feel like second-class features. + +%% In a language like Typer, where the philosophy is to push most +%% constructs out of the compiler and into libraries such method would +%% result in the source file being fully annotated everywhere. For +%% example, \id{if_then_else} and many other constructs are part of the +%% OCaml syntax and would require annotation in Typer if we were to use +%% such strategy. We therefore think Typer has hit a sweet spot between +%% Lisp and OCaml. + +\subsection{Coq} + +Coq~\cite{Coq00} has syntactic extensions similar to mixfix as well as +a metaprogramming language known as Ltac~\cite{Delahaye00}. Coq's syntactic +extensions, based on CamlP4, are fairly sophisticated. But Coq's +metaprogramming language is a separate language that is very different from +Coq core language Gallina and you can't directly invoke Ltac tactics from +Gallina code. This is a key difference between Coq and Typer. We wish for +Typer to have the same language for both purposes as Lisp and Scheme have +already demonstrated the benefits of having the same language for both. + +Nonetheless, it remains to be shown that macros are as user-friendly +to automate mathematical proofs as tactics written in Ltac which is a +domain specific language tailored for this task.

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

-Implementation in progress, available from -\url{http://gitlab.com/monnier/typer%7D. +We have presented the syntactic structure of the programming language Typer. +This shows how to extend Lisp's S-expressions with an infix syntax without +losing Lisp macros's power and flexibility, by using an operator precedence +grammar, which is a sweet spot that is flexible enough to provide a familiar +infix syntax, yet restricted enough that S-expressions can still be parsed +without needing to know anything about macros. + +Typer's implementation is available from +\url{http://gitlab.com/monnier/typer%7D. It is currently still +rather primitive. Our main focus is on developing its macro facilities to +have convenient access to typing information.

\begin{acks} The work is supported by the

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