Declarative Language Definition with the Spoofax Language Workbench
Eelco Visser
Tutorial at PLDI 2020
June 16, 2020

The Spoofax language workbench supports the high-level definition of (domain-specific) programming languages by means of meta-languages and the automatic derivation of implementations from such definitions. A declarative meta-language allows the language designer to abstract from irrelevant implementation details and focus on the essence of a language.

This tutorial will provide an introduction to two meta-languages from the Spoofax language workbench for the definition of syntax and static semantics and demonstrate their application. The tutorial will cover three topics:

(1) Declarative syntax definition with SDF3: the extension of context-free grammars to syntax definitions by means of features such as constructors, layout templates, lexical syntax, and declarative disambiguation in order to derive full featured syntax aware editors.

(2) Name binding and resolution with scope graphs: the definition of a framework for the representation of a wide range of name binding rules, including (mutually recursive) modules and imports.

(3) Type system definition with the Statix constraint language: the interaction between name and type resolution and the automatic scheduling of name resolution queries in order to ensure that all information is collected before it is used.

Live Programming

During the tutorial I will do mostly live programming building the syntax and type checker of a small language. You can find the code that I will recreate during the tutorial at https://github.com/MetaBorgCube/statix-sandbox/tree/master/london. In the first part of the tutorial we look at syntax using the london.syntax project. In the second part we look at static semantics using the london project. The complete code is in the london project, examples in london.example and tests in london.syntax.test and london.test.

I will be using a recent development release (from June 10) of Spoofax, which you can find at http://www.metaborg.org/en/latest/source/release/development.html. I have not installed the very latest development release, so there is a slight chance that something will break.

About Spoofax

For an overview of the Spoofax Language Workbench see http://metaborg.org.

The main publication about Spoofax1 is

  • The Spoofax language workbench: rules for declarative specification of languages and IDEs. Lennart C. L. Kats, Eelco Visser. OOPSLA 2010 [doi]

There is not one paper about Spoofax2, but many about aspects. This Onward’14 paper presents a vision towards higher-level language definitions:

  • A Language Designer’s Workbench: A One-Stop-Shop for Implementation and Verification of Language Designs. Eelco Visser, Guido Wachsmuth, Andrew P. Tolmach, Pierre Néron, Vlad A. Vergu, Augusto Passalaqua, Gabriël Konat. Onward 2014 [doi]

About SDF3

SDF3 is a syntax definition formalism in the SDF family of languages. It supports character-level grammars based on Scannerless Generalized LR (SGLR) parsing. SDF3 further supports abstract syntax tree constructors, templates (for pretty-printing and completion), declarative disambiguation, modules, and many more. Look for papers about aspects of SDF3 at my publication page. An overview paper about SDF3 is forthcoming. Papers that were mentioned during the tutorial:

  • Declarative specification of indentation rules: a tooling perspective on parsing and pretty-printing layout-sensitive languages. Luís Eduardo de Souza Amorim, Michael J. Steindorfer, Sebastian Erdweg, Eelco Visser. SLE 2018 [doi]

  • Principled syntactic code completion using placeholders. Luis Eduardo de Souza Amorim, Sebastian Erdweg, Guido Wachsmuth, Eelco Visser. SLE 2016 [doi]

About Statix

Statix is a new constraint-based language for the executable specification of type systems. Statix specifications consist of predicates that define the well-formedness of language constructs in terms of built-in and user-defined constraints. Statix has a declarative semantics that defines whether a model satisfies a constraint. The operational semantics of Statix is defined as a sound constraint solving algorithm that searches for a solution for a constraint. The aim of the design is that Statix users can ignore the execution order of constraint solving and think in terms of the declarative semantics.

A distinctive feature of Statix is its use of scope graphs, a language parametric framework for the representation and querying of the name binding facts in programs. Since types depend on name resolution and name resolution may depend on types, it is typically not possible to construct the entire scope graph of a program before type constraint resolution. In (algorithmic) type system specifications this leads to explicit ordering of the construction and querying of the type environment (class table, symbol table). Statix automatically stages the construction of the scope graph of a program such that queries are never executed when their answers may be affected by future scope graph extension. In the talk, I will explain the design of Statix by means of examples and discuss the distinction between its declarative and operational semantics.

The design of Statix is based on the following publications:

  • Scopes as types. Hendrik van Antwerpen, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser. PACMPL 2(OOPSLA) 2018 [doi]

  • A constraint language for static semantic analysis based on scope graphs. Hendrik van Antwerpen, Pierre Néron, Andrew P. Tolmach, Eelco Visser, Guido Wachsmuth. PEPM 2016 [doi]

  • A Theory of Name Resolution. Pierre Néron, Andrew P. Tolmach, Eelco Visser, Guido Wachsmuth. ESOP 2015 [doi]

Speaker: Eelco Visser (TU Delft) 

Bio: Eelco Visser is Professor of Computer Science and chair of the Programming Languages Group at Delft University of Technology. His current research is on the foundation and implementation of declarative specification of programming languages. The results of the research are integrated in the Spoofax Language Workbench (http://metaborg.org). For more information see http://eelcovisser.org.