Janvier 2017 - Typer - mailman.iro.umontreal.ca

Datatypes and tuples
by Stefan Monnier 02 Oct '18

02 Oct '18

Hi guys, Wondering if you might have an idea: In Typer, the basic datastructure is the "algebraic datatype" (which combines a sum, product, and recursion), and the basic eliminator is the "pattern matching case". It works OK, but is unsatisfactory: 1- both of those are fairly large/complex. 2- it means that extracting a record field is a "case" operation that discards all but the required field, so it's an O(n) operation (where n is the size of the record), if not in the final code, at least in intermediate code. 3- it means the choice of representation of datatype tags is hardcoded in the blackbox compiler. While point n°2 might seem irrelevant, it is a pain with large records, such as those you might get when records are used to represent modules: the encoding of the simple "String.concat" reference ends up taking space proportional to the number of primitives exported from the "String" module, which can be rather large. I'd like to find another option and was thinking of something along the following lines: - provide a separate product primitive. - provide a "union" type, i.e. an *untagged* sum. - provide primitive discrimination operations, such as "dispatch on an Int". then the Either type could look like Either a b = union (Singleton(1), a) (Singleton(2), b) and case e | Left x => ... | Right y => ... would turn into switch (e.0 <withmagicproof>) | 1 => let e' = cast (Singleton(1), a) e; x = e'.1 in ... | 2 => let e' = cast (Singleton(2), b) e; y = e'.1 in ... Obviously, we'd still want to have "case", but written as a macro. The `magicproof` is needed to convince Typer that all union members have a field 0. And of course, each `cast` would also need to provide a proof (constructed from a proof provided by `switch`) that indeed we know that `e` is this specific member of the union. The way I presented it is fairly general, but pretty heavyweight to define and to use: every "case" will be compiled to that big switch-with-proofs and the definition of a "record selection out of a union" (such as the "e.0 <withmagicproof>") seems fairly complex as well. Does anyone here have another approach to suggest? Stefan

5 7

Typer paper for ELS-2017
by Stefan Monnier 30 Jan '17

30 Jan '17

I just saw that the deadline for ELS has been pushed to Feb 6, so we have a bit more time to clean up the paper. Stefan

1 0

[Git][monnier/typer][report/els-2017] -
by Stefan 30 Jan '17

30 Jan '17

