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

Commits: 705cb09e by Vincent Archambault-Bouffard at 2017-02-06T11:39:43-05:00 Avoids goals list being alone on top right corner

- - - - - 8d24df5a by Vincent Archambault-Bouffard at 2017-02-06T12:08:24-05:00 Avoids code being cut in half by column break

- - - - - 9a943d60 by Vincent Archambault-Bouffard at 2017-02-06T12:27:04-05:00 Explicitly tells what's going on in the example

- - - - - c3ddaac4 by Vincent Archambault-Bouffard at 2017-02-06T12:38:04-05:00 Not perfect, but 1st member is with related text

- - - - - 9ac39976 by Vincent Archambault-Bouffard at 2017-02-06T12:42:24-05:00 Overfull box corrected.

- - - - - aec4fc6c by Vincent Archambault-Bouffard at 2017-02-06T12:45:52-05:00 Corrects overfull box

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -196,8 +196,9 @@ Racket~\cite{Felleisen11}).

The design of Typer aims to preserve and even extend the expressive power of Lisp's macros, but adapting it to the context of a statically typed -functional language in the tradition of ML~\cite{Milner84}. More specifically, -while designing Typer, we had the following goals: +functional language in the tradition of ML~\cite{Milner84}. + +More specifically, while designing Typer, we had the following goals: \begin{itemize} \item The language should be functional, statically typed, and with a syntax reminiscent of that of ML or Haskell. @@ -454,9 +455,13 @@ 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$.

-There is just one remaining construct in Typer, which is \kw{let}: This -allows you to introduce new locally scoped definitions. For example, we -could have defined the above map function as follows: +There is just one remaining construct in Typer, which is \kw{let}: +This allows you to introduce new locally scoped definitions. The shape +of this construct is +``$\texttt{let}~\id{decls}~\texttt{in}~\id{exp}$'' where \id{decls} is +a sequence of declarations such as the ones shown above, separated by +semi-colons. For example, we could have defined the above map function +as follows: \begin{verbatim} map = lambda (a : Type) (b : Type) (f : a -> b) -> let map' : List a -> List b; @@ -465,10 +470,7 @@ could have defined the above map function as follows: | cons x xs => cons (f x) (map' xs) in map' \end{verbatim} -As you can guess from this example, the shape of this construct is -``$\texttt{let}~\id{decls}~\texttt{in}~\id{exp}$'' where \id{decls} is -a sequence of declarations such as the ones shown above, separated by -semi-colons. +%As you can guess from this example,

So Typer has fundamentally two syntactic categories: expressions and declarations. A Typer file is defined as a sequence of declarations, @@ -625,8 +627,9 @@ is basically parsed as \begin{verbatim} let (x = (a; b)) in ((x = a); b) \end{verbatim} -So if Typer supported a similar grammar, when faced with a macro call of the -form +Notice that before the \id{in} keyword the ; has higher precedence than += and after it it's the opposite. So if Typer supported +a similar grammar, when faced with a macro call of the form \begin{verbatim} mymacro (x = a; b) \end{verbatim} @@ -849,12 +852,11 @@ recursive functions: \item \id{check} takes a type environment, an \id{Sexp}, and its expected type (an \id{Lexp}), and returns the elaborated form, of type \id{Lexp}. \end{itemize} -The type environment carries the type of every variable in scope, of course, -but it also carries the definition of all the variables in scope which were -defined via a \id{let} binding. - -The complete presentation of the type checker is out of scope of this -article, but we will simply sketch the way function calls are handled: +The type environment carries the type of every variable in scope, of +course, but it also carries the definition of all the variables in +scope which were defined via a \id{let} binding. The complete +presentation of the type checker is out of scope of this article, but +we will simply sketch the way function calls are handled: \begin{enumerate} \item When a function call is encountered, \id{infer} is called on the function part. @@ -1085,7 +1087,7 @@ to find its type (if known to the compiler). %% This functionality is similar \subsection{OCaml}

The OCaml language offers extensible syntax via its -Camlp4~\cite{de2003camlp4} system where the ``P4'' stands for PreProcessor +Camlp4 system~\cite{de2003camlp4} where the ``P4'' stands for PreProcessor and Pretty-Printer. Much like a macro system, it allows the programmer to describe an extension to the OCaml parser. The job of CamlP4 is to convert those extensions to standard OCaml's AST. The syntax extension is transparent @@ -1138,7 +1140,7 @@ grammar, which is a sweet spot that is flexible enough to provide a familiar infix syntax, yet restricted enough that S-expressions can still be parsed without needing to know anything about macros.

-Typer's implementation is available from +Typer's implementation is available online from \url{http://gitlab.com/monnier/typer%7D. It is currently still rather primitive. Our main focus is on developing its macro facilities to have convenient access to typing information.

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