Type-Dependent Name Resolution

In our ESOP 2015 paper on A Theory of Name Resolution we presented a semantic framework for specification of the name binding patterns in programming languages. We are working on extending this framework with type analysis in order to support declarative specification of type systems. In this technical report we discuss our first results in this direction. We use constraints to formalize type analysis and connect these constraints to the references and declarations in scope graphs to provide a typing context to the names in programs. The connection between names and types is especially interesting in cases where type analysis is needed to perform name resolution, i.e. type-dependent name resolution. This occurs in programming languages in constructs such as field and method access in object-oriented languages, or in with expressions (inspired by Pascal’s with statement). Figure 6 from the paper illustrates how such binding patterns are expressed in our framework using a combination of scope graph and constraints. We have a prototype implementation for the framework performing constraint resolution, and we have a prototype of a new version of our name binding and type analysis DSLs NaBL/TS targeting this framework as back-end.

Hendrik van Antwerpen, Pierre Neron, Andrew P. Tolmach, Eelco Visser, Guido Wachsmuth. Language-Independent Type-Dependent Name Resolution. Technical Report TUD-SERG-2015-006, Delft University of Technology, Software Engineering Research Group, Delft, The Netherlands, July 2015. [researchr, PDF]

Abstract: We extend and combine two existing declarative formalisms, the scope graphs of Neron et al. and type constraint systems, to build a language-independent theory that can describe both name and type resolution for realistic languages with complex scope and typing rules. Unlike conventional static semantics presentations, our approach maintains a clear separation between scoping and typing concerns, while still being able to handle language constructs, such as class field access, for which name and type resolution are necessarily intertwined. We define a constraint scheme that can express both typing and name binding constraints, and give a formal notion of constraint satisfiability together with a sound algorithm for finding solutions in important special cases. We describe the details of constraint generation for a model language that illustrates many of the interesting resolution issues associated with modules, classes, and records. Our constraint generator and solver have been implemented in the Spoofax Language Workbench.