Stefan pushed to branch report/els-2017 at Stefan / Typer Commits: dd6ff23d by Stefan Monnier at 2017-01-30T02:00:51-05:00 - - - - - - 2 changed files: - paper.tex - refs.bib Changes: ===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -132,7 +132,7 @@ syntactic malleability of Lisp by relying on the traditional Lisp-style S-expressions and macros. Its main tools to this end are the use of an infix notation for -S-expressions, as well as the use of a pure type system to reduce the number +S-expressions, as well as the use of a Pure Type System to reduce the number of syntactic categories and generally make ``everything'' first-class. \end{abstract} @@ -221,7 +221,7 @@ mixfix elements. The parser is still very primitive, since it uses an operator precedence grammar~\cite{Floyd63}, but is already powerful enough to handle a syntax that will feel familiar to ML and Haskell users. -Typer's core language is based on a pure type system~\cite{Barendregt91b}, +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 @@ -382,12 +382,15 @@ To define a new datatype to represent singly linked lists you can write: List : Type -> Type; type List (a : Type) | nil - | cons a (List a); + | cons (hd : a) (tl : List a); \end{verbatim} %% -Notice that we added a type annotation before the datatype definition: this -is currently needed as a forward declaration otherwise the recursive use of -\id{List} inside its definition is rejected. +where \id{hd} and \id{tl} are field names. We could have written just +\verb+cons a (List a)+ instead to keep the fields anonymous. + +Notice that we added a type annotation for \id{List} before the datatype +definition: this is currently needed as a forward declaration otherwise the +recursive use of \id{List} inside its definition is rejected. More importantly, notice that this forward type declaration of \id{List} uses the same syntax as the previous forward declaration of the function @@ -727,32 +730,139 @@ it was natural and important to be able to distinguish those two cases. \end{array} } \end{displaymath} - \label{fig:Lexp} \caption{Definition of core $\lambda$-expressions} + \label{fig:Lexp} \end{figure} } \FigLexp -No hard coded names: just initial bindings of constructs to special forms -and primitive functions. +Elaboration is the phase in Typer's compiler which turns an S-expression +into what we call a $\lambda$-expression, whose (simplified) representation is +shown in Fig.~\ref{fig:Lexp}. Notice that \id{Lexp} represents both what is +usually considered \emph{expressions} (such as \id{let}, \id{fun}, ...) as +well as what is usually considered as \emph{types} +(e.g.~$\id{arw}~x~t_1~t_2$ which represents the function type +\texttt{(x~:~t$_1$) -> t$_2$}, or \id{adt} which is the representation of an +abstract data type) since this core language is a Pure Type System. -Macros recognized by the type \kw{Macro}. - -Bidirectional type checking. +Elaboration performs the following tasks: +\begin{itemize} +\item Finish the syntactic analysis: distinguish the function calls, from + the macro calls, from the \id{let} definitions, from the \id{case} + analyses, ... +\item Infer and verify the types. +\item Macro expand the macro calls. +\end{itemize} -Lexically scoped macros. +This is the heart of Typer's front-end and requires a fair bit of supporting +functionality: type inference needs to be able to normalize and compare +arbitrary \id{Lexp} terms; while macro expansion requires evaluation of +arbitrary Typer code, either via a small interpreter, or via the complete +compiler and runtime system. -No notion of phase level for bindings~\cite{Flatt02}: instead, when a macro -call is found, the macro definition needs to be \emph{closed} and its -dependencies are all evaluated. Since Typer is pure, these evaluations have -no effect and their results can be cached. +\subsection{Type checking} -Interleaved type checking/inference and macro expansion. +We use a bidirectional type checking~\cite{Pierce00} approach to minimize +the required type annotations. So elaboration is split into two mutually +recursive functions: +\begin{itemize} +\item \id{infer} takes a type environment and an \id{Sexp} and returns the + corresponding elaborated \id{Lexp} along with its type (also an \id{Lexp}). +\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 variable 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. +\item The returned type is verified to be that of a function and then split + into the argument type and the return type. +\item Then \id{check} is called on the argument since we now know its + expected type. +\item Finally we can construct the \id{app} node and return it along with + its type. +\end{enumerate} + +\subsection{Final syntactic analysis} + +Elaboration has to distinguish the different constructs of the language. +In the case of Typer, just as is the case of Scheme, we do it without hard +coding the meaning of any identifier. More specifically, neither \id{check} +nor \id{infer} will check to see if an \id{Sexp} \id{node} has a symbol such +as \id{let\_in\_} as its head. Instead, when those functions encounter +a \id{node}, they do the following: +\begin{enumerate} +\item Call \id{infer} on its head. +\item If the returned type is \id{Special-Form}, make sure the expression is + a primitive (i.e. of the form \id{prim}), and if so, call the + corresponding special form's elaboration function, found in a global + table. There is a special form for each core syntactic construct, such as + \kw{let} and \kw{case}. +\item If the returned type is \id{Macro}, then it is a macro call, and we + expand it, as detailed below. +\item Otherwise, it should be a function call so we do as outlined above. +\end{enumerate} + +Note that at step 2 above, we have to double check that the head is +a \id{prim}, because in case of a source code such as +``\verb|(if x then let_in_ else case_) 42|'' the head is a valid +expression of type \id{Special-Form} but is not a primitive, so we have to +reject such meaningless code. + +So the way keywords like \id{let\_in\_} get their special meaning is simply +by binding them to the corresponding special form primitive in the initial +environment. The programmer is free to rebind those identifiers if she +wants, or to bind the corresponding primitive to other identifiers. + +\subsection{Macro expansion} + +As explained above, a macro call is recognized simply by the fact that the +head of the \id{node} has type \id{Macro}. As before with +\id{Special-Form}, the mere fact that the head has type \id{Macro} does not +guarantee that this is a valid macro. Again we may just be looking at +a source code of the form: +\begin{verbatim} + (if x then mymacro else yourmacro) 42 +\end{verbatim} +where the head may be a valid expression of type \id{Macro} but is not +really a macro because $x$ will only be known at runtime. So, to make sure +we do have a macro, we additionally need to verify that the head expression +is \emph{closed}: it can refer to let-bound variables, as long as these are +themselves \emph{closed}, but it cannot refer to a function's formal +argument. Once established that it is closed, we can just evaluate it to +a value, along with all the let-bound variables to which it refers. +Since Typer is pure, these evaluations have no visible side-effects and +their results can be cached. + +This \emph{closedness} criterion along with the opportunistic evaluation of +required definitions lets us avoid the complexity of a notion such as +binding phase levels used in Scheme~\cite{Flatt02}. It also naturally +supports lexically scoped macros or even higher-order macros. + +The downside of this approach is that it needs to know the type of the head +of a \id{node} to detect a macro call. This makes it virtually impossible +to expand all macros in a separate phase before we infer types. And we +can't infer types before we have expanded the macros either, so we are +forced to interleave macro expansion and type inference within one big +elaboration phase. While this is a significant downside, performing macro +expansion from inside the type inference phase has the advantage that macros +can get access to the complete type environment as well as to the expected +return type of the code it should construct. + +In the context of macros that provide syntax extensions, this is often of +little benefit, but it is crucial for macros that act as \emph{proof + tactics}, where the type environment represents the set of valid +hypotheses, and the expected return type is the proposition one wants to +prove. While Typer is a programming language at heart, its core language is +very similar to that of proof assistants such as Coq, so it can also be used +to write and manipulate propositions and proofs. -Access to the typing environment and expected type of returned code -(i.e. hypotheses and goal, when seen from the point of view of a proof -assistant). \section{Related work} \label{sec:related} ===================================== refs.bib ===================================== --- a/refs.bib +++ b/refs.bib @@ -173,6 +173,7 @@ toiti @string{Paterson= { Ross Paterson }} @string{Pfenning= { Frank Pfenning }} @string{Pientka = { Brigitte Pientka }} +@string{Pierce = { Benjamin C. Pierce }} @string{Piessens= { Frank Piessens }} @string{Plotkin = { Gordon Plotkin }} @string{Pym = { David J. Pym }} @@ -203,6 +204,7 @@ toiti @string{Thiemann= { Peter Thiemann }} @string{Tofte = { Mads Tofte }} @string{Trifonov= { Valery Trifonov }} +@string{Turner = { David M. Turner }} @string{Urban = { Christian Urban }} @string{Vanderwaart={ Joseph C. Vanderwaart }} @string{VanHorn = { Van Horn, David }} @@ -5097,6 +5099,31 @@ toiti examples which illustrate these features.} } +@Article{Pierce00, + author = Pierce #{and}# Turner, + title = {Local type inference}, + journal = TOPLAS, + year = 2000, + volume = 22, + number = 1, + pages = {1-44}, + month = {jan}, + url = {http://dl.acm.org/citation.cfm?id=345100}, + abstract = {We study two partial type inference methods for a language + combining subtyping and impredicative polymorphism. + Both methods are local in the sense that missing + annotations are recovered using only information from + adjacent nodes in the syntax tree, without long-distance + constraints such as unification variables. One method + infers type arguments in polymorphic applications + using a local constraint solver. The other infers + annotations on bound variables in function abstractions by + propagating type constraints downward from enclosing + application nodes. We motivate our design choices + by a statistical analysis of the uses of type inference + in a sizable body of existing ML code.} +} + @InProceedings{Pirinen98, author = {Pekka P. Pirinen}, title = {Barrier Techniques for Incremental Tracing}, @@ -6149,7 +6176,7 @@ toiti pages = {347-359} } @InProceedings{Wadler95, - author = {D. N. Turner and } # Wadler, + author = Turner #{and}# Wadler, title = {Once Upon a Type}, crossref = {FPCA95}, pages = {1-11} View it on GitLab: https://gitlab.com/monnier/typer/commit/dd6ff23da94ffde77026d732ffa3c99459f…

1 0

[Git][monnier/typer][report/els-2017] -
by Stefan 29 Jan '17

29 Jan '17

Stefan pushed to branch report/els-2017 at Stefan / Typer Commits: 6a1f5c7c by Stefan Monnier at 2017-01-29T23:17:35-05:00 - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -15,7 +15,7 @@ \citestyle{acmauthoryear} -\acmConference[ELS'2017]{European Lisp Conference}{April 2017} +\acmConference[ELS'2017]{European Lisp Symposium}{April 2017} {Vrije Universiteit Brussel, Belgium} \acmYear{2017} %% \copyrightyear{2017} @@ -250,23 +250,29 @@ The power of Lisp's macros relies on the following: \subsection{S-expressions} +\newcommand \FigLispSexp { + \begin{figure} + \begin{displaymath} + \MAlign{ + \kw{type}~\id{Sexp} \\ + ~~|~\id{cons}~(\id{car} : \id{Sexp})~(\id{cdr} : \id{Sexp}) \\ + ~~|~\id{symbol}~(\id{name} : \id{String}) \\ + ~~|~\id{number}~\id{Int} \\ + ~~|~\id{string}~\id{String} \\ + } + \end{displaymath} + \caption{Definition of Lisp's S-expressions} + \label{fig:Lisp-Sexp} + \end{figure} +} Once lexical analysis is performed, rather than performing the syntactic analysis in one step, Lisp languages further subdivide the syntactic analysis phase into two steps. The first step does a rudimentary analysis that only extracts a generic tree structure, called S-expression. The shape -of S-expressions could be described with the following algebraic datatype: -%% -\begin{displaymath} - \MAlign{ - \kw{type}~\id{Sexp} \\ - ~~|~\id{cons}~\id{Sexp}~\id{Sexp} \\ - ~~|~\id{symbol}~\id{String} \\ - ~~|~\id{number}~\id{Int} \\ - ~~|~\id{string}~\id{String} \\ - ~~~\ldots - } -\end{displaymath} -%% +of S-expressions could be described with the datatype shown in Fig.~\ref{fig:Lisp-Sexp}. + +\FigLispSexp + Note how, at this stage, there is no notion of bindings, functions, or function calls. It's only in a second step that S-expressions are analyzed to distinguish the various constructs such as macro calls, function calls, @@ -470,15 +476,38 @@ one used in Template Haskell and \id{return} is the unit of that monad. \section{Parsing into S-expressions} \label{sec:parsing} +\newcommand \FigTyperSexp { + \begin{figure} + \begin{displaymath} + \MAlign{ + \kw{type}~\id{Sexp} \\ + ~~|~\id{node}~(\id{head} : \id{Sexp})~(\id{args} : \id{List}~\id{Sexp}) \\ + ~~|~\id{symbol}~(\id{name} : \id{String}) \\ + ~~|~\id{number}~\id{Int} \\ + ~~|~\id{string}~\id{String} \\ + } + \end{displaymath} + \caption{Definition of Typer's S-expressions} + \label{fig:Typer-Sexp} + \end{figure} +} +\FigTyperSexp + Like Lisp, Typer's parsing is done in 3 steps: the first turns the input into a stream of tokens; the second turns this stream into an S-expression tree; and the third finally recognizes the actual language's constructs. -We will first look at the middle step, and we will return to tokenizing later. +Fig.~\ref{fig:Typer-Sexp} shows how Typer's S-expressions are represented +internally. This is very similar to Lisp's representation except that +the \id{cons} constructor is replaced by a \id{node} constructor which +basically enforces that sub-lists are \emph{proper} lists. + +We will first look at the actual syntax analysis step, and we will return to +tokenizing later. \subsection{Operator precedence grammar} -Typer's notion of S-expression is more flexible than Lisp's, since it allows -infix notation. It relies on operator precedence grammars +Typer's external notion of S-expression is more flexible than Lisp's, since +it allows infix notation. It relies on operator precedence grammars (OPG)~\cite{Floyd63} for that. An OPG is a very restrictive subset of context free grammars, much more restrictive than LALR, for example. @@ -665,21 +694,45 @@ it was natural and important to be able to distinguish those two cases. \section{Elaboration to core Typer} \label{sec:elaboration} -\begin{figure} - \begin{displaymath} - \MAlign{ - \kw{type}~\id{Lexp} \\ - ~~|~\id{var}~\id{Id} \\ - ~~|~\id{app}~\id{Lexp}~(\id{List}~\id{Lexp}) \\ - ~~|~\id{fun}~(\id{List}~\id{Id})~\id{Lexp} \\ - ~~|~\id{let}~\id{Id}~\id{Lexp}~\id{Lexp} \\ - ~~|~\id{case}~\id{Lexp}~(\id{List}~\id{Lbranch}) \\ - ~~~\ldots - } - \end{displaymath} - \label{fig:Lexp} - \caption{Definition of $\lambda$-expressions} -\end{figure} +\newcommand \FigLexp { + \begin{figure} + \begin{displaymath} + \MAlign{ + \kw{type}~\id{Lexp} \\ + \hspace{5pt}\begin{array}{@{|~}l@{~}l} + \id{var} & \id{Id} \\ + \id{app} & (f : \id{Lexp})~(\id{arg} : \id{Lexp}) \\ + \id{fun} & (\id{arg} : \id{Id})~(\id{atype} : \id{Lexp}) + ~(\id{body} : \id{Lexp}) \\ + \id{arw} & (\id{arg} : \id{Id})~(\id{atype} : \id{Lexp}) + ~(\id{rtype} : \id{Lexp}) \\ + \id{let} & (\id{var} : \id{Id})~(\id{val} : \id{Lexp}) + ~(\id{body} : \id{Lexp}) \\ + \id{case}& (\id{val} : \id{Lexp}) + ~(\id{cases} : \id{List}~\id{Lbranch}) \\ + \id{con} & (\id{adt} : \id{Lexp})~(\id{name} : \id{Id}) \\ + \id{adt} & (\id{params} : \id{List}~\id{Id}) + ~(\id{cases} : \id{List}~\id{LadtCase}) \\ + \id{prim}& (\id{id} : \id{String}) \\ + \end{array} \medskip \\ + \kw{type}~\id{LadtCase} \\ + \hspace{5pt}\begin{array}{@{|~}l@{~}l} + \id{adtcase} & (\id{name} : \id{Id})~(\id{fields} : + \id{List}~\id{Lexp}) + \end{array} \medskip \\ + \kw{type}~\id{Lbranch} \\ + \hspace{5pt}\begin{array}{@{|~}l@{~}l} + \id{case} & (\id{pattern} : \id{List}~\id{Id}) + ~(\id{body} : \id{Lexp}) + \end{array} + } + \end{displaymath} + \label{fig:Lexp} + \caption{Definition of core $\lambda$-expressions} + \end{figure} +} + +\FigLexp No hard coded names: just initial bindings of constructs to special forms and primitive functions. View it on GitLab: https://gitlab.com/monnier/typer/commit/6a1f5c7c19764ee964272ab9d902564f0b3…

