Scope Graph Types/Schemas - checking and inference

Scope Graph Types/Schemas - checking and inference
Master Project

Project description

Scope graphs are a nice generic framework for describing the name binding structures of programs and programming languages. They are a bit similar to grammars for the description of textual structure. Statix is a domain-specific meta-language for specifying static semantics (mostly names and types) based on scope graphs and constraints.

When you have a Statix specification, this includes the types of the AST (abstract syntax tree) of a programming language, and the rules that map a program of that programming language to a scope graph/constraints. When writing and talking about these specifications, people talk about scope graphs and programs, both with concrete examples and while thinking about patterns in the scope graph that match the binding behaviour of the language. But these patterns, or shapes, are not made explicit.

In this project, we want to explore the description of the shape of the scope graph. You could consider it types, or as it was previously called in group discussions, the schema of the scope graphs of a programming language. We think these will be useful for explaining, understanding, and checking Statix (or other scope-graph-based) specifications. We also think they will unlock the ability to make Statix a fully compiled language, where part of the constraint solving can be optimised out (compiling/optimising Statix will be solidly out of scope for this project). Open questions are such things as:

Can we describe a single scope graph schema that capture the relevant patterns in the scope graph that map to different name binding / typing constructs in the language.
Can we use such a schema to ‘type-check’ Statix rules?
Can we infer such a schema from Statix rules?
Which of those is more useful/natural?