I gave a talk in the PL seminar at TU Delft about our work in progress on formalizing the semantics of disambiguation by associativity and priority rules.

A Direct Semantics of Declarative Disambiguation Rules from Eelco Visser

These are the slides of my talk at the IFIP WG2.16 (Language Design) meeting in Portland in February 2019. The code of the slides can be found in the Statix Sandbox repository on github.

Abstract: In this talk I present the design of Statix, 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 staging 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.

At PEPM 2016 we presented the design of a constraint language for type checking based on scope graphs. That design was the basis for the NaBL2 name and type analysis language that is currently integrated into the Spoofax language workbench. While the approach deals elegantly with a large variety of name binding patterns, including type-dependent name resolution, it was limited to `simple’ type systems. In particular, NaBL2 does not support type systems with structural (anonymous) types and generic (parameterized) types. In our OOPSLA 2018 paper we show that these limitations are not intrinsic to the scope graph model. We show that by using scopes as types, we can model such types. The picture shows the scope graph for a program with structural record types.

To be presented next week at SPLASH 2018 in Boston.

Hendrik van Antwerpen, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser. Scopes as Types. Proceedings of the ACM on Programming Languages, Volume 2 Issue OOPSLA, November 2018, Article No. 114. 10.1145/3276484

Abstract: Scope graphs are a promising generic framework for modeling the binding structures of programming languages, briding formalization and implementation, supporting the definition of type checkers and the automation of type safety proofs. However, previous work on scope graphs has been limited to simple, nominal type systems. In this paper, we show that viewing scopes as types enables us to model the internal structure of types in a range of non-simple type systems (including structural records and generic classes) using the generic representation of scopes. Further, we show that relations between such types can be expressed in terms of generalized scope graph queries. We extend scope graphs with scoped relations and queries. We introduce Statix, a new domain-specific meta-language for the specification of static semantics, based on scope graphs and constraints. We evaluate the scopes as types approach and the Statix design in case studies of STLCREC, System F, and Featherweight Generic Java.

Following up on our paper about the design of the PIE build DSL, a paper at the ASE 2018 conference, to be presented by Gabriël Konat next week, deals with the poor scalability of the Pluto algorithm we used for the implementation of PIE. Since the algorithm inspects the entire dependency graph, even if few nodes are affected by a change, there is a large overhead that becomes significant in large projects. This paper extends the Pluto algorithm with a bottom-up traversal of the dependency graph that only visits nodes affected by a change, dramatically reducing build times in most scenarios.

Gabriël Konat, Sebastian Erdweg, and Eelco Visser. 2018. Scalable incremental building with dynamic task dependencies. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering (ASE 2018). ACM, New York, NY, USA, 76-86. DOI: https://doi.org/10.1145/3238147.3238196

Abstract:

Incremental build systems are essential for fast, reproducible software builds. Incremental build systems enable short feedback cycles when they capture dependencies precisely and selectively execute build tasks efficiently. A much overlooked feature of build systems is the expressiveness of the scripting language, which directly influences the maintainability of build scripts. In this paper, we present a new incremental build algorithm that allows build engineers to use a full-fledged programming language with explicit task invocation, value and file inspection facilities, and conditional and iterative language constructs. In contrast to prior work on incrementality for such programmable builds, our algorithm scales with the number of tasks affected by a change and is independent of the size of the software project being built. Specifically, our algorithm accepts a set of changed files, transitively detects and re-executes affected build tasks, but also accounts for new task dependencies discovered during building. We have evaluated the performance of our algorithm in a real-world case study and confirm its scalability.

Programming language design requires many iterations to get right. Building the tools to use and evaluate a design is an important cost factor. In this talk I discuss and demonstrate the Spoofax language workbench, its high-level declarative meta-languages for the definition of syntax and semantics of programming languages, and the live generation of programming environments from those definitions.