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

Commits: fa6dcfed by Vincent Archambault-Bouffard at 2017-02-03T21:52:22-05:00 Spelling

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -888,9 +888,8 @@ 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 form and built tower -of languages. In Template Haskell, quasiquotation~\cite{mainland2007s} -can be use for introducing domain specific langages but again their +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.

\subsection{Agda} @@ -901,25 +900,25 @@ 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}.

-Agda doesn't have a macros system and up to our knowledge nothing in +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.

\subsection{Coq} -Coq~\cite{Coq00} has both mixfix and a metaprogramming langage known +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 -separate langage that is very different from Coq core langage +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 -langage for both programming and metaprogramming and Typer aims to +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 macros system and a stactic types +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. @@ -927,17 +926,17 @@ 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 +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 generaly Scheme macros on the -other hand do not have access to the environement at the expansion +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 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. +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} @@ -946,21 +945,21 @@ Dylan~\cite{Dylan,Backrach99} Pre Processor Pretty Printer

\subsection{Nemerle} -Nemerle~\cite{skalski2004meta} is a statically typed langage targeting +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 acheive mixfix syntax like +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.

-To avoid ambiguities with the basic langage syntax the \id{Syntax} +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 literals and macro parameters. In a macro call, +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. For example the +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) @@ -974,7 +973,7 @@ if (a == 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. +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}

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