Scopes as Types

October 27, 2018

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.