Skip to content

A Statix Bibliography

The Statix1 2 meta-language provides support for the declarative definition of the static semantics of programming languages in terms of unification constraints and scope graph constraints for name resolution1 guaranteeing query stability2. Here we trace the development of the Statix language.

The NaBL Name Binding Language

The NaBL3 language provides support for the declaration of the name binding rules of programming languages in terms of definitions, references, and scoping.

The NaBL task engine supports incremental execution of type checkers based on NaBL4.

While the paper used the WebDSL language as example, the NaBL analysis was only applied in production in the SDF3 language.

The NaBL language is very declarative, but binding patterns such as sequential let and 'subsequent scope' are difficult to express in it.

Scope Graphs

The study of the semantics of NaBL (and its limits in expressiveness) led to the formulation of a general theory of name resolution based on scope graphs5.

The vertices of scope graphs are scopes and the edges model reachability. Declarations are associated with scopes. Name resolution by means of a declarative resolution calculus is defined as finding a path from the scope of a reference to the scope of a declaration taking into account the structure of the scope graph extended with visibility rules formulated in terms of path well-formedness and path specificity.

Constraint Language

Based on the theory of name resolution, a constraint language was defined with a declarative and operational semantics6.

The language was designed for a two stage type checking process. In the first phase unification and scope constraints are generated, in the second phase these constraints are solved. A distinctive feature of this approach with respect to other constraint-based approaches to type checking, is the fact that name resolution is deferred until constraint resolution. This makes the definition of type-dependent name resolution, e.g. for computing the types of record fields, straightforward.

The NaBL2 language was a concrete implementation of this design and was integrated into Spoofax. It featured concrete syntax for unification and scope graph constraints, and rules for mapping AST nodes to constraints.

The two stage type checking process entailed limitations for the type systems that could be expressed in NaBL2. In particular, it was not possible to generate constraints based on information computed during the second stage. For example, a subtyping rule operating on types computed during constraint resolution

Furthermore, the NaBL2 language itself was untyped, making it easy to make errors in specifications.

Statix Language

The Statix language1 was designed to overcome the limitations of NaBL2.

The language is typed, with signatures describing the types of ASTs, and typing rules declaring the types of predicates. The type system of Statix is expressed in NaBL2, making the specification of rules statically checked and much less prone to errors. This also provided a useful testbed of the ideas of scope graphs and constraints.

The generation and resolution of constraints is intertwined, in order to allow computing constraints over inferred information.

Furthermore, in order to generalize the notions of visibility supported by the NaBL2 language, Statix features query constraints, in order to relate references to declarations, but also to compute sets of names based on broader criteria. For example, the definition of structural record types can be expressed by a query that produces all fields of a record.

Necessarily these changes entail that queries need to be executed in a scope graph that is not in its final form.

This necessitate a theory of query stability. Name resolution queries such be scheduled such that they produce stable results, i.e. results that would also be produced at the end of the process. The this end a theory of critical edges was developed that asserts when it is safe to perform a query in a certain scope2.

The Statix solver implements the operational semantics on the language in order to automatically derive type checkers from specifications. Optimizations of this solver can be based on the generaly underlying theory and be applied to all languages for which Statix specifications have been written. One such optimization is the derivation of implicitly parallel type checkers from Statix specifications[@AntwerpenV21-preprint].

Editor Services

A next step in the evolution of Statix is the derivation of semantic editor services such as renaming and code completion from specifications7.

References

  1. Hendrik van Antwerpen, Casper Bach Poulsen, Arjen Rouvoet, and Eelco Visser. Scopes as types. Proceedings of the ACM on Programming Languages, 2018. URL: https://doi.org/10.1145/3276484, doi:10.1145/3276484. ↩↩↩

  2. Arjen Rouvoet, Hendrik van Antwerpen, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser. Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications. Proceedings of the ACM on Programming Languages, 2020. URL: https://doi.org/10.1145/3428248, doi:10.1145/3428248. ↩↩↩

  3. Gabriël Konat, Lennart C. L. Kats, Guido Wachsmuth, and Eelco Visser. Declarative name binding and scope rules. In Krzysztof Czarnecki and Görel Hedin, editors, Software Language Engineering, 5th International Conference, SLE 2012, Dresden, Germany, September 26-28, 2012, Revised Selected Papers, volume 7745 of Lecture Notes in Computer Science, 311–331. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-36089-3_18, doi:10.1007/978-3-642-36089-3_18. ↩

  4. Guido Wachsmuth, Gabriël Konat, Vlad A. Vergu, Danny M. Groenewegen, and Eelco Visser. A language independent task engine for incremental name and type analysis. In Martin Erwig, Richard F. Paige, and Eric Van Wyk, editors, Software Language Engineering - 6th International Conference, SLE 2013, Indianapolis, IN, USA, October 26-28, 2013. Proceedings, volume 8225 of Lecture Notes in Computer Science, 260–280. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-319-02654-1_15, doi:10.1007/978-3-319-02654-1_15. ↩

  5. Pierre Néron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. A theory of name resolution. In Jan Vitek, editor, Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9032 of Lecture Notes in Computer Science, 205–231. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46669-8_9, doi:10.1007/978-3-662-46669-8_9. ↩

  6. Hendrik van Antwerpen, Pierre Néron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. A constraint language for static semantic analysis based on scope graphs. In Martin Erwig and Tiark Rompf, editors, Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, 49–60. ACM, 2016. URL: http://doi.acm.org/10.1145/2847538.2847543, doi:10.1145/2847538.2847543. ↩

  7. Daniël A. A. Pelsmaeker, Hendrik van Antwerpen, and Eelco Visser. Towards language-parametric semantic editor services based on declarative type system specifications (brave new idea paper). In Alastair F. Donaldson, editor, 33rd European Conference on Object-Oriented Programming, ECOOP 2019, July 15-19, 2019, London, United Kingdom, volume 134 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2019.26, doi:10.4230/LIPIcs.ECOOP.2019.26. ↩

Last update: October 17, 2024
Created: October 17, 2024