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

Commits: e883a92c by Vincent Archambault-Bouffard at 2017-02-03T12:43:24-05:00 Related Work. Still mising Dylan, Nemerle CamlP4.

- - - - -

2 changed files:

- paper.tex - refs.bib

Changes:

===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -867,19 +867,65 @@ to write and manipulate propositions and proofs. \section{Related work} \label{sec:related}

+\subsection{Operator precedence grammars} Operator precedence grammars~\cite{Floyd63}

-Mixfix~\cite{Danielsson08} in Agda~\cite{Bove09} - +\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 +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 +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 +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 +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 +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 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. + +\subsection{Dylan} Dylan~\cite{Dylan,Backrach99}

-Nemerle - -CamlP4 - -Template Haskell~\cite{Sheard02} +\subsection{CamlP4} +Pre Processor Pretty Printer

-Coq~\cite{Coq00} +\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 )

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

===================================== refs.bib ===================================== --- a/refs.bib +++ b/refs.bib @@ -3924,6 +3924,15 @@ toiti complete the design and implementation." }

+@inproceedings{mainland2007s, + title={Why it's nice to be quoted: quasiquoting for haskell}, + author={Mainland, Geoffrey}, + booktitle={Proceedings of the ACM SIGPLAN workshop on Haskell workshop}, + pages={73--82}, + year={2007}, + organization={ACM} +} + @Book{MIPS92, author = "Gerry Kane and Joe Heinrich", title = "{MIPS} {RISC} Architecture",

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