Vincent Archambault-Bouffard pushed to branch report/els-2017 at Stefan / Typer

Commits: 5a562a41 by Vincent Archambault-Bouffard at 2017-02-03T15:41:08-05:00 Related Work : Nemerle

- - - - -

2 changed files:

- paper.tex - refs.bib

Changes:

===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -889,8 +889,7 @@ 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 mifix 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}. @@ -902,18 +901,36 @@ 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 langage 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 separate langage that is very different from Coq core langage Gallina. This is a key difference between Coq and Typer. Lisp and Scheme have already demonstrated the benefits of having the same langage for both programming and metaprogramming and Typer aims to keep those advantages. +Coq~\cite{Coq00} has both mixfix and a metaprogramming langage 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 +separate langage that is very different from Coq core langage +Gallina. This is a key difference between Coq and Typer. Lisp and +Scheme have already demonstrated the benefits of having the same +langage 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 macros system and a stactic types 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 intented 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 generaly Scheme macros on the other hand do not have access to the environement 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 langages. Thus Typed Racket lacks algebraic datatypes, its variables are mutables and is impure. In that regard, Typer is closer to Coq core langage Gallina than Typed Racket. +At first look one might see Typer as a dependently typed Typed +Racket. Indeed both have a powerful macros system and a stactic types +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 intented 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 generaly Scheme macros on the +other hand do not have access to the environement 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 langages. Thus Typed Racket lacks algebraic datatypes, its +variables are mutables and is impure. In that regard, Typer is closer +to Coq core langage Gallina than Typed Racket.

\subsection{Dylan} Dylan~\cite{Dylan,Backrach99} @@ -922,10 +939,35 @@ Dylan~\cite{Dylan,Backrach99} Pre Processor Pretty Printer

\subsection{Nemerle} -Macros have access to the context / compiler -They are different macro categories (4 of them) -We cannot use the given macro without an "else" construct, as we can in C, since "else" is a required keyword, and it is not possible to make it non-required, because it would introduce ambiguity (after all, "if" could be used in an expression!) -Syntax must be surrounded by ( and ) +Nemerle~\cite{skalski2004meta} is a statically typed langage 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 acheive 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. + +To avoid ambiguities with the basic langage syntax the \id{Syntax} +construct imposes a few restrictions. The programmer can only declare +a sequence of text literals 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. 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 macros 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 the environnement the at expansion site.

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

===================================== refs.bib ===================================== --- a/refs.bib +++ b/refs.bib @@ -5675,6 +5675,14 @@ 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} +} + @InProceedings{Smith00, author = {Frederick Smith and}# Walker #{and}# Morrisett, title = {Alias Types},

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