1 0

[Git][monnier/typer][report/els-2017] -
by Stefan 29 Jan '17

29 Jan '17

Stefan pushed to branch report/els-2017 at Stefan / Typer Commits: 678efd2a by Stefan Monnier at 2017-01-29T21:34:28-05:00 - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -175,6 +175,8 @@ of syntactic categories and generally make ``everything'' first-class. \keywords{Macros, S-expressions, Pure Type Systems, ML, Lisp} \maketitle +\renewcommand \shortauthors { + P. Delaunay, V. Archamboult-Bouffard, and S. Monnier} \section{Introduction} @@ -290,22 +292,6 @@ explicitly quoting the macro's arguments (e.g.~passing them as strings), making the macro calls more verbose, and the macro itself harder to implement since you have to manually parse those quoted arguments. -%% \begin{figure} -%% \begin{displaymath} -%% \MAlign{ -%% \kw{type}~\id{Lexp} \\ -%% ~~|~\id{var}~\id{Id} \\ -%% ~~|~\id{app}~\id{Lexp}~(\id{List}~\id{Lexp}) \\ -%% ~~|~\id{fun}~(\id{List}~\id{Id})~\id{Lexp} \\ -%% ~~|~\id{let}~\id{Id}~\id{Lexp}~\id{Lexp} \\ -%% ~~|~\id{case}~\id{Lexp}~(\id{List}~\id{Lbranch}) \\ -%% ~~~\ldots -%% } -%% \end{displaymath} -%% \label{fig:Lexp} -%% \caption{Definition of $\lambda$-expressions} -%% \end{figure} - Of course, it should be noted that the rest of the world re-discovered the power of S-expressions under the name of XML, where it is used for similar reasons: this intermediate parsing stage is a convenient compromise, since @@ -679,6 +665,25 @@ it was natural and important to be able to distinguish those two cases. \section{Elaboration to core Typer} \label{sec:elaboration} +\begin{figure} + \begin{displaymath} + \MAlign{ + \kw{type}~\id{Lexp} \\ + ~~|~\id{var}~\id{Id} \\ + ~~|~\id{app}~\id{Lexp}~(\id{List}~\id{Lexp}) \\ + ~~|~\id{fun}~(\id{List}~\id{Id})~\id{Lexp} \\ + ~~|~\id{let}~\id{Id}~\id{Lexp}~\id{Lexp} \\ + ~~|~\id{case}~\id{Lexp}~(\id{List}~\id{Lbranch}) \\ + ~~~\ldots + } + \end{displaymath} + \label{fig:Lexp} + \caption{Definition of $\lambda$-expressions} +\end{figure} + +No hard coded names: just initial bindings of constructs to special forms +and primitive functions. + Macros recognized by the type \kw{Macro}. Bidirectional type checking. @@ -716,6 +721,9 @@ Coq~\cite{Coq00} \section{Conclusion and future work} \label{sec:conclusion} +Implementation in progress, available from +\url{http://gitlab.com/monnier/typer}. + \begin{acks} The work is supported by the \grantsponsor{NSERC}{National Science and Engineering Research of Canada} View it on GitLab: https://gitlab.com/monnier/typer/commit/678efd2a7dab4a7cce341592ec13f4a97d9…

