Bootstrapping and Generics for Statix
Master Project of Boris Janssen


Project description

When working with the Spoofax workbench, the Statix meta-language can be used for the specification of Static Semantics. Although type systems expressed in Statix are generally quite concise, Statix’ users often report that support for generics (parametric polymorphism) would reduce clutter in the specification even further. However, before generics can be supported by Statix, it is required that Statix is bootstrapped. This project will consist of implementing and validating these new features. ​

Bootstrapping

It is common practice to write compilers in the language they are compiling. The same can be done for meta-languages, such as Statix. In this project, we will first bootstrap Statix. That is, we express the type system of Statix in Statix itself. Part of this bootstrapping effort will also be devoted to adapting the transformations to use the new analysis result representation.

We see bootstrapping Statix as important for a number of reasons:

  • As a case study on the usage of Statix, it can provide useful insight in the application of Statix.
  • Because there are some large Statix specifications for other languages, bootstrapping Statix generates opportunities for benchmarking, which can lead to further improvements of the Statix backend.
  • Using a more expressive meta-language to specify the type system of Statix, new possibilities for innovation in the Statix language arise, such as support for generics.
Generics

A generic entity in a programming language is an entity that can be used regardless of the exact type of its arguments, while maintaining type-safety. This is desirable, because it allows source code to be more concise. A typical example is manipulation of list structures, without manipulating the contained objects.

There are multiple approaches to compilation of generic language constructs. One of these approaches is template expansion, which means that for every set of (type) parameters a specialized instance of the parametric construct is created. ​ In this project, we implement generics for various constructs, such as user-defined constraints, in Statix. These generic constructs will be desugared to core constructs using template expansion. The choice for template expansion is motivated by the fact that this strategy does not complicate other aspects of the language, especially the permission analysis and the solver.

We expect this to be an full-fledged language engineering project, involving both high-level design (What would generics in Statix look like) and the implementation of syntax, static semantics and ‘compilation’ through template expansion. Particular interesting challenges we expect are:

  1. Hygiene in expansion,
  2. Assigning proper error locations to static errors arising at use sites
  3. Managing the interplay between analysis of templates, template expansion and the analysis of the expanded program.

Relevant literature:

[1] Gabriël Konat, Sebastian Erdweg, and Eelco Visser. 2016. Bootstrapping domain-specific meta-languages in language workbenches. SIGPLAN Not. 52, 3 (March 2017), 47–58.

[2] Hindley, Roger. “The principal type-scheme of an object in combinatory logic.” Transactions of the american mathematical society 146 (1969): 29-60.

[3] Tim Sheard and Simon Peyton Jones. 2002. Template meta-programming for Haskell. In Proceedings of the 2002 ACM SIGPLAN workshop on Haskell (Haskell ‘02). Association for Computing Machinery, New York, NY, USA, 1–16.

[4] Eugene Kohlbecker, Daniel P. Friedman, Matthias Felleisen, and Bruce Duba. 1986. Hygienic macro expansion. In Proceedings of the 1986 ACM conference on LISP and functional programming (LFP ‘86). Association for Computing Machinery, New York, NY, USA, 151–161.

[5] Hendrik van Antwerpen, Casper Bach Poulsen, Arjen Rouvoet, and Eelco Visser. 2018. Scopes as types. Proc. ACM Program. Lang. 2, OOPSLA, Article 114 (November 2018), 30 pages.

Contacts for the project


Bootstrapping and Generics for Statix

Student: Boris Janssen
Supervisor(s): Aron Zwaan, Eelco Visser