Scoping rules on a platter
Larisse Voufo, Marcin Zalewski, Andrew Lumsdaine · 2014
We present a simple and generic way to reason about name binding. Name binding is an essential component of every nontrivial programming language, matching uses of names, references, with the things that they name, declarations, based on scoping rules defined by the language. The definition of name binding is often entangled with the language-specific details, which makes abstract and comparative analysis of competing designs challenging. We present a framework that allows to abstract the fundamental notions of references, declarations, and scopes, and to express scoping rules in terms of four scope combinators and three properties of a specific programming language encapsulated in a concept named Language. Using this framework, we clarify complex scoping rules like argument-dependent lookup in C++, investigate the implications of the concepts feature for C++, and introduce a novel scoping rule named weak hiding. In an ideal world, specifications could be formulated based on our framework, and compilers could use such formulation to unambiguously implement name binding. While our examples are primarily centered around C++ and lexical scoping, our framework has applications in other languages and dynamic scoping.