1 0

[Git][monnier/typer][report/els-2017] -
by Stefan 29 Jan '17

29 Jan '17

Stefan pushed to branch report/els-2017 at Stefan / Typer Commits: 982f07e3 by Stefan Monnier at 2017-01-29T21:13:18-05:00 - - - - - - 2 changed files: - paper.tex - all.bib → refs.bib Changes: ===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -622,6 +622,8 @@ is parsed into the following S-expression: nil (cons a (List a))) \end{verbatim} +Because \id{type} is defined as a prefix operator, and $\mid$ is defined as +an associative infix operator. \subsection{Two-level tokenizing} @@ -677,6 +679,23 @@ it was natural and important to be able to distinguish those two cases. \section{Elaboration to core Typer} \label{sec:elaboration} +Macros recognized by the type \kw{Macro}. + +Bidirectional type checking. + +Lexically scoped macros. + +No notion of phase level for bindings~\cite{Flatt02}: instead, when a macro +call is found, the macro definition needs to be \emph{closed} and its +dependencies are all evaluated. Since Typer is pure, these evaluations have +no effect and their results can be cached. + +Interleaved type checking/inference and macro expansion. + +Access to the typing environment and expected type of returned code +(i.e. hypotheses and goal, when seen from the point of view of a proof +assistant). + \section{Related work} \label{sec:related} @@ -708,8 +727,7 @@ Coq~\cite{Coq00} %% \bibliographystyle{alpha} \bibliographystyle{ACM-Reference-Format} -\bibliography{all.bib} -%% \bibliography{refs.bib} +\bibliography{refs.bib} \end{document} ===================================== all.bib → refs.bib ===================================== --- a/all.bib +++ b/refs.bib @@ -2359,6 +2359,32 @@ toiti crossref = {PLDI93}, pages = "237-247" } +@InProceedings{Flatt02, + author = Flatt, + title = {Composable and Compilable Macros: You Want it When?}, + crossref = {ICFP02}, + pages = {72-83}, + url = {http://dl.acm.org/citation.cfm?id=581486}, + abstract = {Many macro systems, especially for Lisp and Scheme, allow + macro transformers to perform general computation. + Moreover, the language for implementing compile-time macro + transformers is usually the same as the language for + implementing run-time functions. As a side effect of this + sharing, implementations tend to allow the mingling of + compile-time values and run-time values, as well as values + from separate compilations. Such mingling breaks + programming tools that must parse code without executing + it. Macro implementors avoid harmful mingling by obeying + certain macro-definition protocols and by inserting + phase-distinguishing annotations into the code. However, + the annotations are fragile, the protocols are not + enforced, and programmers can only reason about the result + in terms of the compiler's implementation. MzScheme---the + language of the PLT Scheme tool suite---addresses the + problem through a macro system that separates compilation + without sacrificing the expressiveness of macros.} +} + @Article{Floyd63, author = {Robert W. Floyd}, title = {Syntactic Analysis and Operator Precedence}, @@ -6920,6 +6946,15 @@ toiti publisher = ACM, address = {Florence, Italy} } +@Proceedings{ICFP02, + title = ICFP, + booktitle = ICFP, + year = 2002, + key = {ICFP'02}, + month = oct, + publisher = ACM, + address = {Pittsburgh, PA} +} @Proceedings{ICFP03, title = ICFP, booktitle = ICFP, View it on GitLab: https://gitlab.com/monnier/typer/commit/982f07e33d6366997776f51af92be46d515…

1 0

[Git][monnier/typer][report/els-2017] -
by Stefan 29 Jan '17

29 Jan '17

Stefan pushed to branch report/els-2017 at Stefan / Typer Commits: ac04a418 by Stefan Monnier at 2017-01-29T20:30:46-05:00 - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -492,9 +492,9 @@ We will first look at the middle step, and we will return to tokenizing later. \subsection{Operator precedence grammar} Typer's notion of S-expression is more flexible than Lisp's, since it allows -infix notation. It relies on operator precedence grammars (OPG) for that. -An OPG is a very restrictive subset of context free grammars, much more -restrictive than LALR, for example. +infix notation. It relies on operator precedence grammars +(OPG)~\cite{Floyd63} for that. An OPG is a very restrictive subset of +context free grammars, much more restrictive than LALR, for example. You can think of the job of an OPG parser as trying to add parentheses to recover the document's structure: whenever the parser sees something of the @@ -508,7 +508,7 @@ In Typer, the grammar is represented by simply associating to each keyword two precedence levels: one for its left side and another for its right side. Then parsing uses the following rule: when we see ``$\id{kw}_1~e~\id{kw}_2$'', we lookup the right precedence of $\id{kw}_1$ -and the left precedence of $\id{kw}_2$, and we then attach $e$ with +and the left precedence of $\id{kw}_2$, and we then attach $e$ to whichever is higher. While it enjoys an efficient implementation, the motivation behind the View it on GitLab: https://gitlab.com/monnier/typer/commit/ac04a418077ef52f8bd512e6d00d21c8fbb…

1 0

[Git][monnier/typer][report/els-2017] -
by Stefan 29 Jan '17

29 Jan '17

Stefan pushed to branch report/els-2017 at Stefan / Typer Commits: e0136bf8 by Stefan Monnier at 2017-01-29T20:26:27-05:00 - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -648,11 +648,19 @@ But these lexical rules pose a problem in our quest to have an ML-style syntax with a minimalist core: we want to be able to define a module system outside of the core language, and we also want to be able to use a syntax such as \texttt{String.concat} to refer to the \id{concat} function of the -\id{String} module. - -So after splitting tokens according to the above rules, each token is -\emph{parsed} using a grammar, even more limited than the OTG grammar -presented earlier, where \Char{.} can be given the status of infix +\id{String} module. Yet, we can't simply define \Char{.} to be +a \emph{single-char token} character and then define it as an infix +operator, because that would give us +\begin{displaymath} + \begin{array}{r@{\hspace{10pt}\equiv\hspace{10pt}}l} + \verb+String.concat a b+ & \verb+_\._ String (concat a b)+ + \end{array} +\end{displaymath} +We could try to extend out OPG parser so as to allow infix operators to bind +more tightly than the ``space'', but instead we decided to do a two-level +tokenization: after splitting tokens according to the above rules, each +token is \emph{parsed} using a grammar, even more limited than the OPG +grammar presented earlier, where \Char{.} can be given the status of infix operator. We can again override this special handling of a given character by escaping it. So, the following equalities hold: \begin{displaymath} @@ -661,6 +669,10 @@ by escaping it. So, the following equalities hold: \texttt{a * M.b} & \verb+_*_ a (__\.__ M b)+ \end{array} \end{displaymath} +One of the advantages of this two-level approach is that this allows us to +distinguish ``\verb+M.b+'' from ``\verb+M . b+''. Given the fact that +Typer, like Lisp, relies heavily on spaces as separators, we felt that +it was natural and important to be able to distinguish those two cases. \section{Elaboration to core Typer} \label{sec:elaboration} View it on GitLab: https://gitlab.com/monnier/typer/commit/e0136bf8413115f6cbac9f5d8d9bd3b2240…

1 0

[Git][monnier/typer] Deleted branch report/vincent
by Stefan 29 Jan '17

29 Jan '17

Stefan deleted branch report/vincent at Stefan / Typer

1 0

[Git][monnier/typer] Pushed new branch report/vincent-bonnevalle
by Stefan 29 Jan '17

29 Jan '17

Stefan pushed new branch report/vincent-bonnevalle at Stefan / Typer

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Janvier 2017