Vincent Archambault-Bouffard pushed to branch report/els-2017 at Stefan / Typer
Commits: 13d5b472 by Vincent Archambault-Bouffard at 2017-02-05T00:54:20-05:00 Related Work : Roughly finished
- - - - - 73c70e0f by Vincent Archambault-Bouffard at 2017-02-05T01:27:12-05:00 Archamboult -> Archambault
- - - - - 26ac2071 by Vincent Archambault-Bouffard at 2017-02-05T03:27:07-05:00 Related Work done
- - - - - 89756e44 by Vincent Archambault-Bouffard at 2017-02-05T04:04:35-05:00 Merge branch 'report/els-2017' of https://gitlab.com/monnier/typer into report/els-2017
- - - - -
2 changed files:
- paper.tex - refs.bib
Changes:
===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -177,7 +177,7 @@ of syntactic categories and generally make ``everything'' first-class.
\maketitle \renewcommand \shortauthors { - P. Delaunay, V. Archamboult-Bouffard, and S. Monnier} + P. Delaunay, V. Archambault-Bouffard, and S. Monnier}
\section{Introduction}
@@ -888,10 +888,6 @@ to write and manipulate propositions and proofs. \section{Related work} \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 @@ -904,34 +900,43 @@ But Typer and Template Haskell differs 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 -the other hand can easily introduce new binding forms and domain specific languages. In Template Haskell, quasiquotation~\cite{mainland2007s} -can be used for introducing domain specific languages but again their -use in the source file is not transparent to the programmer. +the other hand can easily introduce new binding forms and domain +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 +final code after expansion is also typed checked. Unlike Typer, this +is not done to determine if an expression is a macro call or not +because the use of the $ sign makes it easy, but simply to ensure +type safety.
\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 mixfix 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~\citet{Danielsson08}. +S-expression 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 a one. Although Typer's syntax is -simpler because of the use of S-expressions than Agda's syntax, we -think our work with Typer can showcase the potential of a macro system -for Agda. +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. Coq mixfix are similar to Typer's mixfix a can be declared -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 -language for both programming and metaprogramming and Typer aims to -keep those advantages. +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.
\subsection{Typed Racket}
@@ -956,71 +961,114 @@ 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} +Dylan~\cite{Dylan,Backrach99} is a functional and object-oriented +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.
-\subsection{CamlP4} -Pre Processor Pretty Printer +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.
-\subsection{Nemerle} +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.
-\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 + +\subsection{Nemerle} +% \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. } +% 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}, -\id{using} are macros in Nemerle. +programming construct like \id{while}, \id{for}, \id{foreach} 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). -} +% \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). +% } +% Vincent : Indeed google scholar says they are in there but Springer +% says the opposite. +% But syntax details are in the text (for macro) and also on the github page. + 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. 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. - -%% 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} +anything between parenthesis or braces is considered as list of tokens and attributed to one parameter. +% 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} + +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. +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. + +%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.
\section{Conclusion and future work} \label{sec:conclusion}
===================================== refs.bib ===================================== --- a/refs.bib +++ b/refs.bib @@ -1798,6 +1798,7 @@ toiti generation.} }
+ @Article{Danvy96:eta, author = Danvy #{and Karoline Malmkj{\ae}r and Jens Palsberg}, title = {Eta-Expansion Does {T}he {T}rick}, @@ -1854,6 +1855,14 @@ 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
View it on GitLab: https://gitlab.com/monnier/typer/compare/c53087055fbabe7243a96d53a511ff35bf2...