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

Commits: 7878ed44 by Christopher League at 2017-02-03T19:26:18-05:00 Fix minor typos

- - - - - 6292e762 by Christopher League at 2017-02-03T19:26:18-05:00 Fix/add a couple URLs in bib

- - - - - ea608585 by Christopher League at 2017-02-03T19:26:18-05:00 Cite Steele's book for Common Lisp

I thought there should be some reference for these syntactic-category macros (I'm not really familiar with them), although Steele's book only defines `symbol-macrolet`, not the others. The `defsetf` can be found in some LispWorks documentation, and as far as I can tell, `pcase-defmacro` is only an Elisp thing...?

- - - - - d0562f79 by Christopher League at 2017-02-03T19:26:18-05:00 Wording fix

- - - - - 44c20b9a by Christopher League at 2017-02-03T19:26:18-05:00 Explain the quote/uquote primitives? (see TODO)

- - - - - b3526f6d by Christopher League at 2017-02-03T19:26:18-05:00 Correct mismatched parens in OPG example

It seems like you're not parenthesizing the outermost Sexp in these examples, so I'll leave off the outermost... but it initially had an outer close-paren.

- - - - - 7c78df2b by Vincent Archambault-Bouffard at 2017-02-03T21:26:41-05:00 Update .gitignore list.

- - - - - 42a22913 by Vincent Archambault-Bouffard at 2017-02-03T21:32:16-05:00 Merge branch 'report/els-2017' of gitlab.com:league/typer into report/els-2017

Pull changes made by Christopher League

- - - - -

3 changed files:

- .gitignore - paper.tex - refs.bib

Changes:

===================================== .gitignore ===================================== --- a/.gitignore +++ b/.gitignore @@ -5,3 +5,5 @@ *.blg *.out comment.cut +auto/* +_build/*

===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -225,15 +225,15 @@ Typer's core language is based on a Pure Type System~\cite{Barendregt91b}, so as to use a single syntactic category for types and expressions. More specifically, its core language is similar to that of proof assistants such as Coq~\cite{Coq00} and can also be used to write logical propositions -and proofs. So beside being used for syntactic extensions, Typer macros intend -to be used to automate the construction of proofs, similar to what is done +and proofs. So beside being used for syntactic extensions, Typer macros may +be used to automate the construction of proofs, similar to what is done with tactic languages~\cite{Delahaye00, Ziliani13}.

In Sec.~\ref{sec:background}, we begin by giving some background on Lisp's macro system; in Sec~\ref{sec:primer} we give a short Typer primer; in Sec.~\ref{sec:parsing} we show how preliminary parsing is performed; in Sec.~\ref{sec:elaboration} we present how macros get expanded into the core -language; in Sec~\ref{sec:related} we discus related work; and in +language; in Sec~\ref{sec:related} we discuss related work; and in Sec.~\ref{sec:conclusion} we conclude with some discussion of future work.

\section{Background} @@ -314,10 +314,11 @@ declarations, expressions, statements, annotations, etc, treating them all as expressions.

Of course, in practice it's virtually impossible to only have a single -syntactic category. For example, Common Lisp provides separate macros for -the syntactic category of symbols (\kw{symbol-macrolet}) and lvalues -(\kw{defsetf}), and Emacs Lisp similarly uses separate macros to define new -patterns (\kw{pcase-defmacro}). +syntactic category. For example, Common Lisp \cite{Steele90} provides +separate macros for the syntactic category of symbols +(\kw{symbol-macrolet}) and lvalues (\kw{defsetf}), and Emacs Lisp +similarly uses separate macros to define new patterns +(\kw{pcase-defmacro}).

Languages like Dylan do not try to unify all syntactic categories and instead provide separate macros for use in contexts such as definitions or @@ -332,11 +333,12 @@ more generally useful.

\subsection{No special syntax for macro calls}

-The basic syntax of Lisp macros is indistinguishable from the basic syntax -of primitive syntactic forms. This means that the user does not need to -know if \kw{cond} is implemented as a primitive or as a macro to expands to -a bunch of \kw{if}, or vice versa. This is a very important property in -order to make the language truly extensible. +The basic syntax of Lisp macros is indistinguishable from the basic +syntax of primitive syntactic forms. This means that the user does not +need to know if \kw{cond} is implemented as a primitive or as a macro +that expands to a bunch of \kw{if} expressions, or vice versa. This is +a very important property in order to make the language truly +extensible.

Other systems such as Template Haskell instead use a special syntactic form for macro calls. While the difference may appear to be cosmetic and of no @@ -418,8 +420,8 @@ traditional \id{map} function as follows: Here you see a new notation of the form \texttt{(x~:~t$_1$) -> t$_2$}. It is the dependent function type, used to give a name to the function argument, so it can be used in the return type. In type theory this is -often presented with the notation $\Pi x:t_1 . t_2$, but in the above case it -is better read as a universal quantifier $\forall x:t_1 . t_2$. The normal +often presented with the notation $\Pi,x!:!t_1 . t_2$, but in the above case it +is better read as a universal quantifier $\forall x!:!t_1 . t_2$. The normal function type \texttt{t$_1$ -> t$_2$} is actually a shorthand for \texttt{(x~:~t$_1$) -> t$_2$} used when the variable \id{x} is not used inside $t_2$. @@ -446,7 +448,7 @@ separated by semi-colons. Most Lisps manage to conflate those two categories, but in our case, we were unable to unify them without introducing more problems. E.g. Common-Lisp solves the problem by treating declarations like \kw{defun} as side-effects on the global environment (an -option we do not have, since your language is purely functional), and Scheme +option we do not have, since our language is purely functional), and Scheme solves it in a way that's more compatible with purity, but still relies on the use of sequences of expressions which again does not come naturally in a purely functional language. @@ -471,6 +473,11 @@ 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. + 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 code, \id{ME} is the macro-expansion monad, used for the same purpose as the @@ -578,7 +585,7 @@ other way. In the case of Typer, instead of writing \end{verbatim} the user can write \begin{verbatim} - _=_ x (_+_ (_*_ a b) c)) + _=_ x (_+_ (_*_ a b) c) \end{verbatim} and these two notations result in identical S-expressions, just like in Lisp, expressions like \texttt{(a . (b))} and \texttt{(a b)} cannot be @@ -590,7 +597,7 @@ thanks to two more rules: \item If two keywords have the same precedence, then they are part of the same construct. \item A keyword can have a ``nil'' precedence on the left or on the right, - meaning that it is a prefix resp.~postfix operator. + meaning that it is a prefix or (respectively) postfix operator. \end{itemize} So, if the tokens ``['' and ``]'' are given precedences respectively $(\id{nil}, 0)$ and $(0, \id{nil})$, they will be treated as the usual

===================================== refs.bib ===================================== --- a/refs.bib +++ b/refs.bib @@ -985,6 +985,7 @@ toiti Dependent Types}, crossref = {TPHOLs09}, pages = {73-78}, + url = {http://www.cse.chalmers.se/~ulfn/papers/tphols09/tutorial.pdf%7D, abstract = {We give an overview of Agda, the latest in a series of dependently typed programming languages developed in Gothenburg. Agda is based on Martin-Löf’s intuitionistic @@ -1884,7 +1885,7 @@ toiti title = {A Tactic Language for the System {C}oq}, crossref = {LPAR00}, pages = {85-95}, - url = {http://www.lirmm.fr/~delahaye/papers/ltac (LPAR'00).pdf}, + url = {https://pdfs.semanticscholar.org/51e8/2c766a9fb5d476c00dbe96530a5b4c0ded92.p..., abstract = {We propose a new tactic language for the system Coq, which is intended to enrich the current tactic combinators (tacticals). This language is based on a functional core @@ -5116,7 +5117,7 @@ toiti volume = 22, number = 1, pages = {1-44}, - month = {jan}, + month = {Jan}, url = {http://dl.acm.org/citation.cfm?id=345100%7D, abstract = {We study two partial type inference methods for a language combining subtyping and impredicative polymorphism. @@ -5585,7 +5586,8 @@ toiti author = Sheard #{and}# Simon, title = {Template metaprogramming for {Haskell}}, crossref = {Haskell02}, - pages = {1-16} + pages = {1-16}, + url = {http://dl.acm.org/citation.cfm?id=636528%7D }

@InProceedings{Sheard04, @@ -5795,6 +5797,13 @@ toiti design by showing a number of type-safe tactics and decision procedures written in VeriML.} } +@Book{Steele90, + author = "Guy L. Steele", + title = "Common Lisp the Language", + year = "1990", + publisher = "Digital Press", + url = "https://www.cs.cmu.edu/Groups/AI/html/cltl/cltl2.html" +} @InProceedings{Steele93, author = "Guy L. Steele and Richard P. Gabriel", title = "The Evolution of {LISP}",

View it on GitLab: https://gitlab.com/monnier/typer/compare/5a562a41c0bde791a30048d49025bc0ab88...